Revision 6a1a01d2 src/normalization.ml
src/normalization.ml | ||
---|---|---|
65 | 65 |
if List.exists (fun v -> v.var_id = s) vars then aux () else |
66 | 66 |
{ |
67 | 67 |
var_id = s; |
68 |
var_orig = false; |
|
68 | 69 |
var_dec_type = dummy_type_dec; |
69 | 70 |
var_dec_clock = dummy_clock_dec; |
70 | 71 |
var_dec_const = false; |
... | ... | |
371 | 372 |
- compute the associated expression without aliases |
372 | 373 |
*) |
373 | 374 |
let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in |
375 |
let split_defs = Splitting.tuple_split_eq_list defs in |
|
374 | 376 |
let norm_traceability = { |
375 |
annots = |
|
376 |
List.map |
|
377 |
(fun v -> |
|
378 |
let expr = substitute_expr diff_vars defs ( |
|
379 |
let eq = try |
|
380 |
List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs |
|
381 |
with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in |
|
382 |
eq.eq_rhs) in |
|
383 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
|
384 |
["horn_backend";"trace"], pair |
|
385 |
) |
|
386 |
diff_vars ; |
|
377 |
annots = List.map (fun v -> |
|
378 |
let eq = |
|
379 |
try |
|
380 |
List.find (fun eq -> eq.eq_lhs = [v.var_id]) split_defs |
|
381 |
with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in |
|
382 |
let expr = substitute_expr diff_vars split_defs eq.eq_rhs in |
|
383 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
|
384 |
(["horn_backend";"trace"], pair) |
|
385 |
) diff_vars; |
|
387 | 386 |
annot_loc = Location.dummy_loc |
388 | 387 |
} |
389 | 388 |
|
Also available in: Unified diff