Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/options.ml | ||
---|---|---|
36 | 36 |
let global_inline = ref false |
37 | 37 |
let witnesses = ref false |
38 | 38 |
let optimization = ref 2 |
39 |
let horntraces = ref false |
|
40 |
let horn_queries = ref false |
|
39 | 41 |
|
40 | 42 |
let options = |
41 | 43 |
[ "-d", Arg.Set_string dest_dir, |
... | ... | |
51 | 53 |
"-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"; |
52 | 54 |
"-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; |
53 | 55 |
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C"; |
56 |
"-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend."; |
|
57 |
"-horn-queries", Arg.Set horn_queries, "add the queries instructions at the end of the generated horn files"; |
|
54 | 58 |
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations"; |
55 | 59 |
"-inline", Arg.Set global_inline, "inline all node calls (require a main node)"; |
56 | 60 |
"-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation"; |
Also available in: Unified diff
Merged horn_traces branch