Revision 01c7d5e1 src/causality.ml
src/causality.ml | ||
---|---|---|
249 | 249 |
mashup_appl_dependencies f e g |
250 | 250 |
| Expr_appl (f, e, Some (r, _)) -> |
251 | 251 |
mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g) |
252 |
| Expr_uclock (e, _) |
|
253 |
| Expr_dclock (e, _) |
|
254 |
| Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g |
|
255 | 252 |
in |
256 | 253 |
let g = |
257 | 254 |
List.fold_left |
... | ... | |
294 | 291 |
| Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2) |
295 | 292 |
| Expr_ite (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e)) |
296 | 293 |
| Expr_pre e |
297 |
| Expr_when (e,_,_) |
|
298 |
| Expr_uclock (e,_) |
|
299 |
| Expr_dclock (e,_) |
|
300 |
| Expr_phclock (e,_) -> get_expr_calls prednode e |
|
294 |
| Expr_when (e,_,_) -> get_expr_calls prednode e |
|
301 | 295 |
| Expr_appl (id,e, _) -> |
302 | 296 |
if not (Basic_library.is_internal_fun id) && prednode id |
303 | 297 |
then ESet.add expr (get_expr_calls prednode e) |
... | ... | |
357 | 351 |
module Cycles = Graph.Components.Make (IdentDepGraph) |
358 | 352 |
|
359 | 353 |
let mk_copy_var n id = |
360 |
mk_new_name (node_vars n) id |
|
354 |
mk_new_name (get_node_vars n) id
|
|
361 | 355 |
|
362 | 356 |
let mk_copy_eq n var = |
363 |
let var_decl = node_var var n in |
|
357 |
let var_decl = get_node_var var n in
|
|
364 | 358 |
let cp_var = mk_copy_var n var in |
365 | 359 |
let expr = |
366 | 360 |
{ expr_tag = Utils.new_tag (); |
Also available in: Unified diff