Project

General

Profile

Revision c02d255e

View differences:

_oasis
7 7
Plugins:     DevFiles (0.2)
8 8
# , Custom (0.2)
9 9
PreBuildCommand: ./svn_version.sh 
10
PostInstallCommand: mkdir -p /usr/local/include/lustrec; cp include/* /usr/local/include/lustrec/ 
10
PostInstallCommand: mkdir -p $(prefix)/include; cp -rf include $(prefix)/include/lustrec
11 11

  
12 12
Executable lustrec
13 13
  Path:       src
setup.ml
1 1
(* setup.ml generated for the first time by OASIS v0.2.0 *)
2 2

  
3 3
(* OASIS_START *)
4
(* DO NOT EDIT (digest: bfbef9a3c28e55b657d10679aeb14c68) *)
4
(* DO NOT EDIT (digest: 6666f62d55895fd4c2e5dbbf8e9d4998) *)
5 5
(*
6 6
   Regenerated by OASIS v0.2.0
7 7
   Visit http://oasis.forge.ocamlcore.org for more information and
......
5165 5165
                        (("mkdir",
5166 5166
                           [
5167 5167
                              "-p";
5168
                              "/usr/local/include/lustrec;";
5168
                              "$(prefix)/include;";
5169 5169
                              "cp";
5170
                              "include/*";
5171
                              "/usr/local/include/lustrec/"
5170
                              "-rf";
5171
                              "include";
5172
                              "$(prefix)/include/lustrec"
5172 5173
                           ])))
5173 5174
                 ];
5174 5175
               };
src/c_backend.ml
28 28
open Corelang
29 29
open Machine_code
30 30

  
31

  
32 31
(********************************************************************************************)
33 32
(*                     Basic      Printing functions                                        *)
34 33
(********************************************************************************************)
......
92 91
  let rec aux t pp_suffix =
93 92
  match (Types.repr t).Types.tdesc with
94 93
  | Types.Tclock t'       -> aux t' pp_suffix
95
  | Types.Tbool           -> Format.fprintf fmt "_Bool %s%a" var pp_suffix ()
96
  | Types.Treal           -> Format.fprintf fmt "double %s%a" var pp_suffix ()
97
  | Types.Tint            -> Format.fprintf fmt "int %s%a" var pp_suffix ()
94
  | Types.Tbool           -> fprintf fmt "_Bool %s%a" var pp_suffix ()
95
  | Types.Treal           -> fprintf fmt "double %s%a" var pp_suffix ()
96
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
98 97
  | Types.Tarray (d, t')  ->
99
    let pp_suffix' fmt () = Format.fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
98
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
100 99
    aux t' pp_suffix'
101
  | Types.Tstatic (_, t') -> Format.fprintf fmt "const "; aux t' pp_suffix
102
  | Types.Tconst ty       -> Format.fprintf fmt "%s %s" ty var
103
  | Types.Tarrow (_, _)   -> Format.fprintf fmt "void (*%s)()" var
104
  | _                     -> Format.eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false
100
  | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
101
  | Types.Tconst ty       -> fprintf fmt "%s %s" ty var
102
  | Types.Tarrow (_, _)   -> fprintf fmt "void (*%s)()" var
103
  | _                     -> eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false
105 104
  in aux t (fun fmt () -> ())
106 105

  
107 106
let rec pp_c_initialize fmt t = 
......
111 110
  | Types.Tbool -> pp_print_string fmt "0" 
112 111
  | Types.Treal -> pp_print_string fmt "0."
113 112
  | Types.Tarray (d, t') when Dimension.is_dimension_const d ->
114
    Format.fprintf fmt "{%a}"
113
    fprintf fmt "{%a}"
115 114
      (Utils.fprintf_list ~sep:"," (fun fmt _ -> pp_c_initialize fmt t'))
116 115
      (Utils.duplicate 0 (Dimension.size_const_dimension d))
117 116
  | _ -> assert false
......
146 145
  pp_c_type id.var_id fmt id.var_type
147 146

  
148 147
let pp_c_decl_array_mem self fmt id =
149
  Format.fprintf fmt "%a = (%a) (%s->_reg.%s)"
148
  fprintf fmt "%a = (%a) (%s->_reg.%s)"
150 149
    (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
151 150
    (pp_c_type "(*)") id.var_type
152 151
    self
......
169 168
let pp_c_var_read m fmt id =
170 169
  if Types.is_array_type id.var_type
171 170
  then
172
    Format.fprintf fmt "%s" id.var_id
171
    fprintf fmt "%s" id.var_id
173 172
  else
174 173
    if List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs (* id is output *)
175
    then Format.fprintf fmt "*%s" id.var_id
176
    else Format.fprintf fmt "%s" id.var_id
174
    then fprintf fmt "*%s" id.var_id
175
    else fprintf fmt "%s" id.var_id
177 176

  
178 177
(* Addressable value of a variable, the one that is passed around in calls:
179 178
   - if it's not a scalar non-output, then its name is enough
......
183 182
let pp_c_var_write m fmt id =
184 183
  if Types.is_array_type id.var_type
185 184
  then
186
    Format.fprintf fmt "%s" id.var_id
185
    fprintf fmt "%s" id.var_id
187 186
  else
188 187
    if List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs (* id is output *)
189 188
    then
190
      Format.fprintf fmt "%s" id.var_id
189
      fprintf fmt "%s" id.var_id
191 190
    else
192
      Format.fprintf fmt "&%s" id.var_id
191
      fprintf fmt "&%s" id.var_id
193 192

  
194 193
let pp_c_decl_instance_var fmt (name, (node, static)) = 
195
  Format.fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
194
  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
196 195

  
197 196
let pp_c_tag fmt t =
198 197
 pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
......
204 203
    | Const_real r   -> pp_print_string fmt r
205 204
    | Const_float r  -> pp_print_float fmt r
206 205
    | Const_tag t    -> pp_c_tag fmt t
207
    | Const_array ca -> Format.fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_c_const) ca
206
    | Const_array ca -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_c_const) ca
208 207

  
209 208
(* Prints a value expression [v], with internal function calls only.
210 209
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
......
213 212
let rec pp_c_val self pp_var fmt v =
214 213
  match v with
215 214
    | Cst c         -> pp_c_const fmt c
216
    | Array vl      -> Format.fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
217
    | Access (t, i) -> Format.fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
215
    | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
216
    | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
218 217
    | Power (v, n)  -> assert false
219 218
    | LocalVar v    -> pp_var fmt v
220 219
    | StateVar v    ->
221 220
      if Types.is_array_type v.var_type
222
      then Format.fprintf fmt "*%a" pp_var v
223
      else Format.fprintf fmt "%s->_reg.%a" self pp_var v
221
      then fprintf fmt "*%a" pp_var v
222
      else fprintf fmt "%s->_reg.%a" self pp_var v
224 223
    | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
225 224

  
226 225
let pp_c_checks self fmt m =
227
  Utils.fprintf_list ~sep:"" (fun fmt (loc, check) -> Format.fprintf fmt "@[<v>%a@,assert (%a);@]@," Location.pp_c_loc loc (pp_c_val self (pp_c_var_read m)) check) fmt m.mstep.step_checks
226
  Utils.fprintf_list ~sep:"" (fun fmt (loc, check) -> fprintf fmt "@[<v>%a@,assert (%a);@]@," Location.pp_c_loc loc (pp_c_val self (pp_c_var_read m)) check) fmt m.mstep.step_checks
228 227

  
229 228

  
230 229
(********************************************************************************************)
......
269 268
(* Prints a one loop variable suffix for arrays *)
270 269
let pp_loop_var fmt lv =
271 270
 match snd lv with
272
 | LVar v -> Format.fprintf fmt "[%s]" v
273
 | LInt r -> Format.fprintf fmt "[%d]" !r
271
 | LVar v -> fprintf fmt "[%s]" v
272
 | LInt r -> fprintf fmt "[%d]" !r
274 273

  
275 274
(* Prints a suffix of loop variables for arrays *)
276 275
let pp_suffix fmt loop_vars =
......
286 285
 | _               , Fun (n, vl)  ->
287 286
   Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl
288 287
 | _               , _            ->
289
   let pp_var_suffix fmt v = Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
288
   let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
290 289
   pp_c_val self pp_var_suffix fmt value
291 290

  
292 291
(* type_directed assignment: array vs. statically sized type
......
297 296
*)
298 297
let pp_assign m self pp_var fmt var_type var_name value =
299 298
  let depth = expansion_depth value in
300
(*Format.eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)
299
(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)
301 300
  let loop_vars = mk_loop_variables m var_type depth in
302 301
  let reordered_loop_vars = reorder_loop_variables loop_vars in
303 302
  let rec aux fmt vars =
......
305 304
    | [] ->
306 305
      fprintf fmt "%a = %a;" (pp_value_suffix self loop_vars pp_var) var_name (pp_value_suffix self loop_vars pp_var) value
307 306
    | (d, LVar i) :: q ->
308
(*Format.eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
309
      Format.fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
307
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
308
      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
310 309
	i i i Dimension.pp_dimension d i
311 310
	aux q
312 311
    | (d, LInt r) :: q ->
313
(*Format.eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
312
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
314 313
      let szl = Utils.enumerate (Dimension.size_const_dimension d) in
315
      Format.fprintf fmt "@[<v 2>{@,%a@]@,}"
314
      fprintf fmt "@[<v 2>{@,%a@]@,}"
316 315
	(Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux fmt q)) szl
317 316
  in
318 317
  begin
......
324 323
let pp_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) =
325 324
 try (* stateful node instance *)
326 325
   let (n,_) = List.assoc i m.minstances in
327
   Format.fprintf fmt "%s_step (%a%t%a%t%s->%s);"
326
   fprintf fmt "%s_step (%a%t%a%t%s->%s);"
328 327
     (node_name n)
329 328
     (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
330 329
     (Utils.pp_final_char_if_non_empty ", " inputs) 
......
334 333
     i
335 334
 with Not_found -> (* stateless node instance *)
336 335
   let (n,_) = List.assoc i m.mcalls in
337
   Format.fprintf fmt "%s (%a%t%a);"
336
   fprintf fmt "%s (%a%t%a);"
338 337
     (node_name n)
339 338
     (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
340 339
     (Utils.pp_final_char_if_non_empty ", " inputs) 
......
385 384
	(Utils.fprintf_list ~sep:"@," (pp_machine_branch m self)) hl
386 385

  
387 386
and pp_machine_branch m self fmt (t, h) =
388
  Format.fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) h
387
  fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) h
388

  
389

  
390
(**************************************************************************)
391
(*     Printing spec for c *)
392

  
393
(**************************************************************************)
394

  
395

  
396
let pp_econst fmt c = 
397
  match c with
398
    | EConst_int i -> pp_print_int fmt i
399
    | EConst_real r -> pp_print_string fmt r
400
    | EConst_float r -> pp_print_float fmt r
401
    | EConst_bool b -> pp_print_bool fmt b
402
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
403

  
404
let rec pp_eexpr is_output fmt eexpr = 
405
  let pp_eexpr = pp_eexpr is_output in
406
  match eexpr.eexpr_desc with
407
    | EExpr_const c -> pp_econst fmt c
408
    | EExpr_ident id -> 
409
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
410
    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
411
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
412
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
413
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
414
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
415
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
416
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
417
    | EExpr_merge (id, e1, e2) -> 
418
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
419
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
420
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e 
421
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e 
422

  
423

  
424
    (* | EExpr_whennot _ *)
425
    (* | EExpr_uclock _ *)
426
    (* | EExpr_dclock _ *)
427
    (* | EExpr_phclock _ -> assert false *)
428
and pp_eapp is_output fmt id e r =
429
  let pp_eexpr = pp_eexpr is_output in
430
  match r with
431
  | None ->
432
    (match id, e.eexpr_desc with
433
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
434
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
435
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
436
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
437
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
438
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
439
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
440
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
441
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
442
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
443
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
444
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
445
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
446
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
447
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
448
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
449
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
450
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
451
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
452
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
453

  
454
let pp_ensures is_output fmt e =
455
  match e with
456
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e
457
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args
458

  
459
let pp_acsl_spec outputs fmt spec =
460
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
461
  let pp_eexpr = pp_eexpr is_output in
462
  fprintf fmt "@[<v 2>/*@@ ";
463
  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
464
  Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
465
  fprintf fmt "@ ";
466
  (* fprintf fmt "assigns *self%t%a;@ "  *)
467
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
468
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
469
  Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
470
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
471
      name
472
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
473
      (Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
474
  ) fmt spec.behaviors;
475
  fprintf fmt "@]@ */@.";
