summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorThomas Bauereiss2017-08-29 17:17:49 +0100
committerThomas Bauereiss2017-08-29 17:47:16 +0100
commit5ec766ceb381f15e6ab4cf568b0f6ab919ca6b68 (patch)
tree2f05bfb585ae26b8ac904850fc378db5427398b9 /src
parent2c3608d421db5978958f010c34e83346ae06fdaa (diff)
Fix bug in rewriting local variable updates
Don't pull out local variables that are introduced inside a sub-block.
Diffstat (limited to 'src')
-rw-r--r--src/rewriter.ml15
1 files changed, 14 insertions, 1 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 4af90f51..eb2a0bdf 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2939,11 +2939,24 @@ let eqidtyp (id1,_) (id2,_) =
let name2 = match id2 with Id_aux ((Id name | DeIid name),_) -> name in
name1 = name2
-let find_updated_vars exp =
+let find_introduced_vars exp =
let lEXP_aux ((ids,lexp),annot) =
let ids = match lexp, annot with
| LEXP_id id, (_, Some (env, _, _)) ->
(match Env.lookup_id id env with
+ | Unbound -> IdSet.add id ids
+ | _ -> ids)
+ | _ -> ids in
+ (ids, LEXP_aux (lexp, annot)) in
+ fst (fold_exp
+ { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
+
+let find_updated_vars exp =
+ let intros = find_introduced_vars exp in
+ let lEXP_aux ((ids,lexp),annot) =
+ let ids = match lexp, annot with
+ | LEXP_id id, (_, Some (env, _, _)) when not (IdSet.mem id intros) ->
+ (match Env.lookup_id id env with
| Local (Mutable, _) -> (id, annot) :: ids
| _ -> ids)
| _ -> ids in