Revision f7caf067 src/options.ml
| src/options.ml | ||
|---|---|---|
| 142 | 142 |
"-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>"; |
| 143 | 143 |
"-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend"; |
| 144 | 144 |
(* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *) |
| 145 |
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
|
|
| 146 |
"-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produces traceability file for Horn backend. Enable the horn backend.";
|
|
| 147 |
"-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generates cex enumeration. Enable the horn backend (work in progress)";
|
|
| 148 |
"-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generates queries in generated Horn file. Enable the horn backend (work in progress)";
|
|
| 149 |
"-horn-sfunction", Arg.Set_string sfunction, "gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
|
|
| 145 |
"-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
|
|
| 146 |
"-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
|
|
| 147 |
"-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
|
|
| 148 |
"-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
|
|
| 149 |
"-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
|
|
| 150 | 150 |
"-print-reuse", Arg.Set print_reuse, "prints variable reuse policy"; |
| 151 | 151 |
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations"; |
| 152 |
"-emf", Arg.Unit (fun () -> output := "emf"), "generates EMF output, to be used by CocoSim";
|
|
| 152 |
"-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
|
|
| 153 | 153 |
"-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding"; |
| 154 | 154 |
"-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation"; |
| 155 | 155 |
"-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>"; |
| 156 |
"-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>"; |
|
| 157 | 156 |
|
| 158 | 157 |
"-c++" , Arg.Set cpp , "c++ backend"; |
| 159 | 158 |
"-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")"; |
Also available in: Unified diff