476
  ()
389 477

  
390 478
(********************************************************************************************)
391 479
(*                      Prototype Printing functions                                        *)
......
567 655
    (match m.mspec with
568 656
      | None -> ()
569 657
      | Some spec -> 
570
	Printers.pp_acsl_spec m.mstep.step_outputs fmt spec
658
	pp_acsl_spec m.mstep.step_outputs fmt spec
571 659
    );
572 660
    fprintf fmt "extern %a;@.@."
573 661
      (print_step_prototype self)
......
772 860

  
773 861
let print_makefile basename nodename fmt =
774 862
  fprintf fmt "GCC=gcc@.";
775
  fprintf fmt "INC=/usr/local/include/lustrec@.";
863
  fprintf fmt "LUSTREC=%s@." Sys.executable_name;
864
  fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));
865
  fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";
776 866
  fprintf fmt "@.";
777 867
  fprintf fmt "%s_%s:@." basename nodename;
778 868
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename;    
779 869
  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/io_frontend.c@.";    
780 870
(*  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@."; *)
781 871
(*  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename*)
782
 fprintf fmt "\t${GCC} -o %s_%s io_frontend.o -lm %s.o@." basename nodename basename
872
 fprintf fmt "\t${GCC} -o %s_%s io_frontend.o -lm %s.o@." basename nodename basename;
873
 fprintf fmt "@.";
874
 fprintf fmt "clean:@.";
875
 fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename
783 876

  
784 877

  
785 878

  
src/corelang.ml
75 75
  | Expr_pre of expr
76 76
  | Expr_when of expr * ident * label
77 77
  | Expr_merge of ident * (label * expr) list
78
  | Expr_appl of ident * expr * (ident * label) option
78
  | Expr_appl of call_t
79 79
  | Expr_uclock of expr * int
80 80
  | Expr_dclock of expr * int
81 81
  | Expr_phclock of expr * rat
82

  
82
 and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)
