Project

General

Profile

Revision 3ca6d126

View differences:

src/backends/Horn/horn_backend.ml
564 564

  
565 565
let translate fmt basename prog machines =
566 566
  List.iter (print_machine machines fmt) (List.rev machines);
567

  
568 567
  main_print machines fmt
569 568

  
570 569

  
......
579 578
    let traces : (ident * expr) list=
580 579
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
581 580
      let filtered =
582
	List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
581
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
583 582
      in
584 583
      let content = List.map snd filtered in
585 584
      (* Elements are supposed to be a pair (tuple): variable, expression *)
......
620 619
      List.map (fun (p, v) ->
621 620
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
622 621
	let traces = List.assoc machine machines_traces in
623
	if List.mem_assoc v.var_id traces then
622
	if List.mem_assoc v.var_id traces then (
624 623
	  (* We take the expression associated to variable v in the trace info *)
624
	  (* Format.eprintf "Found variable %a in traces: %a@."  pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
625 625
	  p, List.assoc v.var_id traces
626
	else
626
      )
627
	else (
627 628
	  (* We keep the variable as is: we create an expression v *)
629
	  (* Format.eprintf "Unable to found variable %a in traces (%a)@."  pp_var v (Utils.fprintf_list ~sep:", " Format.pp_print_string) (List.map fst traces); *)
628 630
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
631
	)
629 632

  
630 633
      ) (compute_mems m)
631 634
    in
632 635
    let memories_next = (* We remove the topest pre in each expression *)
633 636
      List.map
634
	(fun (prefix, ee) ->
635
	  match ee.expr_desc with
636
	  | Expr_pre e -> prefix, e
637
	  | _ -> Format.eprintf
638
	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
639
	    (Utils.fprintf_list ~sep:","
640
	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
641
	    (List.rev prefix)
642
	    Printers.pp_expr ee;
643
	    assert false)
637
      	(fun (prefix, ee) ->
638
      	  match ee.expr_desc with
639
      	  | Expr_pre e -> prefix, e
640
      	  | _ -> Format.eprintf
641
      	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
642
      	    (Utils.fprintf_list ~sep:","
643
      	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
644
      	    (List.rev prefix)
645
      	    Printers.pp_expr ee;
646
      	    assert false)
644 647
	memories_old
645 648
    in
646 649

  
......
680 683

  
681 684

  
682 685
(* Local Variables: *)
683
(* compile-command:"make -C .." *)
686
(* compile-command:"make -C ../.." *)
684 687
(* End: *)
src/normalization.ml
127 127
	(Clocks.clock_list_of_clock expr.expr_clock) in
128 128
    let new_def =
129 129
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
130
    in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
130
    in
131
    (* Format.eprintf "Checkign def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
132
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
131 133

  
132 134
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
133 135
   and [opt] is true *)
......
383 385
	with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
384 386
      let expr = substitute_expr diff_vars defs eq.eq_rhs in
385 387
      let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
386
      (["horn_backend";"trace"], pair)
387
    ) [] (*diff_vars*);
388
      (["traceability"], pair)
389
    ) diff_vars;
388 390
    annot_loc = Location.dummy_loc
389 391
  }
390 392

  
test/test-compile.sh
135 135
    popd > /dev/null
136 136
	# Cheching witness
137 137
    pushd $build > /dev/null
138
    $LUSTREC -verbose 0 -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
138
    $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
139 139
    popd > /dev/null
140 140
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
141 141
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
169 169
	
170 170
    # Checking horn backend
171 171
    if [ "$main" != "" ]; then
172
	$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
172
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
173 173
    else
174
	$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus
174
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
175 175
    fi
176 176
    if [ $? -ne 0 ]; then
177 177
        rlustrec="INVALID";

Also available in: Unified diff