Add sem.null-pointer.dereference-refine option

goblint · Sep 13, 2023 · ceaf644 · ceaf644
1 parent 85aec69
commit ceaf644
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 2 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -1054,7 +1054,7 @@ struct
            then M.error ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "Must dereference NULL pointer"
            else if AD.may_be_null adr
            then M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer");
-          if AD.may_be_null adr then emit (Events.SplitBranch (n, true));
+          if get_bool "sem.null-pointer.dereference-refine" && AD.may_be_null adr then emit (Events.SplitBranch (n, true));
           AD.map (add_offset_varinfo (convert_offset a emit gs st ofs)) adr
         | _ ->
           M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;

diff --git a/src/util/options.schema.json b/src/util/options.schema.json
@@ -1417,6 +1417,12 @@
               "type": "string",
               "enum": ["assume_top", "assume_none"],
               "default": "assume_none"
+            },
+            "dereference-refine": {
+              "title": "sem.null-pointer.dereference-refine",
+              "description": "Assume not null after first null dereference",
+              "type": "boolean",
+              "default": false
             }
           },
           "additionalProperties": false

diff --git a/tests/regression/08-malloc_null/02-paths-malloc.c b/tests/regression/08-malloc_null/02-paths-malloc.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] malloc_null
+// PARAM: --set ana.activated[+] malloc_null --disable sem.null-pointer.dereference-refine
 #include <stdlib.h>
 #include <stdio.h>
 

diff --git a/tests/regression/26-undefined_behavior/09-nullpointer-dereference-struct.c b/tests/regression/26-undefined_behavior/09-nullpointer-dereference-struct.c
@@ -1,3 +1,4 @@
+// PARAM: --disable sem.null-pointer.dereference-refine
 #include <stdio.h>
 struct person {
   int age;

diff --git a/tests/regression/26-undefined_behavior/12-nullpointer-dereference-array.c b/tests/regression/26-undefined_behavior/12-nullpointer-dereference-array.c
@@ -1,3 +1,4 @@
+// PARAM: --disable sem.null-pointer.dereference-refine
 #include <stdio.h>
 // source base:
 // https://stackoverflow.com/questions/4007268/what-exactly-is-meant-by-de-referencing-a-null-pointer