83 83

  
84 84
type eq =
85 85
    {eq_lhs: ident list;
......
513 513
	| _       -> decl
514 514
    ) prog 
515 515

  
516

  
517

  
518
(************************************************************************)
519
(*        Renaming                                                      *)
520

  
516 521
(* applies the renaming function [fvar] to all variables of expression [expr] *)
517 522
 let rec expr_replace_var fvar expr =
518 523
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
......
571 576
       | _                    -> assert false)
572 577
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
573 578

  
579

  
580
 let rec rename_expr  f_node f_var f_const expr =
581
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
582
 and rename_expr_desc f_node f_var f_const expr_desc =
583
   let re = rename_expr  f_node f_var f_const in
584
   match expr_desc with
585
   | Expr_const _ -> expr_desc
586
   | Expr_ident i -> Expr_ident (f_var i)
587
   | Expr_array el -> Expr_array (List.map re el)
588
   | Expr_access (e1, d) -> Expr_access (re e1, d)
589
   | Expr_power (e1, d) -> Expr_power (re e1, d)
590
   | Expr_tuple el -> Expr_tuple (List.map re el)
591
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
592
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
593
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
594
   | Expr_pre e' -> Expr_pre (re e')
595
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
596
   | Expr_merge (i, hl) -> 
597
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
598
   | Expr_appl (i, e', i') -> 
