Project

General

Profile

« Previous | Next » 

Revision 7d62bf41

Added by Pierre-Loïc Garoche almost 5 years ago

Merged code

View differences:

src/options.ml
44 44
let const_unfold = ref false
45 45
let mpfr = ref false
46 46
let mpfr_prec = ref 0
47

  
47
  
48 48
let traces = ref false
49 49
let horn_cex = ref false
50 50
let horn_query = ref true
......
53 53

  
54 54
let sfunction = ref ""
55 55

  
56

  
56 57
let set_mpfr prec =
57 58
  if prec > 0 then (
58 59
    mpfr := true;
......
61 62
  )
62 63
  else
63 64
    failwith "mpfr requires a positive integer"
64
			
65

  
66
let set_backend s =
67
  output := "emf";
68
  Backends.setup s
69
  
65 70
let options =
66 71
[ "-d", Arg.Set_string dest_dir,
67 72
"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";
......
77 82
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
78 83
    "-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";
79 84
    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
80
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
81
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
82
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
83
    "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
85
    "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
86
    "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
87
    "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
88
    "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
84 89
    "-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction";
85 90
    "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
86
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
87
    "-emf", Arg.Unit (fun () -> output := "emf"), "generates EMF output, to be used by CocoSim";
91
    "-lustre", Arg.Unit (fun () -> set_backend "lustre"), "generates Lustre output, performing all active optimizations";
92
    "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
88 93
    "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
89 94
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
90 95
    "-print_types", Arg.Set print_types, "prints node types";

Also available in: Unified diff