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