Project

General

Profile

« Previous | Next » 

Revision 57f27fe1

Added by Pierre-Loïc Garoche about 6 years ago

Bug solved: issues when generation traceability annotation in normalization

View differences:

src/backends/Horn/horn_backend.ml
12 12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13 13
   Kahsai, HCSV'14.
14 14

  
15
   This is a modified version that handle reset
15
   This is a modified version that handles reset and automaton
16 16
*)
17 17

  
18 18
open Format
src/normalization.ml
379 379
	  annots = List.map (fun v ->
380 380
	    let eq =
381 381
	      try
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs) 
383
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
382
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
383
	      with Not_found -> 
384
		(
385
		  Format.eprintf "Traceability annotation generation: var %s not found@.Eqs: " v.var_id; 
386
		  assert false
387
		) 
388
	    in
384 389
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
385 390
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
386 391
	    (["traceability"], pair)

Also available in: Unified diff