Do not swallow dead code and add example

Author: michael-schwarz

src/analyses/baseInvariant.ml

@@ -102,7 +102,7 @@ struct
       )
     | Mem (Lval lv), NoOffset ->
       let lvals = eval_lv ~man st x in
-      let res = AD.fold (fun a acc -> 
+      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
@@ -111,14 +111,18 @@ struct
           (* 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 
+          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
+          )
+        ) lvals (D.bot ())
+      in
+      if D.is_bot res then
+        raise Analyses.Deadcode
+      else
+        res
     | Var _, _
     | Mem _, _ ->
       (* For accesses via pointers, not yet *)

tests/regression/27-inv_invariants/25-deadcode.c

@@ -0,0 +1,27 @@
+// PARAM: --enable ana.int.interval
+
+int two = 2;
+int three = 5;
+
+int main() {
+	int* ptr;
+	int top;
+
+	int indicator = 1;
+
+	if(top) {
+		ptr = &two;
+	} else {
+		ptr = &three;
+	}
+
+	// Evaluating this in the interval domain yields [2,5]
+	// Only trying to optimize per-pointer discovers that this in fact dead code (https://github.com/goblint/analyzer/pull/1659)
+	if(*ptr == 3) {
+		// Dead
+		indicator = 0;
+	}
+
+	__goblint_check(indicator == 1);
+  	return 0;
+}