Merge pull request #1982 from goblint/refine-pointer-by-pointee-option

Add option `ana.base.branch.refine-pointer-by-pointee`

Author: sim642

conf/examples/large-program.json

@@ -7,6 +7,9 @@
         "privatization": "none",
         "context": {
           "non-ptr": false
+        },
+        "branch": {
+          "refine-pointer-by-pointee": false
         }
       },
       "thread": {

src/analyses/baseInvariant.ml

@@ -112,7 +112,7 @@ struct
         if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r;
         r
       )
-    | Mem (Lval lv), off ->
+    | Mem (Lval lv), off when GobConfig.get_bool "ana.base.branch.refine-pointer-by-pointee" ->
       (* Underlying lvals (may have offsets themselves), e.g., for struct members NOT including any offset appended to outer Mem *)
       let lvals = eval_lv ~man st (Mem (Lval lv), NoOffset) in
       (* Additional offset of value being refined in Addr Offset type *)

src/config/options.schema.json

@@ -886,6 +886,19 @@
                 }
               },
               "additionalProperties": false
+            },
+            "branch": {
+              "title": "ana.base.branch",
+              "type": "object",
+              "properties": {
+                "refine-pointer-by-pointee": {
+                  "title": "ana.base.branch.refine-pointer-by-pointee",
+                  "description": "Refine points-to sets by dereferenced value when branching.",
+                  "type": "boolean",
+                  "default": true
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false