Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

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