Project

General

Profile

Revision 8b3afe43

View differences:

src/c_backend.ml
567 567
    pp_machine_memtype_name m.mname.node_id
568 568
    pp_registers_struct m
569 569
    (Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances
570
    (Utils.pp_final_char_if_non_empty "; " m.minstances) 
570
    (Utils.pp_final_char_if_non_empty "; " m.minstances)
571

  
571 572
(*
572 573
let pp_static_array_instance fmt m (v, m) =
573 574
 fprintf fmt "%s" (mk_addr_var m v)
......
889 890
  (* Print the svn version number and the supported C standard (C90 or C99) *)
890 891
  print_version header_fmt;
891 892
  fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
892
(*
893
  let machine_iter = compute_dep_machines machines in
894
*)
895
  (* Print the struct of all machines. This need to be done following the good
896
     order. *)
893
  (* Print the struct declarations of all machines. *)
897 894
  fprintf header_fmt "/* Struct declarations */@.";
898 895
  List.iter (print_machine_struct header_fmt) machines;
899 896
  pp_print_newline header_fmt ();
900

  
901 897
  (* Print the prototypes of all machines *)
902 898
  fprintf header_fmt "/* Nodes declarations */@.";
903 899
  List.iter (print_machine_decl header_fmt) machines;
src/clock_calculus.ml
100 100
    raise (Error (loc, Clock_extrusion (ck_node, ck)))
101 101

  
102 102
(* Clocks instanciation *)
103
let instanciate_carrier cr inst_cr_vars =
103
let instantiate_carrier cr inst_cr_vars =
104 104
  let cr = carrier_repr cr in
105 105
  match cr.carrier_desc with
106 106
  | Carry_const _
......
119 119
(* inst_ck_vars ensures that a polymorphic variable is instanciated with
120 120
   the same monomorphic variable if it occurs several times in the same
121 121
   type. inst_cr_vars is the same for carriers. *)
122
let rec instanciate inst_ck_vars inst_cr_vars ck =
122
let rec instantiate inst_ck_vars inst_cr_vars ck =
123 123
  match ck.cdesc with
124 124
  | Carrow (ck1,ck2) ->
125 125
      {ck with cdesc =
126
       Carrow ((instanciate inst_ck_vars inst_cr_vars ck1),
127
               (instanciate inst_ck_vars inst_cr_vars ck2))}
126
       Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),
127
               (instantiate inst_ck_vars inst_cr_vars ck2))}
128 128
  | Ctuple cklist ->
129 129
      {ck with cdesc = Ctuple 
130
         (List.map (instanciate inst_ck_vars inst_cr_vars) cklist)}
130
         (List.map (instantiate inst_ck_vars inst_cr_vars) cklist)}
