diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 34fa34e429..f51a23434b 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2226,6 +2226,20 @@ struct in List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown end + | SignalHandler { signal; handler }, _ -> begin + (* extra sync so that we do not analyze new threads with bottom global invariant *) + publish_all man `Thread; + (* Collect the threads. *) + let start_addr = eval_tv ~man man.local handler in + let start_funvars = AD.to_var_may start_addr in + let start_funvars_with_unknown = + if AD.mem Addr.UnknownPtr start_addr then + dummyFunDec.svar :: start_funvars + else + start_funvars + in + List.filter_map (create_thread ~multiple:false None (Some signal)) start_funvars_with_unknown + end | _, _ -> let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml index 862205aad1..07ec5323e7 100644 --- a/src/util/library/libraryDesc.ml +++ b/src/util/library/libraryDesc.ml @@ -87,6 +87,7 @@ type special = | Bounded of { exp: Cil.exp} (** Used to check for bounds for termination analysis. *) | Rand | Once of { once_control: Cil.exp; init_routine: Cil.exp; } + | SignalHandler of { signal: Cil.exp; handler: Cil.exp; } | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 01e0e7801e..99b4dcf0bb 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -180,7 +180,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("remove", unknown [drop "pathname" [r]]); ("raise", unknown [drop "sig" []]); (* safe-ish, we don't handle signal handlers for now *) ("timespec_get", unknown [drop "ts" [w]; drop "base" []]); - ("signal", unknown [drop "signum" []; drop "handler" [s]]); + ("signal", special [__ "signum" []; __ "handler" [s]] @@ fun signal handler -> SignalHandler {signal; handler}); ("va_arg", unknown [drop "ap" [r]; drop "T" []]); ("va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]); ("va_end", unknown [drop "ap" [r_deep]]); @@ -301,7 +301,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("gethostname", unknown [drop "name" [w]; drop "len" []]); ("getpeername", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [r; w]]); ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]); - ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); + ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); (* TODO: SignalHandler special *) ("tcgetattr", unknown [drop "fd" []; drop "termios_p" [w_deep]]); ("tcsetattr", unknown [drop "fd" []; drop "optional_actions" []; drop "termios_p" [r_deep]]); ("access", unknown [drop "pathname" [r]; drop "mode" []]); diff --git a/tests/regression/03-practical/37-signal-sound.c b/tests/regression/03-practical/37-signal-sound.c new file mode 100644 index 0000000000..5c91b8df20 --- /dev/null +++ b/tests/regression/03-practical/37-signal-sound.c @@ -0,0 +1,15 @@ +#include +#include + +int g = 0; + +void handler(int sig) { + g = 1; +} + +int main() { + __goblint_check(g == 0); + signal(SIGTERM, handler); + __goblint_check(g == 0); // UNKNOWN! + return 0; +} diff --git a/tests/regression/03-practical/38-signal-unique.c b/tests/regression/03-practical/38-signal-unique.c new file mode 100644 index 0000000000..7a6646a576 --- /dev/null +++ b/tests/regression/03-practical/38-signal-unique.c @@ -0,0 +1,13 @@ +#include + +int g = 0; + +void handler(int sig) { + g = 1; // NORACE + g = 2; // NORACE +} + +int main() { + signal(SIGTERM, handler); + return 0; +} diff --git a/tests/regression/03-practical/39-signal-arg.c b/tests/regression/03-practical/39-signal-arg.c new file mode 100644 index 0000000000..c2c7d7b7d0 --- /dev/null +++ b/tests/regression/03-practical/39-signal-arg.c @@ -0,0 +1,11 @@ +#include +#include + +void handler(int sig) { + __goblint_check(sig == SIGTERM); +} + +int main() { + signal(SIGTERM, handler); + return 0; +}