Project

General

Profile

Revision c065827c src/options.ml

View differences:

src/options.ml
33 33
let optimization = ref 2
34 34
let lusi = ref false
35 35
let print_reuse = ref false
36
let traces = ref false
36 37

  
37 38
let horntraces = ref false
38 39
let horn_cex = ref false
......
53 54
    "-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";
54 55
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
55 56
    "-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-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
57 58
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
58 59
    "-horn-queries", Arg.Unit (fun () -> output := "horn"; horn_queries:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
59 60
    "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";

Also available in: Unified diff