Revision a56f563e
Added by Lélio Brun over 3 years ago
| src/machine_code_common.ml | ||
|---|---|---|
| 344 | 344 |
| Some (Contract spec) -> |
| 345 | 345 |
pp_mspec m fmt spec) |
| 346 | 346 |
(pp_memory_packs m) |
| 347 |
m.mspec.mmemory_packs
|
|
| 347 |
(snd m.mspec.mmemory_packs)
|
|
| 348 | 348 |
(pp_transitions m) |
| 349 | 349 |
m.mspec.mtransitions |
| 350 | 350 |
(pp_print_list Printers.pp_expr_annot) |
| ... | ... | |
| 449 | 449 |
]; |
| 450 | 450 |
step_asserts = []; |
| 451 | 451 |
}; |
| 452 |
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
|
|
| 452 |
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = -1, [] };
|
|
| 453 | 453 |
mannot = []; |
| 454 | 454 |
msch = None; |
| 455 | 455 |
mis_contract = false; |
| ... | ... | |
| 492 | 492 |
step_instrs = []; |
| 493 | 493 |
step_asserts = []; |
| 494 | 494 |
}; |
| 495 |
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
|
|
| 495 |
mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = -1, [] };
|
|
| 496 | 496 |
mannot = []; |
| 497 | 497 |
msch = None; |
| 498 | 498 |
mis_contract = false; |
Also available in: Unified diff
more compact assign clauses for state variables, and remove useless memory pack predicates and assertions