599
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
600
   | _ -> assert false
601

  
602
 let rename_node_annot f_node f_var f_const expr  =
603
   assert false
604

  
605
 let rename_expr_annot f_node f_var f_const annot =
606
   assert false
607

  
608
let rename_node f_node f_var f_const nd =
609
  let rename_var v = { v with var_id = f_var v.var_id } in
610
  let inputs = List.map rename_var nd.node_inputs in
611
  let outputs = List.map rename_var nd.node_outputs in
612
  let locals = List.map rename_var nd.node_locals in
613
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
614
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
615
  let node_asserts = List.map 
616
    (fun a -> 
617
      { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 
618
    ) nd.node_asserts
619
  in
620
  let eqs = List.map 
621
    (fun eq -> { eq with
622
      eq_lhs = List.map f_var eq.eq_lhs; 
623
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
624
    } ) nd.node_eqs
625
  in
626
  let spec = 
627
    Utils.option_map 
628
      (fun s -> rename_node_annot f_node f_var f_const s) 
629
      nd.node_spec 
630
  in
631
  let annot =
632
    Utils.option_map
633
      (fun s -> rename_expr_annot f_node f_var f_const s) 
634
      nd.node_annot
635
  in
636
  {
637
    node_id = f_node nd.node_id;
638
    node_type = nd.node_type;
639
    node_clock = nd.node_clock;
640
    node_inputs = inputs;
641
    node_outputs = outputs;
642
    node_locals = locals;
643
    node_gencalls = gen_calls;
644
    node_checks = node_checks;
645
    node_asserts = node_asserts;
646
    node_eqs = eqs;
647
    node_spec = spec;
648
    node_annot = annot;
649
  }
650

  
651

  
652
let rename_const f_const c =
653
  { c with const_id = f_const c.const_id }
654
    
655
let rename_prog f_node f_var f_const prog =
656
  List.rev (
657
    List.fold_left (fun accu top ->
658
      (match top.top_decl_desc with
659
      | Node nd -> 
660
	{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
661
      | Consts c -> 
662
	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
663
      | ImportedNode _
664
      | ImportedFun _
665
      | Open _ -> top)
666
      ::accu
667
) [] prog
668
  )
669

  
670
(**********************************************************************)
574 671
(* Pretty printers *)
575 672

  
576 673
let pp_decl_type fmt tdecl =
src/corelang.mli
45 45
type var_decl = LustreSpec.var_decl
46 46

  
47 47
type expr =
48
    {expr_tag: tag; (* Unique identifier *)
49
     expr_desc: expr_desc;
50
     mutable expr_type: Types.type_expr;
51
     mutable expr_clock: Clocks.clock_expr;
52
     mutable expr_delay: Delay.delay_expr;
53
     mutable expr_annot: LustreSpec.expr_annot option;
54
     expr_loc: Location.t}
48
  {expr_tag: tag; (* Unique identifier *)
49
   expr_desc: expr_desc;
50
   mutable expr_type: Types.type_expr;
51
   mutable expr_clock: Clocks.clock_expr;
52
   mutable expr_delay: Delay.delay_expr; (* Used for the initialisation check *)
53
   mutable expr_annot: LustreSpec.expr_annot option; (* Spec *)
54
   expr_loc: Location.t}
55 55

  
56 56
and expr_desc =
57
  | Expr_const of constant
58
  | Expr_ident of ident
59
  | Expr_tuple of expr list
60
  | Expr_ite   of expr * expr * expr
61
  | Expr_arrow of expr * expr
62
  | Expr_fby of expr * expr
63
  | Expr_array of expr list
64
  | Expr_access of expr * Dimension.dim_expr
65
  | Expr_power of expr * Dimension.dim_expr
66
  | Expr_pre of expr
67
  | Expr_when of expr * ident * label
68
  | Expr_merge of ident * (label * expr) list
69
  | Expr_appl of ident * expr * (ident * label) option
70
  | Expr_uclock of expr * int
71
  | Expr_dclock of expr * int
72
  | Expr_phclock of expr * rat
57
| Expr_const of constant
58
| Expr_ident of ident
59
| Expr_tuple of expr list
60
| Expr_ite   of expr * expr * expr
61
| Expr_arrow of expr * expr
62
| Expr_fby of expr * expr
63
| Expr_array of expr list
64
| Expr_access of expr * Dimension.dim_expr (* acces(e,i) is the i-th element 
65
					      of array epxression e *)
66
| Expr_power of expr * Dimension.dim_expr (* power(e,n) is the array of 
67
					     size n filled with expression e *)
68
| Expr_pre of expr
69
| Expr_when of expr * ident * label
70
| Expr_merge of ident * (label * expr) list
71
| Expr_appl of call_t
72
| Expr_uclock of expr * int
73
| Expr_dclock of expr * int
74
| Expr_phclock of expr * rat
75
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)
73 76

  
74 77
type assert_t = 
75 78
    {
......
223 226
val expr_replace_var: (ident -> ident) -> expr -> expr
224 227
val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
225 228

  
229
(** rename_prog f_node f_var f_const prog *)
230
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
231

  
226 232
val update_expr_annot: expr -> LustreSpec.expr_annot -> expr
227 233

  
228 234

  
src/dimension.ml
367 367
  | Dident id1, Dident id2 when id1 = id2 -> ()
368 368
  | _ -> raise (Unify (dim1, dim2))
369 369

  
370
let rec expr_replace_var fvar e = 
371
 { e with dim_desc = expr_replace_desc fvar e.dim_desc }
372
and expr_replace_desc fvar e =
373
  let re = expr_replace_var fvar in
374
  match e with
375
  | Dvar
376
  | Dunivar
377
  | Dbool _
378
  | Dint _ -> e
379
  | Dident v -> Dident (fvar v)
380
  | Dappl (id, el) -> Dappl (id, List.map re el)
381
  | Dite (g,t,e) -> Dite (re g, re t, re e)
382
  | Dlink e -> Dlink (re e)
src/lustreSpec.ml
68 68
  | EExpr_tuple of eexpr list
69 69
  | EExpr_arrow of eexpr * eexpr
70 70
  | EExpr_fby of eexpr * eexpr
71
  | EExpr_concat of eexpr * eexpr
72
  | EExpr_tail of eexpr
71
  (* | EExpr_concat of eexpr * eexpr *)
72
  (* | EExpr_tail of eexpr *)
73 73
  | EExpr_pre of eexpr
74 74
  | EExpr_when of eexpr * ident
75
  | EExpr_whennot of eexpr * ident
75
  (* | EExpr_whennot of eexpr * ident *)
76 76
  | EExpr_merge of ident * eexpr * eexpr
77 77
  | EExpr_appl of ident * eexpr * ident option
78
  | EExpr_uclock of eexpr * int
79
  | EExpr_dclock of eexpr * int
80
  | EExpr_phclock of eexpr * rat
78
  (* | EExpr_uclock of eexpr * int *)
79
  (* | EExpr_dclock of eexpr * int *)
80
  (* | EExpr_phclock of eexpr * rat *)
81 81
  | EExpr_exists of var_decl list * eexpr
82 82
  | EExpr_forall of var_decl list * eexpr
83 83

  
src/main_lustre_compiler.ml
137 137
  (* Clock calculus *)
138 138
  let computed_clocks_env = clock_decls clock_env prog in
139 139

  
140
  (* Perform global inlining *)
141
  let prog =
142
    if !Options.global_inline && 
143
      (match !Options.main_node with | "" -> false | _ -> true) then
144
      Inliner.global_inline prog type_env clock_env
145
    else
146
      prog
147
  in
148

  
140 149
  (* Delay calculus *)
141 150
  (*
142 151
    if(!Options.delay_calculus)
src/options.ml
33 33
let java = ref false
34 34
let dest_dir = ref ""
35 35
let verbose_level = ref 1
36
let global_inline = ref false
37
let witnesses = ref false
36 38

  
37 39
let options =
38 40
  [ "-d", Arg.Set_string dest_dir,
......
45 47
    "-c-spec", Arg.Set c_spec, 
46 48
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
47 49
    "-java", Arg.Set java, "generates Java output instead of C";
50
    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
51
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
48 52
    "-print_types", Arg.Set print_types, "prints node types";
49 53
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
50 54
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
src/parserLustreSpec.mly
102 102
    {mkeexpr (EExpr_arrow ($1,$3))}
103 103
| expr FBY expr 
104 104
    {mkeexpr (EExpr_fby ($1,$3))}
105
| expr COLCOL expr 
106
    {mkeexpr (EExpr_concat ($1,$3))} 
107
| TAIL LPAR expr RPAR
108
    {mkeexpr (EExpr_tail $3)}
109 105
| expr WHEN IDENT 
110 106
    {mkeexpr (EExpr_when ($1,$3))}
111
| expr WHENNOT IDENT
112
    {mkeexpr (EExpr_whennot ($1,$3))}
113 107
| MERGE LPAR IDENT COMMA expr COMMA expr RPAR
114 108
    {mkeexpr (EExpr_merge ($3,$5,$7))}
115 109
| IDENT LPAR expr RPAR
src/printers.ml
60 60
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
61 61
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
62 62
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
63
    | Expr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_expr e1 pp_expr e2
63
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
64 64
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
65 65
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
66 66
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
......
101 101
    | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
102 102
    | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
103 103
    | "not", _ -> fprintf fmt "(not %a)" pp_expr e
104
    | _ -> fprintf fmt "%s (%a)" id pp_expr e)
104
    | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
105
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
106
)
105 107
  | Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x 
106 108
	
107 109
let pp_node_eq fmt eq = 
......
138 140
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
139 141
(*   ) *)
140 142

  
143

  
144
let pp_econst fmt c = 
145
  match c with
146
    | EConst_int i -> pp_print_int fmt i
147
    | EConst_real r -> pp_print_string fmt r
148
    | EConst_float r -> pp_print_float fmt r
149
    | EConst_bool b -> pp_print_bool fmt b
150
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
151

  
152
let rec pp_eexpr fmt eexpr = 
153
  match eexpr.eexpr_desc with
154
    | EExpr_const c -> pp_econst fmt c
155
    | EExpr_ident id -> pp_print_string fmt id
156
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
157
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
158
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
159
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
160
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
161
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
162
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
163
    | EExpr_merge (id, e1, e2) -> 
164
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
165
    | EExpr_appl (id, e, r) -> pp_eapp fmt id e r
166
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
167
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
168

  
169

  
170
    (* | EExpr_whennot _ *)
171
    (* | EExpr_uclock _ *)
172
    (* | EExpr_dclock _ *)
173
    (* | EExpr_phclock _ -> assert false *)
174
and pp_eapp fmt id e r =
175
  match r with
176
  | None ->
177
    (match id, e.eexpr_desc with
178
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
179
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
180
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
181
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
182
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
183
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
184
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
185
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
186
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
187
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
188
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
189
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
190
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
191
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
192
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
193
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
194
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
195
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
196
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
197
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
198

  
199
  
200
let pp_ensures fmt e =
201
  match e with
202
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e
203
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args
204
 
205
let pp_spec fmt spec =
206
  fprintf fmt "@[<hov 2>(*@@ ";
207
  fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
208
  fprintf_list ~sep:"" pp_ensures fmt spec.ensures;
209
  fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
210
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
211
      name
212
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
213
      (fprintf_list ~sep:"@ " pp_ensures) requires
214
  ) fmt spec.behaviors;
215
  fprintf fmt "@]*)";
216
  ()
217

  
141 218
let pp_node fmt nd = 
142
fprintf fmt "@[<v>node %s (%a) returns (%a)@ %a%alet@ @[<h 2>   @ @[%a@]@ @]@ tel@]@ "
219
fprintf fmt "@[<v 0>%a%tnode %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[%a@]@ @]@.tel@]@."
220
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
221
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.") 
143 222
  nd.node_id
144 223
  pp_node_args nd.node_inputs
145 224
  pp_node_args nd.node_outputs
......
212 291
      pp_node_args nd.node_outputs
213 292
  | ImportedNode _ | ImportedFun _ | Consts _ | Open _ -> ()
214 293

  
215
let pp_econst fmt c = 
216
  match c with
217
    | EConst_int i -> pp_print_int fmt i
218
    | EConst_real r -> pp_print_string fmt r
219
    | EConst_float r -> pp_print_float fmt r
220
    | EConst_bool b -> pp_print_bool fmt b
221
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
222 294

  
223
let rec pp_eexpr is_output fmt eexpr = 
224
  let pp_eexpr = pp_eexpr is_output in
225
  match eexpr.eexpr_desc with
226
    | EExpr_const c -> pp_econst fmt c
227
    | EExpr_ident id -> 
228
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
229
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
230
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
231
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
232
    | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2
233
    | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e
234
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
235
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
236
    | EExpr_merge (id, e1, e2) -> 
237
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
238
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
239
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
240
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
241

  
242

  
243
    | EExpr_whennot _
244
    | EExpr_uclock _
245
    | EExpr_dclock _
246
    | EExpr_phclock _ -> assert false
247
and pp_eapp is_output fmt id e r =
248
  let pp_eexpr = pp_eexpr is_output in
249
  match r with
250
  | None ->
251
    (match id, e.eexpr_desc with
252
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
253
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
254
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
255
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
256
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
257
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
258
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
259
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
260
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
261
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
262
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
263
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
264
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
265
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
266
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
267
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
268
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
269
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
270
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
271
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
272

  
273
  
274
let pp_ensures is_output fmt e =
275
  let pp_eexpr = pp_eexpr is_output in
276
  match e with
277
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e
278
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args
279
 
280
let pp_acsl_spec outputs fmt spec =
281
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
282
  let pp_eexpr = pp_eexpr is_output in
283
  fprintf fmt "@[<v 2>/*@@ ";
284
  fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
285
  fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
286
  fprintf fmt "@ ";
287
  (* fprintf fmt "assigns *self%t%a;@ "  *)
288
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
289
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
290
  fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
291
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
292
      name
293
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
294
      (fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
295
  ) fmt spec.behaviors;
296
  fprintf fmt "@]@ */@.";
297
  ()
298 295

  
299 296

  
300 297
let pp_lusi_header fmt filename prog =
src/typing.ml
287 287
  ty_res
288 288

  
289 289
(* emulates a subtyping relation between types t and (d : t),
290
   used during node application only *)
290
   used during node applications and assignments *)
291 291
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
292 292
  let loc = real_arg.expr_loc in
293 293
  let const = const || (Types.get_static_value formal_type <> None) in
......
486 486
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
487 487
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
488 488
     to a (always non-constant) lhs variable *)
