Stuff

Author: sim642

src/analyses/varEq.ml

@@ -327,10 +327,18 @@ struct
 
   (* Remove elements, that would change if the given lval would change.*)
   let remove_exp ask (e:exp) (st:D.t) : D.t =
+    let r =
     D.filter (fun x -> not (may_change ask e x)) st
+    in
+    ignore (Pretty.printf "remove_exp %a %a = %a\n" CilType.Exp.pretty e D.pretty st D.pretty r);
+    r
 
   let remove ask (e:lval) (st:D.t) : D.t =
+    let r =
     remove_exp ask (mkAddrOf e) st
+    in
+    ignore (Pretty.printf "remove %a %a = %a\n" CilType.Lval.pretty e D.pretty st D.pretty r);
+    r
     (*
     let not_in v xs = not (Exp.contains_var v xs) in
     let remove_simple (v,offs) st =
@@ -402,11 +410,16 @@ struct
       | None -> None
       | Some st ->
         let vs = ask.f (Queries.ReachableFrom e) in
-        Some (Queries.LS.join vs st)
+        if Queries.LS.is_top vs then
+          None
+        else
+          Some (Queries.LS.join vs st)
     in
     List.fold_right reachable es (Some (Queries.LS.empty ()))
 
   let rec reachable_from (r:Queries.LS.t) e =
+    ignore (Pretty.printf "reachable_from %a %a\n" Queries.LS.pretty r CilType.Exp.pretty e);
+    let r2 =
     if Queries.LS.is_top r then true else
       let rec is_prefix x1 x2 =
         match x1, x2 with
@@ -440,6 +453,9 @@ struct
       | CastE (_,e)           -> reachable_from r e
       | Question _ -> failwith "Logical operations should be compiled away by CIL."
       | _ -> failwith "Unmatched pattern."
+  in
+  ignore (Pretty.printf "reachable_from %a %a = %B\n" Queries.LS.pretty r CilType.Exp.pretty e r2);
+  r2
 
   (* Probably ok as is. *)
   let body ctx f = ctx.local
@@ -489,13 +505,19 @@ struct
     match reachables (Analyses.ask_of_ctx ctx) es with
     | None -> D.top ()
     | Some rs ->
-      let remove_reachable1 es st =
+      ignore (Pretty.printf "reachables %a: %a\n" (d_list ", " CilType.Exp.pretty) es Queries.LS.pretty rs);
+      (* let remove_reachable1 es st =
         let remove_reachable2 e st =
-          if reachable_from rs e && not (isConstant e) then remove_exp (Analyses.ask_of_ctx ctx) e st else st
+          ignore (Pretty.printf "remove_reachable2 %a %a\n" CilType.Exp.pretty e D.pretty st);
+          if reachable_from rs e && not (isConstant e) then
+            remove_exp (Analyses.ask_of_ctx ctx) e st
+          else
+            st
         in
         D.B.fold remove_reachable2 es st
       in
-      D.fold remove_reachable1 ctx.local ctx.local
+      D.fold remove_reachable1 ctx.local ctx.local *)
+      List.fold_left (fun st e -> remove_exp (Analyses.ask_of_ctx ctx) e st) ctx.local (Queries.LS.fold (fun lval acc -> mkAddrOf (Lval.CilLval.to_lval lval) :: acc) rs [])
 
   let unknown_fn ctx lval f args =
     let args =