Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/backends/C/c_backend_spec.ml | ||
---|---|---|
195 | 195 |
pp_var_decl |
196 | 196 |
|
197 | 197 |
let pp_forall pp_l pp_r fmt (l, r) = |
198 |
fprintf fmt "@[<v 2>\\forall %a;@,%a@]" pp_l l pp_r r
|
|
198 |
fprintf fmt "@[<v 2>\\forall @[<hov>%a@];@,%a@]" pp_l l pp_r r
|
|
199 | 199 |
|
200 | 200 |
let pp_exists pp_l pp_r fmt (l, r) = |
201 | 201 |
fprintf fmt "@[<v 2>\\exists %a;@,%a@]" pp_l l pp_r r |
... | ... | |
240 | 240 |
let pp_initialization pp_mem fmt (name, mem) = |
241 | 241 |
fprintf fmt "%s_initialization(%a)" name pp_mem mem |
242 | 242 |
|
243 |
let pp_init pp_mem fmt (name, mem) = |
|
244 |
fprintf fmt "%s_init(%a)" name pp_mem mem |
|
245 |
|
|
243 | 246 |
let pp_initialization' = pp_initialization pp_print_string |
244 | 247 |
|
245 | 248 |
let pp_local m = |
... | ... | |
628 | 631 |
let pp_lemma pp_l pp_r fmt (l, r) = |
629 | 632 |
fprintf fmt "@[<v 2>lemma %a:@,%a;@]" pp_l l pp_r r |
630 | 633 |
|
634 |
let pp_axiomatic pp_l pp_r fmt (l, r) = |
|
635 |
fprintf fmt "@[<v 2>axiomatic %a {@,%a@]@;}" pp_l l pp_r r |
|
636 |
|
|
637 |
let pp_axiom pp_l pp_r fmt (l, r) = |
|
638 |
fprintf fmt "@[<v 2>axiom %a:@,%a;@]" pp_l l pp_r r |
|
639 |
|
|
631 | 640 |
let pp_mem_valid_def fmt m = |
632 | 641 |
if not (fst (get_stateless_status m)) then |
633 | 642 |
let name = m.mname.node_id in |
... | ... | |
991 | 1000 |
fmt |
992 | 1001 |
() |
993 | 1002 |
|
994 |
let pp_node_spec m fmt = function |
|
995 |
| Contract c |
|
996 |
| NodeSpec (_, Some c) -> |
|
997 |
PrintSpec.pp_spec PrintSpec.TransitionMode m fmt |
|
998 |
(Spec_common.red (Imply (c.mc_pre, c.mc_post))) |
|
999 |
| NodeSpec (f, None) -> |
|
1000 |
pp_print_string fmt f |
|
1003 |
let spec_from_contract c = |
|
1004 |
Spec_common.red (Imply (c.mc_pre, c.mc_post)) |
|
1005 |
|
|
1006 |
let pp_contract m fmt c = |
|
1007 |
PrintSpec.pp_spec PrintSpec.TransitionMode m fmt (spec_from_contract c) |
|
1008 |
|
|
1009 |
let contract_of machines m = |
|
1010 |
match m.mspec.mnode_spec with |
|
1011 |
| Some spec -> |
|
1012 |
begin match spec with |
|
1013 |
| Contract c -> |
|
1014 |
Some c, None |
|
1015 |
| NodeSpec f -> |
|
1016 |
let m_f = find_machine f machines in |
|
1017 |
begin match m_f.mspec.mnode_spec with |
|
1018 |
| Some (Contract c) -> |
|
1019 |
Some c, Some m_f |
|
1020 |
| _ -> |
|
1021 |
None, None |
|
1022 |
end |
|
1023 |
end |
|
1024 |
| None -> |
|
1025 |
None, None |
|
1026 |
|
|
1027 |
let pp_init_def fmt m = |
|
1028 |
let name = m.mname.node_id in |
|
1029 |
let mem = mk_mem m in |
|
1030 |
pp_predicate |
|
1031 |
(pp_init (pp_machine_decl' ~ghost:true)) |
|
1032 |
(pp_and pp_initialization' (pp_reset_flag' ~indirect:false)) |
|
1033 |
fmt |
|
1034 |
((name, (name, mem)), ((name, mem), mem)) |
|
1035 |
|
|
1036 |
let rename n x = sprintf "%s_%d" x n |
|
1037 |
|
|
1038 |
let rename_var_decl n vd = { vd with var_id = rename n vd.var_id } |
|
1039 |
|
|
1040 |
let rec rename_value n v = |
|
1041 |
{ v with value_desc = |
|
1042 |
match v.value_desc with |
|
1043 |
| Machine_code_types.Var v -> Machine_code_types.Var (rename_var_decl n v) |
|
1044 |
| Fun (f, vs) -> Fun (f, List.map (rename_value n) vs) |
|
1045 |
| Array vs -> Array (List.map (rename_value n) vs) |
|
1046 |
| Access (v1, v2) -> Access (rename_value n v1, rename_value n v2) |
|
1047 |
| Power (v1, v2) -> Power (rename_value n v1, rename_value n v2) |
|
1048 |
| v -> v |
|
1049 |
} |
|
1050 |
|
|
1051 |
let rename_expression: type a. int -> (value_t, a) expression_t -> (value_t, a) expression_t = |
|
1052 |
fun n -> function |
|
1053 |
| Val v -> Val (rename_value n v) |
|
1054 |
| Var v -> Var (rename_var_decl n v) |
|
1055 |
| e -> e |
|
1056 |
|
|
1057 |
let rename_predicate n = function |
|
1058 |
| Transition (f, inst, i, es, r, mf, mif) -> |
|
1059 |
Transition (f, inst, i, List.map (rename_expression n) es, r, mf, mif) |
|
1060 |
| p -> p |
|
1061 |
|
|
1062 |
let rec rename_formula n = function |
|
1063 |
| Equal (e1, e2) -> Equal (rename_expression n e1, rename_expression n e2) |
|
1064 |
| And fs -> And (List.map (rename_formula n) fs) |
|
1065 |
| Or fs -> Or (List.map (rename_formula n) fs) |
|
1066 |
| Imply (f1, f2) -> Imply (rename_formula n f1, rename_formula n f2) |
|
1067 |
| Exists (xs, f) -> Exists (List.map (rename_var_decl n) xs, rename_formula n f) |
|
1068 |
| Forall (xs, f) -> Forall (List.map (rename_var_decl n) xs, rename_formula n f) |
|
1069 |
| Ternary (e, t, f) -> Ternary (rename_expression n e, rename_formula n t, rename_formula n f) |
|
1070 |
| Predicate p -> Predicate (rename_predicate n p) |
|
1071 |
| ExistsMem (x, f1, f2) -> ExistsMem (rename n x, rename_formula n f1, rename_formula n f2) |
|
1072 |
| Value v -> Value (rename_value n v) |
|
1073 |
| f -> f |
|
1074 |
|
|
1075 |
|
|
1076 |
let rename_contract n c = |
|
1077 |
{ c with |
|
1078 |
mc_pre = rename_formula n c.mc_pre; |
|
1079 |
mc_post = rename_formula n c.mc_post; } |
|
1080 |
|
|
1081 |
let but_last l = |
|
1082 |
List.(rev (tl (rev l))) |
|
1083 |
|
|
1084 |
let pp_k_induction_case case m pp_mem_in pp_mem_out pp_vars fmt (n, mem_in, mem_out) = |
|
1085 |
let name = m.mname.node_id in |
|
1086 |
let inputs = m.mstep.step_inputs in |
|
1087 |
let outputs = m.mstep.step_outputs in |
|
1088 |
fprintf fmt "%s_%s_%d(@[<hov>%a,@;%a,@;%a@])" |
|
1089 |
name |
|
1090 |
case |
|
1091 |
n |
|
1092 |
pp_mem_in |
|
1093 |
mem_in |
|
1094 |
pp_vars |
|
1095 |
(inputs @ outputs) |
|
1096 |
pp_mem_out |
|
1097 |
mem_out |
|
1098 |
|
|
1099 |
let pp_k_induction_base_case m = |
|
1100 |
pp_k_induction_case "base" m |
|
1101 |
|
|
1102 |
let pp_k_induction_inductive_case m = |
|
1103 |
pp_k_induction_case "inductive" m |
|
1104 |
|
|
1105 |
let pp_base_cases m fmt (c, m_c, k) = |
|
1106 |
let name = m.mname.node_id in |
|
1107 |
let mem = mk_mem m in |
|
1108 |
let inputs = m.mstep.step_inputs in |
|
1109 |
let outputs = m.mstep.step_outputs in |
|
1110 |
let l = List.init (k - 1) (fun n -> n + 1) in |
|
1111 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut |
|
1112 |
(fun fmt n -> |
|
1113 |
let l = List.init (n + 1) (fun n -> n) in |
|
1114 |
let l' = List.init n (fun n -> n) in |
|
1115 |
let pp = |
|
1116 |
pp_implies |
|
1117 |
(pp_and |
|
1118 |
(pp_and_l (fun fmt -> function |
|
1119 |
| 0 -> |
|
1120 |
pp_init pp_print_string fmt (name, rename 0 mem) |
|
1121 |
| n -> |
|
1122 |
pp_transition_aux m pp_print_string pp_print_string pp_var_decl |
|
1123 |
fmt |
|
1124 |
(name, |
|
1125 |
List.map (rename_var_decl n) (inputs @ outputs), |
|
1126 |
rename (n - 1) mem, |
|
1127 |
rename n mem))) |
|
1128 |
(pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl)) |
|
1129 |
(pp_contract m) |
|
1130 |
in |
|
1131 |
pp_predicate |
|
1132 |
(pp_k_induction_base_case |
|
1133 |
m |
|
1134 |
(pp_machine_decl' ~ghost:true) |
|
1135 |
(pp_machine_decl' ~ghost:true) |
|
1136 |
(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl n) xs))) |
|
1137 |
(pp_forall (pp_locals m) |
|
1138 |
(if n > 1 then |
|
1139 |
pp_forall |
|
1140 |
(fun fmt l -> fprintf fmt "%a@,%a" |
|
1141 |
(pp_machine_decl ~ghost:true |
|
1142 |
(pp_comma_list ~pp_eol:pp_print_comma |
|
1143 |
(fun fmt n -> pp_print_string fmt (rename n mem)))) |
|
1144 |
(name, but_last l) |
|
1145 |
(pp_locals m) |
|
1146 |
(List.flatten |
|
1147 |
(List.map (fun n -> |
|
1148 |
List.map (rename_var_decl n) (inputs @ outputs)) |
|
1149 |
(List.tl l)))) |
|
1150 |
pp |
|
1151 |
else |
|
1152 |
fun fmt (_, x) -> pp fmt x)) |
|
1153 |
fmt |
|
1154 |
((n, (name, rename (n - 1) mem), (name, rename n mem)), |
|
1155 |
(List.map (rename_var_decl n) m_c.mstep.step_outputs, |
|
1156 |
(l', ((l, |
|
1157 |
(m_c.mname.node_id, |
|
1158 |
List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs), |
|
1159 |
"", "")), |
|
1160 |
rename_contract n c))))) |
|
1161 |
fmt |
|
1162 |
l |
|
1163 |
|
|
1164 |
let pp_inductive_case m fmt (c, m_c, k) = |
|
1165 |
let name = m.mname.node_id in |
|
1166 |
let mem = mk_mem m in |
|
1167 |
let inputs = m.mstep.step_inputs in |
|
1168 |
let outputs = m.mstep.step_outputs in |
|
1169 |
let l = List.init k (fun n -> n + 1) in |
|
1170 |
let pp = |
|
1171 |
pp_implies |
|
1172 |
(pp_and_l (fun fmt n -> |
|
1173 |
pp_and |
|
1174 |
(pp_and |
|
1175 |
(pp_transition_aux m pp_print_string pp_print_string pp_var_decl) |
|
1176 |
(pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl)) |
|
1177 |
(pp_contract m) |
|
1178 |
fmt |
|
1179 |
(((name, |
|
1180 |
List.map (rename_var_decl n) (inputs @ outputs), |
|
1181 |
rename (n - 1) mem, |
|
1182 |
rename n mem), |
|
1183 |
(m_c.mname.node_id, |
|
1184 |
List.map (rename_var_decl n) (m_c.mstep.step_inputs @ m_c.mstep.step_outputs), |
|
1185 |
"", "")), |
|
1186 |
rename_contract n c))) |
|
1187 |
(pp_contract m) |
|
1188 |
in |
|
1189 |
pp_predicate |
|
1190 |
(pp_k_induction_inductive_case |
|
1191 |
m |
|
1192 |
(pp_machine_decl' ~ghost:true) |
|
1193 |
(pp_machine_decl' ~ghost:true) |
|
1194 |
(fun fmt xs -> pp_locals m fmt (List.map (rename_var_decl k) xs))) |
|
1195 |
(pp_forall (pp_locals m) |
|
1196 |
(if k > 1 then |
|
1197 |
pp_forall |
|
1198 |
(fun fmt l -> fprintf fmt "%a@,%a" |
|
1199 |
(pp_machine_decl ~ghost:true |
|
1200 |
(pp_comma_list ~pp_eol:pp_print_comma |
|
1201 |
(fun fmt n -> pp_print_string fmt (rename (n - 1) mem)))) |
|
1202 |
(name, but_last l) |
|
1203 |
(pp_locals m) |
|
1204 |
(List.flatten |
|
1205 |
(List.map (fun n -> |
|
1206 |
List.map (rename_var_decl (n - 1)) (inputs @ outputs)) |
|
1207 |
(List.tl l)))) |
|
1208 |
pp |
|
1209 |
else |
|
1210 |
fun fmt (_, x) -> pp fmt x)) |
|
1211 |
fmt |
|
1212 |
((k, (name, rename (k - 1) mem), (name, rename k mem)), |
|
1213 |
(List.(flatten (List.map (fun n -> List.map (rename_var_decl n) m_c.mstep.step_outputs) l)), |
|
1214 |
(l, (l, rename_contract k c)))) |
|
1215 |
|
|
1216 |
let pp_k_induction_lemmas m fmt k = |
|
1217 |
let name = m.mname.node_id in |
|
1218 |
let mem_in = mk_mem_in m in |
|
1219 |
let mem_out = mk_mem_out m in |
|
1220 |
let inputs = m.mstep.step_inputs in |
|
1221 |
let outputs = m.mstep.step_outputs in |
|
1222 |
let l = List.init k (fun n -> n + 1) in |
|
1223 |
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut |
|
1224 |
(fun fmt n -> |
|
1225 |
pp_lemma |
|
1226 |
(fun fmt n -> fprintf fmt "%s_k_induction_%d" name n) |
|
1227 |
(pp_forall |
|
1228 |
(fun fmt () -> fprintf fmt "%a,@;%a" |
|
1229 |
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string)) |
|
1230 |
(name, [mem_in; mem_out]) |
|
1231 |
(pp_locals m) |
|
1232 |
(inputs @ outputs)) |
|
1233 |
((if n = k then |
|
1234 |
pp_k_induction_inductive_case |
|
1235 |
else |
|
1236 |
pp_k_induction_base_case) |
|
1237 |
m |
|
1238 |
pp_print_string |
|
1239 |
pp_print_string |
|
1240 |
(pp_comma_list pp_var_decl))) |
|
1241 |
fmt |
|
1242 |
(n, ((), (n, mem_in, mem_out)))) |
|
1243 |
fmt |
|
1244 |
l |
|
1245 |
|
|
1246 |
let pp_k_induction_axiom m fmt (c, m_c, k) = |
|
1247 |
let name = m.mname.node_id in |
|
1248 |
let mem_in = mk_mem_in m in |
|
1249 |
let mem_out = mk_mem_out m in |
|
1250 |
let inputs = m.mstep.step_inputs in |
|
1251 |
let outputs = m.mstep.step_outputs in |
|
1252 |
let l = List.init k (fun n -> n + 1) in |
|
1253 |
pp_axiomatic |
|
1254 |
(fun fmt () -> fprintf fmt "%s_k_Induction" name) |
|
1255 |
(pp_axiom |
|
1256 |
(fun fmt () -> fprintf fmt "%s_k_induction" name) |
|
1257 |
(pp_forall |
|
1258 |
(pp_locals m) |
|
1259 |
(pp_forall |
|
1260 |
(fun fmt () -> fprintf fmt "%a,@;%a" |
|
1261 |
(pp_machine_decl ~ghost:true (pp_comma_list pp_print_string)) |
|
1262 |
(name, [mem_in; mem_out]) |
|
1263 |
(pp_locals m) |
|
1264 |
(inputs @ outputs)) |
|
1265 |
(pp_implies |
|
1266 |
(pp_and |
|
1267 |
(pp_and_l |
|
1268 |
(fun fmt n -> |
|
1269 |
(if n = k then |
|
1270 |
pp_k_induction_inductive_case |
|
1271 |
else |
|
1272 |
pp_k_induction_base_case) |
|
1273 |
m |
|
1274 |
pp_print_string |
|
1275 |
pp_print_string |
|
1276 |
(pp_comma_list pp_var_decl) |
|
1277 |
fmt |
|
1278 |
(n, mem_in, mem_out))) |
|
1279 |
(pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl)) |
|
1280 |
(pp_contract m))))) |
|
1281 |
fmt |
|
1282 |
((), |
|
1283 |
((), |
|
1284 |
(m_c.mstep.step_outputs, |
|
1285 |
((), |
|
1286 |
(((l, |
|
1287 |
(m_c.mname.node_id, |
|
1288 |
m_c.mstep.step_inputs @ m_c.mstep.step_outputs, |
|
1289 |
"", "")), c)))))) |
|
1290 |
|
|
1291 |
|
|
1292 |
let pp_k_induction m fmt (_, _, k as c_m_k) = |
|
1293 |
pp_acsl_cut |
|
1294 |
(fun fmt () -> fprintf fmt "%a@,@,%a@,@,%a@,@,%a@,@,%a" |
|
1295 |
pp_init_def m |
|
1296 |
(pp_base_cases m) c_m_k |
|
1297 |
(pp_inductive_case m) c_m_k |
|
1298 |
(pp_k_induction_lemmas m) k |
|
1299 |
(pp_k_induction_axiom m) c_m_k) |
|
1300 |
fmt |
|
1301 |
() |
|
1302 |
|
|
1303 |
let pp_proof_annotation m m_c fmt c = |
|
1304 |
let pp m_c fmt = function |
|
1305 |
| Kinduction k -> |
|
1306 |
pp_k_induction m fmt (c, m_c, k) |
|
1307 |
in |
|
1308 |
match m_c with |
|
1309 |
| Some m_c -> |
|
1310 |
pp_print_option (pp m_c) fmt c.mc_proof |
|
1311 |
| None -> () |
|
1001 | 1312 |
|
1002 | 1313 |
let pp_step_spec fmt machines self mem m = |
1003 | 1314 |
let name = m.mname.node_id in |
... | ... | |
1014 | 1325 |
let pp_if_outputs pp = |
1015 | 1326 |
if outputs = [] then pp_print_nothing else pp |
1016 | 1327 |
in |
1017 |
let spec = m.mspec.mnode_spec in
|
|
1328 |
let c, m_c = contract_of machines m in
|
|
1018 | 1329 |
(* (\* prevent printing an ensures clause with contract name *\) |
1019 | 1330 |
* let spec = |
1020 | 1331 |
* match m.mspec.mnode_spec with |
... | ... | |
1022 | 1333 |
* | s -> s |
1023 | 1334 |
* in *) |
1024 | 1335 |
let pp_spec = pp_print_option |
1025 |
(if m.mis_contract then pp_print_nothing else pp_ensures (pp_node_spec m)) in |
|
1336 |
(if m.mis_contract then pp_print_nothing else pp_ensures (pp_contract m)) in |
|
1337 |
let pp_spec_vars, pp_assigns_spec_vars = |
|
1338 |
match m.mspec.mnode_spec with |
|
1339 |
| Some (NodeSpec f) -> |
|
1340 |
let m_f = find_machine f machines in |
|
1341 |
pp_acsl_cut |
|
1342 |
(pp_ghost |
|
1343 |
(fun fmt () -> |
|
1344 |
fprintf |
|
1345 |
fmt |
|
1346 |
"@;<0 2>@[<v>%a@]" |
|
1347 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon |
|
1348 |
~pp_eol:pp_print_semicolon (pp_c_decl_local_var m)) |
|
1349 |
m_f.mstep.step_outputs)), |
|
1350 |
fun fmt () -> pp_assigns pp_var_decl fmt m_f.mstep.step_outputs |
|
1351 |
| _ -> pp_print_nothing, pp_print_nothing |
|
1352 |
in |
|
1353 |
pp_print_option (pp_proof_annotation m m_c) fmt c; |
|
1354 |
pp_spec_vars fmt (); |
|
1026 | 1355 |
pp_acsl_cut |
1027 | 1356 |
~ghost:m.mis_contract |
1028 | 1357 |
(fun fmt () -> |
1029 | 1358 |
if fst (get_stateless_status m) then |
1030 | 1359 |
fprintf |
1031 | 1360 |
fmt |
1032 |
"%a@,%a@,%a@,%a@,%a" |
|
1361 |
"%a@,%a@,%a@,%a@,%a@,%a"
|
|
1033 | 1362 |
(pp_if_outputs (pp_requires (pp_valid pp_var_decl))) |
1034 | 1363 |
outputs |
1035 | 1364 |
(pp_if_outputs (pp_requires pp_separated'')) |
1036 | 1365 |
outputs |
1366 |
pp_assigns_spec_vars () |
|
1037 | 1367 |
(pp_assigns pp_ptr_decl) |
1038 | 1368 |
outputs |
1039 | 1369 |
(pp_ensures (pp_transition_aux' m)) |
1040 | 1370 |
(name, inputs @ outputs, "", "") |
1041 | 1371 |
pp_spec |
1042 |
spec
|
|
1372 |
c |
|
1043 | 1373 |
else |
1044 | 1374 |
fprintf |
1045 | 1375 |
fmt |
1046 |
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a" |
|
1376 |
"%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a@,%a"
|
|
1047 | 1377 |
(pp_if_outputs (pp_requires (pp_valid pp_var_decl))) |
1048 | 1378 |
outputs |
1049 | 1379 |
(pp_requires pp_mem_valid') |
... | ... | |
1059 | 1389 |
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v))) |
1060 | 1390 |
(name, inputs @ outputs, mem, mem) |
1061 | 1391 |
pp_spec |
1062 |
spec |
|
1392 |
c |
|
1393 |
pp_assigns_spec_vars () |
|
1063 | 1394 |
(pp_assigns pp_ptr_decl) |
1064 | 1395 |
outputs |
1065 | 1396 |
(pp_assigns (pp_reg self)) |
... | ... | |
1131 | 1462 |
|
1132 | 1463 |
let pp_contract fmt machines _self m = |
1133 | 1464 |
match m.mspec.mnode_spec with |
1134 |
| Some (NodeSpec (f, _)) ->
|
|
1465 |
| Some (NodeSpec f) ->
|
|
1135 | 1466 |
let m_f = find_machine f machines in |
1136 |
pp_acsl_cut |
|
1467 |
pp_acsl_line'_cut
|
|
1137 | 1468 |
(pp_ghost |
1138 | 1469 |
(fun fmt () -> |
1139 | 1470 |
fprintf |
1140 | 1471 |
fmt |
1141 |
"@;<0 2>@[<v>%a%a(%a%a);@]" |
|
1142 |
(pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon ~pp_eol:pp_print_semicolon (pp_c_decl_local_var m)) |
|
1143 |
m_f.mstep.step_outputs |
|
1472 |
"%a(%a%a);" |
|
1144 | 1473 |
pp_machine_step_name |
1145 | 1474 |
m_f.mname.node_id |
1146 | 1475 |
(pp_comma_list ~pp_eol:pp_print_comma (pp_c_var_read m)) |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example