Project

General

Profile

Revision ea1c2906

View differences:

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
    "-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";
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
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
57
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
57 58
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
58 59
    "-horn-queries", 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