diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index 64c61a8d93..6a42e23de9 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -29,7 +29,7 @@ struct let init _ = collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed"; let activated = get_string_list "ana.activated" in - emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) + emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated || List.mem (ThreadAccess.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) = if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach; diff --git a/src/analyses/threadAccess.ml b/src/analyses/threadAccess.ml new file mode 100644 index 0000000000..8205c7033e --- /dev/null +++ b/src/analyses/threadAccess.ml @@ -0,0 +1,42 @@ +open Analyses + +module Spec = +struct + include UnitAnalysis.Spec + + let name () = "threadAccess" + + module V = + struct + include CilType.Varinfo + let is_write_only _ = false + end + + module G = ConcDomain.ThreadSet + + let query man (type a) (q: a Queries.t): a Queries.result = + match q with + | MayBePublic {global; _} -> + if G.cardinal (man.global global) = 1 then + false + else + Queries.Result.top q + | _ -> Queries.Result.top q + + let event man e oman = + match e with + | Events.Access {ad; _} -> + Queries.AD.iter (function + | Queries.AD.Addr.Addr (v, _) when v.vglob -> + begin match man.ask CurrentThreadId with + | `Lifted tid -> man.sideg v (G.singleton tid) + | _ -> () (* TODO: what here? *) + end + | _ -> () + ) ad + | _ -> + man.local +end + +let _ = + MCP.register_analysis ~dep:["access"] (module Spec : MCPSpec) diff --git a/tests/regression/03-practical/39-signal-effectively-local.c b/tests/regression/03-practical/39-signal-effectively-local.c new file mode 100644 index 0000000000..4b6e681a7f --- /dev/null +++ b/tests/regression/03-practical/39-signal-effectively-local.c @@ -0,0 +1,19 @@ +// PARAM: --set ana.activated[+] threadAccess +#include +#include + +int g = 0; + +void handler(int sig) { +} + +int main() { + __goblint_check(g == 0); + g = 1; + __goblint_check(g == 1); + signal(SIGTERM, handler); + __goblint_check(g == 1); + g = 2; + __goblint_check(g == 2); + return 0; +}