Revision c065827c
src/main_lustre_compiler.ml  

267  267 
let fmt = formatter_of_out_channel source_out in 
268  268 
Horn_backend.translate fmt basename prog machine_code; 
269  269 
(* Tracability file if option is activated *) 
270 
if !Options.horntraces then (


270 
if !Options.traces then ( 

271  271 
let traces_file = destname ^ ".traces" in (* Could be changed *) 
272  272 
let traces_out = open_out traces_file in 
273  273 
let fmt = formatter_of_out_channel traces_out in 
src/normalization.ml  

372  372 
let new_locals = List.filter is_local vars in 
373  373 
(* Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals; *) 
374  374  
375 
(* Compute traceability info: 

376 
 gather newly bound variables 

377 
 compute the associated expression without aliases 

378 
*) 

379 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) new_locals in 

380 
let norm_traceability = { 

381 
annots = List.map (fun v > 

382 
let eq = 

383 
try 

384 
List.find (fun eq > eq.eq_lhs = [v.var_id]) defs 

385 
with Not_found > (Format.eprintf "var not found %s@." v.var_id; assert false) in 

386 
let expr = substitute_expr diff_vars defs eq.eq_rhs in 

387 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 

388 
(["traceability"], pair) 

389 
) diff_vars; 

390 
annot_loc = Location.dummy_loc 

391 
} 

392  
375 
let new_annots = 

376 
if !Options.traces then 

377 
begin 

378 
(* Compute traceability info: 

379 
 gather newly bound variables 

380 
 compute the associated expression without aliases 

381 
*) 

382 
let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) new_locals in 

383 
let norm_traceability = { 

384 
annots = List.map (fun v > 

385 
let eq = 

386 
try 

387 
List.find (fun eq > eq.eq_lhs = [v.var_id]) defs 

388 
with Not_found > (Format.eprintf "var not found %s@." v.var_id; assert false) in 

389 
let expr = substitute_expr diff_vars defs eq.eq_rhs in 

390 
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 

391 
(["traceability"], pair) 

392 
) diff_vars; 

393 
annot_loc = Location.dummy_loc 

394 
} 

395 
in 

396 
norm_traceability::node.node_annot 

397 
end 

398 
else 

399 
node.node_annot 

393  400 
in 
401  
394  402 
let node = 
395  403 
{ node with 
396  404 
node_locals = new_locals; 
397  405 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 
398  406 
node_asserts = asserts; 
399 
node_annot = norm_traceability::node.node_annot;


407 
node_annot = new_annots;


400  408 
} 
401  409 
in ((*Printers.pp_node Format.err_formatter node;*) 
402  410 
node 
src/options.ml  

33  33 
let optimization = ref 2 
34  34 
let lusi = ref false 
35  35 
let print_reuse = ref false 
36 
let traces = ref false 

36  37  
37  38 
let horntraces = ref false 
38  39 
let horn_cex = ref false 
...  ...  
53  54 
"cspec", Arg.Unit (fun () > spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend"; 
54  55 
"java", Arg.Unit (fun () > output := "java"), "generates Java output instead of C"; 
55  56 
"horn", Arg.Unit (fun () > output := "horn"), "generates Horn clauses encoding output instead of C"; 
56 
"horntraces", Arg.Unit (fun () > output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";


57 
"horntraces", Arg.Unit (fun () > output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend."; 

57  58 
"horncex", Arg.Unit (fun () > output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)"; 
58  59 
"hornqueries", Arg.Unit (fun () > output := "horn"; horn_queries:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)"; 
59  60 
"print_reuse", Arg.Set print_reuse, "prints variable reuse policy"; 
Also available in: Unified diff