131 131
  | Con (ck',c,l) ->
132
      let c' = instanciate_carrier c inst_cr_vars in
133
      {ck with cdesc = Con ((instanciate inst_ck_vars inst_cr_vars ck'),c',l)}
132
      let c' = instantiate_carrier c inst_cr_vars in
133
      {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}
134 134
  | Cvar _ | Pck_const (_,_) -> ck
135 135
  | Pck_up (ck',k) ->
136
      {ck with cdesc = Pck_up ((instanciate inst_ck_vars inst_cr_vars ck'),k)}
136
      {ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
137 137
  | Pck_down (ck',k) ->
138
      {ck with cdesc = Pck_down ((instanciate inst_ck_vars inst_cr_vars ck'),k)}
138
      {ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
139 139
  | Pck_phase (ck',q) ->
140
      {ck with cdesc = Pck_phase ((instanciate inst_ck_vars inst_cr_vars ck'),q)}
140
      {ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)}
141 141
  | Clink ck' ->
142
      {ck with cdesc = Clink (instanciate inst_ck_vars inst_cr_vars ck')}
142
      {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}
143 143
  | Ccarrying (cr,ck') ->
144
      let cr' = instanciate_carrier cr inst_cr_vars in
144
      let cr' = instantiate_carrier cr inst_cr_vars in
145 145
        {ck with cdesc =
146
         Ccarrying (cr',instanciate inst_ck_vars inst_cr_vars ck')}
146
         Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}
147 147
  | Cunivar cset ->
148 148
      try
149 149
        List.assoc ck.cid !inst_ck_vars
......
512 512
        with Not_found -> 
513 513
	  failwith ("Internal error, variable \""^v^"\" not found")
514 514
      in
515
      let ck = instanciate (ref []) (ref []) ckv in
515
      let ck = instantiate (ref []) (ref []) ckv in
516 516
      expr.expr_clock <- ck;
517 517
      ck
518 518
  | Expr_array elist ->
......
775 775
let clock_prog env decls =
776 776
  List.fold_left (fun e decl -> clock_top_decl e decl) env decls
777 777

  
778
let check_env_compat declared computed =
778
let check_env_compat header declared computed =
779 779
  Env.iter declared (fun k decl_clock_k -> 
780
    let computed_c = Env.lookup_value computed k in
780
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
781 781
    try_unify decl_clock_k computed_c Location.dummy_loc
782 782
  ) 
783 783
(* Local Variables: *)
src/dimension.ml
198 198

  
199 199
let rec normalize dim =
200 200
 dim
201

  
201
(*
202
let rec unnormalize loc l =
203
  let l = List.sort (fun (k, l) (k', l') -> compare l l') (List.map (fun (k, l) -> (k, List.sort compare l)) l) in
204
  match l with
205
  | []   -> mkdim_int loc 0
206
  | t::q -> 
207
 List.fold_left (fun res (k, l) -> mkdim_appl loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q
208
*)
202 209
let copy copy_dim_vars dim =
203 210
  let rec cp dim =
204 211
  match dim.dim_desc with
......
252 259
  | Dvar -> ()
253 260
  | Dunivar -> assert false
254 261

  
255
let rec uneval const univar =
262
let uneval const univar =
256 263
  let univar = repr univar in
257 264
  match univar.dim_desc with
258 265
  | Dunivar -> univar.dim_desc <- Dident const
src/main_lustre_compiler.ml
36 36
    begin
37 37
      try
38 38
	Typing.type_prog env decls
39
    (*Typing.uneval_prog_generics prog*)
40 39
      with (Types.Error (loc,err)) as exc ->
41 40
	Format.eprintf "Typing error at loc %a: %a@]@."
42 41
	  Location.pp_loc loc
......
72 71
  Location.init lexbuf filename;
73 72
  (* Parsing *)
74 73
  report ~level:1 (fun fmt -> fprintf fmt "@[<v>.. parsing header file %s@,@?" filename);
75
  let header = 
76
    try
77
      Parse.prog Parser_lustre.header Lexer_lustre.token lexbuf
78
    with (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 
79
      Parse.report_error err;
80
      raise exc
81
  in
74
  try
75
    Parse.prog Parser_lustre.header Lexer_lustre.token lexbuf
76
  with (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 
77
    Parse.report_error err;
78
    raise exc
79

  
80
let check_lusi header =
82 81
  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)
83 82
  let new_cenv: Clocks.clock_expr Utils.IMap.t = clock_decls Basic_library.clock_env header in   (* Clock calculus *)
84 83
  header, new_tenv, new_cenv
85
  
86 84
    
87 85
let rec compile basename extension =
88 86
  (* Loading the input file *)
......
114 112
      try
115 113
	let basename = s ^ ".lusi" in 
116 114
	report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>Library %s@ " s);
117
	let _, lusi_type_env, lusi_clock_env = load_lusi basename in 
115
	let _, lusi_type_env, lusi_clock_env = check_lusi (load_lusi basename) in 
118 116
	report ~level:1 (fun fmt -> fprintf fmt "@]@,@?");
119 117
	Env.overwrite type_env lusi_type_env,
120 118
	Env.overwrite clock_env lusi_clock_env      
......
172 170
    raise exc
173 171
    end;
174 172
  *)
173

  
174
  (* Checking the existence of a lusi (Lustre Interface file) *)
175
  let lusi_name = basename ^ ".lusi" in
176
  let _ = 
177
    try 
178
      let _ = open_in lusi_name in
179
      let header = load_lusi lusi_name in
180
      let _, declared_types_env, declared_clocks_env = check_lusi header in
181
      (* checking type compatibility with computed types*)
182
      Typing.check_env_compat header declared_types_env computed_types_env;
183
      (* checking clocks compatibilty with computed clocks*)
184
      Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
185
      Typing.uneval_prog_generics prog
186
    with Sys_error _ -> ( 
187
      (* Printing lusi file is necessary *)
188
      report ~level:1 
189
	(fun fmt -> 
190
	  fprintf fmt 
191
	    ".. generating lustre interface file %s@,@?" lusi_name);
192
      let lusi_out = open_out lusi_name in
193
      let lusi_fmt = formatter_of_out_channel lusi_out in
194
      Typing.uneval_prog_generics prog;
195
      Printers.pp_lusi_header lusi_fmt source_name prog
196
    )
197
    | (Types.Error (loc,err)) as exc ->
198
      Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@."
199
	Types.pp_error err;
200
      raise exc
201
  in
202

  
175 203
  (* Computes and stores generic calls for each node,
176 204
     only useful for ANSI C90 compliant generic node compilation *)
177 205
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
......
180 208
  (* Normalization phase *)
181 209
  report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,@?");
182 210
  let normalized_prog = Normalization.normalize_prog prog in
183
  Typing.uneval_prog_generics normalized_prog;
211
  (*Typing.uneval_prog_generics normalized_prog;*)
184 212
  report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Printers.pp_prog normalized_prog);
185 213
  (* Checking array accesses *)
186 214
  if !Options.check then
......
196 224
    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
197 225
    machine_code);
198 226

  
199
  (* Checking the existence of a lusi (Lustre Interface file) *)
200
  let lusi_name = basename ^ ".lusi" in
201
  let _ = 
202
    try 
203
      let _ = open_in lusi_name in
204
      let _, declared_types_env, declared_clocks_env = load_lusi lusi_name in
205
      (* checking type compatibilty with computed types*)
206
      Typing.check_env_compat declared_types_env computed_types_env;
207
      (* checking clocks compatibilty with computed clocks*)
208
      Clock_calculus.check_env_compat declared_clocks_env computed_clocks_env;
209
      
210
    with Sys_error _ -> ( 
211
      (* Printing lusi file is necessary *)
212
      report ~level:1 
213
	(fun fmt -> 
214
	  fprintf fmt 
215
	    ".. generating lustre interface file %s@,@?" lusi_name);
216
      let lusi_out = open_out lusi_name in
217
      let lusi_fmt = formatter_of_out_channel lusi_out in
218
      Printers.pp_lusi_header lusi_fmt source_name normalized_prog
219
    )
220
    | (Types.Error (loc,err)) as exc ->
221
      Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@."
222
	Types.pp_error err;
223
      raise exc
224
  in
225

  
226 227
  (* Printing code *)
227
  let basename    = Filename.basename basename in
228
  let basename    =  Filename.basename basename in
228 229
  let _ = match !Options.output with
229 230
      "C" -> 
230 231
	begin
231
	  let header_file = basename ^ ".h" in (* Could be changed *)
232
	  let source_file = basename ^ ".c" in (* Could be changed *)
233
	  let makefile_file = basename ^ ".makefile" in (* Could be changed *)
232
	  let destname = !Options.dest_dir ^ "/" ^ basename in
233
	  let header_file = destname ^ ".h" in (* Could be changed *)
234
	  let source_file = destname ^ ".c" in (* Could be changed *)
235
	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
234 236
	  let spec_file_opt = if !Options.c_spec then 
235 237
	      (
236 238
		let spec_file = basename ^ "_spec.c" in
......
252 254
	    | Some f -> Some (formatter_of_out_channel (open_out f))
253 255
	  in
254 256
	  report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");
255
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;
257
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code
256 258
	end
257
    | "java" -> begin
258
      failwith "Sorry, but not yet supported !"
259
    | "java" ->
260
      begin
261
	failwith "Sorry, but not yet supported !"
259 262
    (*let source_file = basename ^ ".java" in
260 263
      report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
261 264
      let source_out = open_out source_file in
262 265
      let source_fmt = formatter_of_out_channel source_out in
263 266
      report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
264 267
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
265
    end
266
    | "horn" -> begin
267
      let source_file = basename ^ ".smt2" in (* Could be changed *)
268
      let source_out = open_out source_file in
269
      let fmt = formatter_of_out_channel source_out in
270
      Horn_backend.translate fmt basename normalized_prog machine_code
271
    end
268
      end
269
    | "horn" ->
270
      begin
271
	let source_file = basename ^ ".smt2" in (* Could be changed *)
272
	let source_out = open_out source_file in
273
	let fmt = formatter_of_out_channel source_out in
274
	Horn_backend.translate fmt basename normalized_prog machine_code
275
      end
272 276
    | _ -> assert false
273 277
  in
274 278
  report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
src/options.ml
31 31
let check = ref false
32 32
let c_spec = ref false
33 33
let output = ref "C"
34
let dest_dir = ref ""
34
let dest_dir = ref "."
35 35
let verbose_level = ref 1
36 36
let global_inline = ref false
37 37
let witnesses = ref false
38 38

  
39 39
let options =
40 40
  [ "-d", Arg.Set_string dest_dir,
41
    "produces code in the specified directory";
41
    "produces code in the specified directory (default: .)";
42 42
    "-node", Arg.Set_string main_node, "specifies the main node";
43 43
    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes";
44 44
    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node (default: static)";
45
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default is C99)";
45
    "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant (default: C99)";
46 46
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";
47 47
    "-c-spec", Arg.Set c_spec, 
48 48
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
src/parser_lustre.mly
97 97
%%
98 98

  
99 99
prog:
100
    typ_def_list top_decl_list EOF {$1;(List.rev $2)}
100
 open_list typ_def_list top_decl_list EOF { $1 @ (List.rev $3) }
101 101

  
102 102
header:
103
    typ_def_list top_decl_header_list EOF {$1;(List.rev $2)}
103
 open_list typ_def_list top_decl_header_list EOF { $1 @ (List.rev $3) }
104

  
105
open_list:
106
  { [] }
107
| open_lusi open_list { $1 :: $2 }
108

  
109
open_lusi:
110
  OPEN QUOTE IDENT QUOTE { mktop_decl (Open $3) }
104 111

  
105 112
top_decl_list:
106 113
  top_decl {[$1]}
......
200 207
    in
201 208
    Hashtbl.add node_table $3 nd; nd}
202 209

  
203
| OPEN QUOTE IDENT QUOTE { mktop_decl (Open $3) }
204

  
205 210
nodespec_list:
206 211
NODESPEC { $1 }
207 212
| NODESPEC nodespec_list { LustreSpec.merge_node_annot $1 $2 }
src/printers.ml
48 48
    | Const_tag  t -> pp_print_string fmt t
49 49
    | Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
50 50

  
51
and pp_var fmt id = fprintf fmt "%s: %a" id.var_id Types.print_ty id.var_type
51
and pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type
52

  
53
and pp_node_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type
52 54

  
53 55
and pp_expr fmt expr =
54 56
  match expr.expr_desc with
......
113 115

  
114 116
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq 
115 117

  
116
let pp_node_args = fprintf_list ~sep:"; " pp_var 
118
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
117 119

  
118 120
let pp_var_type_dec fmt ty =
119 121
  let rec pp_var_type_dec_desc fmt tdesc =
......
226 228
  match locals with [] -> () | _ ->
227 229
    fprintf fmt "@[<v 4>var %a@]@ " 
228 230
      (fprintf_list ~sep:"@ " 
229
	 (fun fmt v -> fprintf fmt "%a;" pp_var v))
231
	 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
230 232
      locals
231 233
  ) nd.node_locals
232 234
  (fun fmt checks ->
src/types.ml
96 96
  | Tunivar ->
97 97
    fprintf fmt "'%s" (name_of_type ty.tid)
98 98

  
99
let rec print_node_ty fmt ty =
100
  match ty.tdesc with
101
  | Tint ->
102
    fprintf fmt "int"
103
  | Treal ->
104
    fprintf fmt "real"
105
  | Tbool ->
106
    fprintf fmt "bool"
107
  | Tclock t ->
108
    fprintf fmt "%a clock" print_ty t
109
  | Tstatic (_, t) ->
110
    fprintf fmt "%a" print_node_ty t
111
  | Tconst t ->
112
    fprintf fmt "%s" t
113
  | Trat ->
114
    fprintf fmt "rat"
115
  | Tarrow (ty1,ty2) ->
116
    fprintf fmt "%a->%a" print_ty ty1 print_ty ty2
117
  | Ttuple tylist ->
118
    fprintf fmt "(%a)"
119
      (Utils.fprintf_list ~sep:"*" print_ty) tylist
120
  | Tenum taglist ->
121
    fprintf fmt "(%a)"
122
      (Utils.fprintf_list ~sep:" + " pp_print_string) taglist
123
  | Tarray (e, ty) ->
124
    fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e
125
  | Tlink ty ->
126
      print_ty fmt ty
127
  | Tunivar ->
128
    fprintf fmt "'%s" (name_of_type ty.tid)
129
  | _   -> assert false
130

  
99 131
let pp_error fmt = function
100 132
  | Unbound_value id ->
101 133
    fprintf fmt "Unknown value %s@." id
src/typing.ml
212 212
        t2.tdesc <- Tlink t1
213 213
    | Tarrow (t1,t2), Tarrow (t1',t2') ->
214 214
      begin
215
        unify t1 t1';
216
	unify t2 t2'
215
        semi_unify t1 t1';
216
	semi_unify t2 t2'
217 217
      end
218 218
    | Ttuple tlist1, Ttuple tlist2 ->
219 219
        if (List.length tlist1) <> (List.length tlist2) then
......
237 237
    | Tarray (e1, t1'), Tarray (e2, t2') ->
238 238
      begin
239 239
	semi_unify t1' t2';
240
	Dimension.eval Basic_library.eval_env (fun c -> None) e1;
241
	Dimension.eval Basic_library.eval_env (fun c -> None) e2;
240
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e1;
241
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e2;
242 242
	Dimension.semi_unify e1 e2;
243 243
      end
244 244
    | _,_ -> raise (Unify (t1, t2))
......
252 252
  | Dimension.Unify _ ->
253 253
    raise (Error (loc, Type_clash (ty1,ty2)))
254 254

  
255
let try_semi_unify ty1 ty2 loc =
256
  try
257
    semi_unify ty1 ty2
258
  with
259
  | Unify _ ->
260
    raise (Error (loc, Type_clash (ty1,ty2)))
261
  | Dimension.Unify _ ->
262
    raise (Error (loc, Type_clash (ty1,ty2)))
263

  
255 264
let rec type_const loc c = 
256 265
  match c with
257 266
  | Const_int _ -> Type_predef.type_int
......
516 525
		 expr_annot = None})
517 526
          dummy_id_expr cl
518 527
      in
519
Format.eprintf "yiihii@.";
520 528
      ignore (type_expr env false false when_expr)
521 529

  
522 530
let rec check_type_declaration loc cty =
......
709 717
let uneval_prog_generics prog =
710 718
 List.iter uneval_top_generics prog
711 719

  
712
let check_env_compat declared computed =
720
let check_env_compat header declared computed =
721
  (try 
722
     uneval_prog_generics header
723
   with e -> raise e);
713 724
  Env.iter declared (fun k decl_type_k -> 
714
    let computed_t = Env.lookup_value computed k in
715
    try_unify decl_type_k computed_t Location.dummy_loc
725
    let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
726
    (*Types.print_ty Format.std_formatter decl_type_k;
727
    Types.print_ty Format.std_formatter computed_t;*)
728
    try_semi_unify decl_type_k computed_t Location.dummy_loc
716 729
  ) 
717 730

  
718 731
(* Local Variables: *)
test/src/arrays_arnaud/MatrixAddition.lus
1
#open "dummy_lib"
2

  
1 3
const MatrixAddition_Constant_Value = [ [ 2, 3, 4 ], [ 5, 6, 7 ] ] ;
2 4
const MatrixAddition_Constant1_Value = [ [ 8, 9, 10 ], [ 11, 12, 13 ] ] ;
3 5
const MatrixAddition_Constant2_Value = [ [ 2, 3, 4 ] ] ;
test/src/arrays_arnaud/dummy_lib.lusi
1

  
2
node test(x:int) returns (t:int^2);
3

  
4
function _MatMul_real (
5
	const n, m, p : int ;
6
	in1 : real^n^m ;
7
	in2 : real^m^p)
8
returns (
9
	out : real^n^p) ;
10

  
11
function _Vect_Leqt_real (
12
	const n : int ;
13
	in : real^n ;
14
	in2 : real^n)
15
returns (
16
	out : bool^n) ;
17

  
18
node imp1(const m:int; a:int^(3*m)) returns (c:int^m);
19

  
20
node imp2(const n:int; a:int^n) returns (d:int^n);
test/test-compile.sh
4 4
#LUSTREC="../../_build/src/lustrec"
5 5
LUSTREC=lustrec
6 6
mkdir -p build
7
cd build
8

  
7
build=`pwd`"/build"
9 8
while IFS=, read -r file main opts
10 9
do
11 10
  echo fichier:$file
12 11
#   echo main:$main
13
 #  echo opts:$opts
12
#   echo opts:$opts
14 13
    rm -f witness*
14
    name=`basename "$file" .lus`
15
    dir=`dirname "$file"`
16
    pushd $dir > /dev/null
15 17
    if [ "$main" != "" ]; then
16
        $LUSTREC -d build -verbose 0 $opts -node $main ../$file;
18
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus;
17 19
        if [ $? -ne 0 ]; then
18 20
          rlustrec1="INVALID";
19 21
        else
20 22
          rlustrec1="VALID"
21 23
	fi
22
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
24
	pushd $build > /dev/null
25
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
26
	popd > /dev/null
23 27
        if [ $? -ne 0 ]; then
24 28
          rgcc1="INVALID";
25 29
        else
26 30
          rgcc1="VALID"
27 31
	fi	
28 32
	# Removing Generated lusi file
29
	grep generated ../${file}i > /dev/null
30
	if [ $? -ne 1 ];then
31
	  rm ../${file}i
32
	fi
33
	#grep generated ../${file}i > /dev/null
34
	#if [ $? -ne 1 ];then
35
	#  rm ../${file}i
36
	#fi
33 37
	# Checking inlining
34
	$LUSTREC -d build -verbose 0 $opts -inline -witnesses -node $main ../$file;
38
	$LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
35 39
	if [ $? -ne 0 ]; then
36 40
          rlustrec2="INVALID";
37 41
        else
38 42
          rlustrec2="VALID"
39 43
	fi
40
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
44
	pushd $build > /dev/null
45
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
46
	popd > /dev/null
41 47
        if [ $? -ne 0 ]; then
42 48
          rgcc2="INVALID";
43 49
        else
44 50
          rgcc2="VALID"
45 51
	fi	
46 52
	# Cheching witness
53
	pushd $build > /dev/null
47 54
	lustreh -horn -node check witness.lus 2>/dev/null
55
	popd > /dev/null
48 56
    	z3="`z3 -t:10 witness.smt2 | xargs`"
49 57
    	if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
50 58
	  rinlining="VALID";
......
57 65
	 exit 1
58 66
        fi  
59 67
	# Checking horn backend
60
	$LUSTREC -horn -d build -verbose 0 $opts -node $main ../$file;
61
	echo z3 `basename $file .lus`.smt2 | grep unsat
68
	$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
69
	echo z3 "$name".smt2 | grep unsat
62 70
	# TODO: This part of the script has to be optimized
63
	z3 -t:10 `basename $file .lus`.smt2 | grep unsat > /dev/null
71
	z3 -t:10 "$name".smt2 | grep unsat > /dev/null
64 72
	if [ $? -ne 0 ]; then
65 73
         rhorn="INVALID";
66 74
        else
......
68 76
        fi
69 77
	echo "lustrec ($rlustrec1),gcc($rgcc1),lustrec inline ($rlustrec2), gcc inline ($rgcc2), inlining valid ($rinlining),horn ($rhorn),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
70 78
    else
71
	$LUSTREC -d build -verbose 0 $opts ../$file;
79
	$LUSTREC -d $build -verbose 0 $opts "$name".lus;
72 80
        if [ $? -ne 0 ]; then
73 81
          rlustrec1="INVALID";
74 82
        else
75 83
          rlustrec1="VALID"
76 84
        fi
77
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
85
	pushd $build > /dev/null
86
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
87
	popd > /dev/null
78 88
        if [ $? -ne 0 ]; then
79 89
          rgcc1="INVALID";
80 90
        else
81 91
          rgcc1="VALID"
82 92
        fi
83
	$LUSTREC -horn -d build -verbose 0 $opts ../$file 
93
	$LUSTREC -horn -d $build -verbose 0 $opts ../$file 
84 94
	echo "lustrec ($rlustrec1), gcc($rgcc1), horn($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
85 95
    fi
86
done < ../tests_ok.list
96
    popd > /dev/null
97
done < tests_ok.list

Also available in: Unified diff