diff --git a/src/analyses/base.ml b/src/analyses/base.ml index a71766d20e..fcb61c8bd0 100644 --- 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 index 1ef73378fb..584b9a528b 100644 --- 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 index c0d3b7158b..8c78ffb62f 100644 --- 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 #include diff --git a/tests/regression/26-undefined_behavior/09-nullpointer-dereference-struct.c b/tests/regression/26-undefined_behavior/09-nullpointer-dereference-struct.c index 3b76cd1ef4..a8804f9b43 100644 --- 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 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 index 959c9183cd..36dbf79a82 100644 --- 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 // source base: // https://stackoverflow.com/questions/4007268/what-exactly-is-meant-by-de-referencing-a-null-pointer