489
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
489
  let tins = type_list_of_type ty_lhs in
490
  let args = expr_list_of_expr eq.eq_rhs in
491
  List.iter2 (type_subtyping_arg env in_main false) args tins;
490 492
  undefined_vars
491 493

  
492 494

  
......
632 634

  
633 635
let type_top_decl env decl =
634 636
  match decl.top_decl_desc with
635
  | Node nd ->
636
      type_node env nd decl.top_decl_loc
637
  | Node nd -> (
638
      try
639
	type_node env nd decl.top_decl_loc
640
      with Error (loc, err) as exc -> (
641
	if !Options.global_inline then
642
	  Format.eprintf "Type error: failing node@.%a@.@?"
643
	    Printers.pp_node nd
644
	;
645
	raise exc)
646
  )
637 647
  | ImportedNode nd ->
638 648
      type_imported_node env nd decl.top_decl_loc
639 649
  | ImportedFun nd ->
src/utils.ml
44 44

  
45 45
module ISet = Set.Make(IdentModule)
46 46

  
47
let desome x = match x with Some x -> x | None -> failwith "desome"
48

  
47 49
let option_map f o =
48 50
  match o with
49 51
  | None   -> None
test/Makefile
6 6

  
7 7
clean:
8 8
	@rm -rf build
