diff --git a/docs/user-guide/annotating.md b/docs/user-guide/annotating.md index 8312869ef9..22419f7036 100644 --- a/docs/user-guide/annotating.md +++ b/docs/user-guide/annotating.md @@ -26,6 +26,7 @@ The following string arguments are supported: 4. `base.non-ptr`/`base.no-non-ptr` to override the `ana.base.context.non-ptr` option. 5. `relation.context`/`relation.no-context` to override the `ana.relation.context` option. 6. `widen`/`no-widen` to override the `ana.context.widen` option. +7. `no-context` to disable context-sensitivity for this function entirely (for all analyses). ### Apron attributes The Apron library can be set to only track variables with the attribute `goblint_apron_track` diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index b972195bad..9acce02b15 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -237,13 +237,22 @@ struct and context man fd x = let man'' = outer_man "context_computation" man in let x = spec_list x in - filter_map (fun (n,(module S:MCPSpec),d) -> - if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*) - None - else - let man' : (S.D.t, S.G.t, S.C.t, S.V.t) man = inner_man "context_computation" man'' n d in - Some (n, Obj.repr @@ S.context man' fd (Obj.obj d)) - ) x + (* Check if this function should be analyzed context-insensitively *) + let no_ctx = + ContextUtil.has_attribute "goblint_context" "no-context" fd.svar.vattr + || ContextUtil.has_option "goblint_context" "no-context" fd + || List.mem fd.svar.vname (get_string_list "ana.context.no_fun") + in + if no_ctx then + startcontext () (* context-insensitive: return a fixed context so all callers share one analysis node *) + else + filter_map (fun (n,(module S:MCPSpec),d) -> + if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*) + None + else + let man' : (S.D.t, S.G.t, S.C.t, S.V.t) man = inner_man "context_computation" man'' n d in + Some (n, Obj.repr @@ S.context man' fd (Obj.obj d)) + ) x and branch (man:(D.t, G.t, C.t, V.t) man) (e:exp) (tv:bool) = let spawns = ref [] in diff --git a/src/config/options.schema.json b/src/config/options.schema.json index c002dfa88e..8b2a2a5123 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1073,6 +1073,13 @@ "description": "Length of the call string that should be used as context for the call_string and/or call_site analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to have an effect, one of the analyses in `callstring.ml` must be activated.", "type": "integer", "default": 2 + }, + "no_fun": { + "title": "ana.context.no_fun", + "description": "List of functions to be analyzed context-insensitively (regardless of other context options).", + "type": "array", + "items": { "type": "string" }, + "default": [] } }, "additionalProperties": false @@ -1821,7 +1828,7 @@ "type": "array", "items": { "type": "string", - "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set", "base.no-bitfield", "base.interval", "base.interval_set", "base.bitfield", "relation.no-context", "relation.context", "no-widen", "widen"] + "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set", "base.no-bitfield", "base.interval", "base.interval_set", "base.bitfield", "relation.no-context", "relation.context", "no-widen", "widen", "no-context"] }, "default": [] } diff --git a/tests/regression/90-context/01-no-context-attribute.c b/tests/regression/90-context/01-no-context-attribute.c new file mode 100644 index 0000000000..5fc73a971b --- /dev/null +++ b/tests/regression/90-context/01-no-context-attribute.c @@ -0,0 +1,16 @@ +// PARAM: --enable ana.int.interval --disable ana.context.widen +#include + +int f(int x) __attribute__((goblint_context("no-context"))); // attributes are not permitted in a function definition +int f(int x) { + if (x) + return f(x+1); + else + return x; +} + +int main () { + int a = f(1); + __goblint_check(!a); // UNKNOWN (intended: context-insensitive due to no-context attribute) + return 0; +} diff --git a/tests/regression/90-context/02-no-context-option.c b/tests/regression/90-context/02-no-context-option.c new file mode 100644 index 0000000000..c14fbe7175 --- /dev/null +++ b/tests/regression/90-context/02-no-context-option.c @@ -0,0 +1,15 @@ +// PARAM: --enable ana.int.interval --disable ana.context.widen --set ana.context.no_fun[+] f +#include + +int f(int x) { + if (x) + return f(x+1); + else + return x; +} + +int main () { + int a = f(1); + __goblint_check(!a); // UNKNOWN (intended: context-insensitive due to ana.context.no_fun option) + return 0; +} diff --git a/tests/regression/90-context/03-no-context-annotation.c b/tests/regression/90-context/03-no-context-annotation.c new file mode 100644 index 0000000000..e4fb7a901c --- /dev/null +++ b/tests/regression/90-context/03-no-context-annotation.c @@ -0,0 +1,15 @@ +// PARAM: --enable ana.int.interval --disable ana.context.widen --set annotation.goblint_context.f[+] no-context +#include + +int f(int x) { + if (x) + return f(x+1); + else + return x; +} + +int main () { + int a = f(1); + __goblint_check(!a); // UNKNOWN (intended: context-insensitive due to annotation option) + return 0; +}