Project

General

Profile

Revision 3cd040e3

View differences:

src/backends/C/c_backend_common.ml
108 108
let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id
109 109
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
110 110

  
111
let pp_mod pp_val v1 v2 fmt =
112
  if !Options.integer_div_euclidean then
113
    (* (a mod_C b) + (a < 0 ? abs(b) : 0) *)
114
    Format.fprintf fmt "((%a %% %a) + (%a < 0?(abs(%a)):0))"
115
      pp_val v1 pp_val v2
116
      pp_val v1 pp_val v2
117
  else (* Regular behavior: printing a % *)
118
    Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
119

  
120
let pp_div pp_val v1 v2 fmt =
121
  if !Options.integer_div_euclidean then
122
    (* (a - ((a mod_C b) + (a < 0 ? abs(b) : 0))) div_C b *)
123
    Format.fprintf fmt "(%a - ((%a %% %a) + (%a < 0 ? abs(%a) : 0))) / %a"
124
      pp_val v1 pp_val v1 pp_val v2
125
      pp_val v1 pp_val v2 pp_val v2
126
  else (* Regular behavior: printing a / *)
127
    Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
128
  
111 129
let pp_basic_lib_fun i pp_val fmt vl =
112 130
  match i, vl with
113 131
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
......
115 133
  | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
116 134
  | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
117 135
  | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
118
  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
136
  | "mod", [v1; v2] ->
137
     let typ = v1.value_type in
138
     if Types.is_int_type v1.value_type then
139
       pp_mod pp_val v1 v2 fmt 
140
     else
141
       Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
119 142
  | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
120 143
  | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
144
  | "/", [v1; v2] ->
145
     if Types.is_int_type v1.value_type then
146
       pp_div pp_val v1 v2 fmt
147
     else
148
       Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
121 149
  | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
122 150
  | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
123 151

  
src/options.ml
35 35
let mpfr_prec = ref 100
36 36
let print_dec_types = ref false
37 37

  
38
(* Option to select the expected behavior of integer division: Euclidian or
39
   C. Default C !!! *)
40
let integer_div_euclidean = ref false
41
  
38 42
let traces = ref false
39 43
let horn_cex = ref false
40 44
let horn_query = ref true
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