Add missing __VERIFIER_nondet_X()s

lib/sv-comp/stub/src/sv-comp.c

@@ -22,14 +22,23 @@ __VERIFIER_nondet(char)
 __VERIFIER_nondet(int)
 __VERIFIER_nondet(float)
 __VERIFIER_nondet(double)
-// __VERIFIER_nondet(loff_t)
+// loff_t in LibraryFunctions
 __VERIFIER_nondet(long)
 __VERIFIER_nondet2(char*, pchar)
+__VERIFIER_nondet2(char*, charp) // not in rules
+__VERIFIER_nondet2(const char*, const_char_pointer) // not in rules
+__VERIFIER_nondet2(__SIZE_TYPE__, size_t)
 // missing pthread_t
 // missing sector_t
 __VERIFIER_nondet(short)
-// __VERIFIER_nondet(size_t)
-// missing u32
+__VERIFIER_nondet2(unsigned int, u32)
+__VERIFIER_nondet2(unsigned short int, u16) // not in rules
+__VERIFIER_nondet2(unsigned char, u8) // not in rules
+__VERIFIER_nondet2(unsigned char, unsigned_char) // not in rules
+__VERIFIER_nondet2(long long, longlong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
+__VERIFIER_nondet2(unsigned long long, ulonglong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
+__VERIFIER_nondet2(__uint128_t, uint128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
+__VERIFIER_nondet2(__int128_t, int128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
 __VERIFIER_nondet2(unsigned char, uchar)
 __VERIFIER_nondet2(unsigned int, uint)
 __VERIFIER_nondet2(unsigned long, ulong)
@@ -40,4 +49,4 @@ __VERIFIER_nondet2(void*, pointer)
 
 // atomics are now special in Goblint
 // void __VERIFIER_atomic_begin() { }
-// void __VERIFIER_atomic_end() { }
+// void __VERIFIER_atomic_end() { }

src/analyses/libraryFunctions.ml

@@ -297,6 +297,7 @@ let verifier_atomic = AddrOf (Cil.var (Goblintutil.create_var verifier_atomic_va
 let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__VERIFIER_atomic_begin", special [] @@ Lock { lock = verifier_atomic; try_ = false; write = true; return_on_success = true });
     ("__VERIFIER_atomic_end", special [] @@ Unlock verifier_atomic);
+    ("__VERIFIER_nondet_loff_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *)
   ]
 
 (* TODO: allow selecting which lists to use *)

tests/regression/29-svcomp/30-nondets.c

@@ -0,0 +1,28 @@
+// PARAM: --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"
+#include <pthread.h>
+#include <goblint.h>
+
+// Global is never accessed, hence information about protecting mutexes is implicit \bot
+int g1 = 5;
+
+int main(void) {
+  #ifdef __APPLE__
+    // OS X headers have different names for some types
+  #else
+    size_t x1 = __VERIFIER_nondet_size_t();
+    __U16_TYPE x2 = __VERIFIER_nondet_u16();
+    __uint8_t x3 =__VERIFIER_nondet_u8();
+    __U32_TYPE x4 = __VERIFIER_nondet_u32();
+    size_t x5 = __VERIFIER_nondet_loff_t();
+    __uint128_t x6 = __VERIFIER_nondet_uint128();
+    __int128_t x6andahalf = __VERIFIER_nondet_int128();
+    long long x7 = __VERIFIER_nondet_longlong();
+    unsigned long long x8 = __VERIFIER_nondet_ulonglong();
+    unsigned char x9 = __VERIFIER_nondet_unsigned_char();
+    const char* ptr1 = __VERIFIER_nondet_const_char_pointer();
+    char* ptr2 = __VERIFIER_nondet_charp();
+  #endif
+
+  __goblint_check(g1 == 5); // Should not invalidate
+  return 0;
+}