Project

General

Profile

Revision 3cd040e3 src/options_management.ml

View differences:

src/options_management.ml
97 97
  ]
98 98

  
99 99
let lustrec_options =
100
   common_options @
101
  [ 
102
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
103
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
104
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
105
    "-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>";
106
    "-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
107
    "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
108
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
109
    "-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";
110
    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
111
    "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
112
    "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
113
    "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
114
    "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
115
    "-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
116
    "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
117
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
118
   "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
119
   "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
120
    "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
121
    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
122
    
123
    "-c++" , Arg.Set        cpp      , "c++ backend";
124
    "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
125
    "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
126
    "-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)";
100
  common_options @
101
    [ 
102
      "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
103
      "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
104
      "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
105
      "-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>";
106
      "-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
107
      "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
108
      "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
109
      "-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";
110
      (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
111
      "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
112
      "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
113
      "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
114
      "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
115
      "-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
116
      "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
117
      "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
118
      "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
119
      "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
120
      "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
121
      "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
122
      
123
      "-c++" , Arg.Set        cpp      , "c++ backend";
124
      "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
125
      "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
126
      "-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)";
127
      "-int_div_euclidean", Arg.Set integer_div_euclidean, "interprets integer division as Euclidean (default : C division semantics)";
128
      "-int_div_C", Arg.Clear integer_div_euclidean, "interprets integer division as C division (default)";
127 129

  
128 130
    "-mauve", Arg.String (fun node -> mauve := node; cpp := true; static_mem := false), "generates the mauve code";
129 131
]

Also available in: Unified diff