Merge pull request #1447 from goblint/libfuns-final

Port all remaining library functions
goblint · May 23, 2024 · ac1225a · ac1225a
2 parents aae8d90 + 91eca5a
commit ac1225a
Show file tree

Hide file tree

Showing 4 changed files with 102 additions and 71 deletions.
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
@@ -1344,7 +1344,8 @@
               "zstd",
               "pcre",
               "zlib",
-              "liblzma"
+              "liblzma",
+              "legacy"
             ]
           },
           "default": [
@@ -1355,7 +1356,8 @@
             "glibc",
             "linux-userspace",
             "goblint",
-            "ncurses"
+            "ncurses",
+            "legacy"
           ]
         }
       },

diff --git a/src/util/library/libraryDsl.ml b/src/util/library/libraryDsl.ml
@@ -102,3 +102,5 @@ let f = Access.{ kind = Free; deep = false; }
 let f_deep = Access.{ kind = Free; deep = true; }
 let s = Access.{ kind = Spawn; deep = false; }
 let s_deep = Access.{ kind = Spawn; deep = true; }
+let c = Access.{ kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *)
+let c_deep = Access.{ kind = Spawn; deep = true; }
diff --git a/src/util/library/libraryDsl.mli b/src/util/library/libraryDsl.mli
@@ -71,3 +71,9 @@ val s: LibraryDesc.Access.t
 (** Deep {!AccessKind.Spawn} access.
     Rarely needed. *)
 val s_deep: LibraryDesc.Access.t
+
+(** Shallow {!AccessKind.Spawn} access, substituting function pointer calls for now (TODO). *)
+val c: LibraryDesc.Access.t
+
+(** Deep {!AccessKind.Spawn} access, substituting deep function pointer calls for now (TODO)  *)
+val c_deep: LibraryDesc.Access.t