Consider pointees separately for refinement

Author: michael-schwarz

src/analyses/baseInvariant.ml

@@ -100,6 +100,25 @@ struct
         if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r;
         r
       )
+    | Mem (Lval lv), NoOffset ->
+      let lvals = eval_lv ~man st x in
+      let res = AD.fold (fun a acc -> 
+          if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty (Address (AD.singleton a));
+          let st = set' lv (Address (AD.singleton a)) st in
+          let old_val = get ~man st (AD.singleton a) None in
+          let old_val = VD.cast (Cilfacade.typeOfLval lv) old_val in (* needed as the type of this pointer may be different *)
+          (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *)
+          (* let old_val = eval_rv_lval_refine ~man st exp x in *)
+          let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
+          let v = apply_invariant ~old_val ~new_val:c' in
+          if is_some_bot v then 
+            D.join acc (try contra st with Analyses.Deadcode -> D.bot ())
+          else (
+            if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
+            D.join acc (set' x v st)
+          )   
+        ) lvals (D.bot ()) in
+      res
     | Var _, _
     | Mem _, _ ->
       (* For accesses via pointers, not yet *)

tests/regression/27-inv_invariants/24-ptr.c

@@ -0,0 +1,21 @@
+// PARAM: --enable ana.int.interval
+
+int two = 2;
+int three = 3;
+
+int main() {
+	int* ptr;
+	int top;
+
+	if(top) {
+		ptr = &two;
+	} else {
+		ptr = &three;
+	}
+
+	if(*ptr == 2) {
+		__goblint_check(ptr == &two);
+	}
+
+  	return 0;
+}