Revision c6c8786b
Added by Pierre-Loïc Garoche about 5 years ago
| src/options.ml | ||
|---|---|---|
| 58 | 58 |
let gen_mcdc = ref false |
| 59 | 59 |
let no_mutation_suffix = ref false |
| 60 | 60 |
|
| 61 |
(* Algebraic loops unrolling *) |
|
| 61 | 62 |
let solve_al = ref false |
| 62 | 63 |
let al_nb_max = ref 15 |
| 63 |
|
|
| 64 |
|
|
| 65 |
(* Printer options *) |
|
| 66 |
let kind2_print = ref false |
|
| 67 |
|
|
| 68 |
|
|
| 64 | 69 |
(* Local Variables: *) |
| 65 | 70 |
(* compile-command:"make -C .." *) |
| 66 | 71 |
(* End: *) |
| src/options_management.ml | ||
|---|---|---|
| 92 | 92 |
"-print-clocks", Arg.Set print_clocks, "prints node clocks"; |
| 93 | 93 |
"-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops"; |
| 94 | 94 |
"-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>"; |
| 95 |
"-kind2", Arg.Set kind2_print, "active kind2 output"; |
|
| 95 | 96 |
"-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>"; |
| 96 | 97 |
"-version", Arg.Unit print_version, " displays the version"; |
| 97 | 98 |
] |
| src/printers.ml | ||
|---|---|---|
| 348 | 348 |
stmts = nd.node_stmts @ c.stmts; |
| 349 | 349 |
} |
| 350 | 350 |
) |
| 351 |
|
|
| 351 |
|
|
| 352 |
(* Printing top contract as comments in regular output and as contract |
|
| 353 |
in kind2 *) |
|
| 352 | 354 |
let pp_contract fmt nd = |
| 353 |
|
|
| 354 |
let c = node_as_contract nd in
|
|
| 355 |
fprintf fmt "@[<v 2>(*@contract %s(%a) returns (%a);@ "
|
|
| 355 |
let c = node_as_contract nd in |
|
| 356 |
fprintf fmt "@[<v 2>%scontract %s(%a) returns (%a);@ "
|
|
| 357 |
(if !Options.kind2_print then "" else "(*@")
|
|
| 356 | 358 |
nd.node_id |
| 357 | 359 |
pp_node_args nd.node_inputs |
| 358 | 360 |
pp_node_args nd.node_outputs; |
| 359 | 361 |
fprintf fmt "@[<v 2>let@ "; |
| 360 | 362 |
pp_spec fmt c; |
| 361 |
fprintf fmt "@]@ tel@ @]*)@ " |
|
| 363 |
fprintf fmt "@]@ tel@ @]%s@ " |
|
| 364 |
(if !Options.kind2_print then "" else "*)") |
|
| 362 | 365 |
|
| 363 | 366 |
let pp_spec_as_comment fmt (inl, outl, spec) = |
| 364 | 367 |
match spec with |
Also available in: Unified diff
kind2 output for printer. global option available