Add option sem.atexit.ignore

goblint · Oct 23, 2024 · 4d4de22 · 4d4de22
1 parent 8782650
commit 4d4de22
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 2 deletions.
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
@@ -1544,6 +1544,19 @@
             }
           },
           "additionalProperties": false
+        },
+        "atexit": {
+          "title": "sem.atexit",
+          "type": "object",
+          "properties": {
+            "ignore": {
+              "title": "sem.atexit.ignore",
+              "description": "Ignore atexit callbacks (unsound).",
+              "type": "boolean",
+              "default": false
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false

diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
@@ -145,7 +145,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
-    ("atexit", unknown [drop "function" [s]]);
+    ("atexit", unknown [drop "function" [if_ (fun () -> not (get_bool "sem.atexit.ignore")) s]]);
     ("atoi", unknown [drop "nptr" [r]]);
     ("atol", unknown [drop "nptr" [r]]);
     ("atoll", unknown [drop "nptr" [r]]);

diff --git a/tests/regression/41-stdlib/08-atexit-no-spawn.c b/tests/regression/41-stdlib/08-atexit-no-spawn.c
@@ -1,4 +1,4 @@
-// PARAM: --disable sem.unknown_function.spawn
+// PARAM: --enable sem.atexit.ignore
 #include <stdlib.h>
 #include <goblint.h>