9
	@for i in `find . -iname *.lusi`; do grep generated $$i > /dev/null; if [ $$? -eq 0 ]; then rm $$i; fi; done
9 10

  
10 11
distclean: clean
11 12
	@rm -rf report*
test/test-compile.sh
1 1
#!/bin/bash
2 2

  
3 3
NOW=`date "+%y%m%d%H%M"`
4
LUSTREC="../../_build/src/lustrec"
4
#LUSTREC="../../_build/src/lustrec"
5
LUSTREC=lustrec
5 6
mkdir -p build
6 7
cd build
7 8

  
8 9
while IFS=, read -r file main opts
9 10
do
10
#   echo fichier:$file
11
  echo fichier:$file
11 12
#   echo main:$main
12
#   echo opts:$opts
13
 #  echo opts:$opts
14
   rm -f witness*
13 15
    if [ "$main" != "" ]; then
14
	$LUSTREC -d build -verbose 0 $opts -node $main ../$file;
16
	$LUSTREC -d build -verbose 0 $opts -inline -witnesses -node $main ../$file;
15 17
    else
16 18
	$LUSTREC -d build -verbose 0 $opts ../$file
17 19
    fi
......
20 22
    else 
21 23
      rlustrec="VALID" 
22 24
    fi
23
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
24
    if [ $? -ne 0 ]; then
25
      rgcc="INVALID";
25
  #  echo "horn encoding: lustreh -horn -node check witness.lus 2>/dev/nul"
26
    lustreh -horn -node check witness.lus 2>/dev/null
27
    #    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
28
   # echo "Calling z3: "
29
    z3="`z3 -t:10 witness.smt2 | xargs`"
30
    #echo "Test: $z3"
31
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
32
      rz3="VALID";
33
    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
34
      rz3="ERROR";
35
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
36
      rz3="UNKNOWN";
26 37
    else
27
      rgcc="VALID"
38
      rz3="INVALID"
39
      exit 1
28 40
    fi    
29
    echo "lustrec ($rlustrec),gcc ($rgcc),diff with ref ($rdiff),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep INVALID
41
    echo "lustrec ($rlustrec),inlining valid ($rz3),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
30 42
# awk 'BEGIN { FS = "\" " } ; { printf "%-20s %-40s\n", $1, $2, $3}' 
31
done < ../tests_ok.list
43
done < ../tests_ok.nolarge.list

Also available in: Unified diff