Add __VERIFIER_assert to library functions for evalAssert transformed…

… output analysis
goblint · Mar 12, 2024 · 98ef567 · 98ef567
1 parent 7ffd335
commit 98ef567
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 23 deletions.
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
@@ -1028,6 +1028,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__VERIFIER_nondet_loff_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *)
     ("__VERIFIER_nondet_int", unknown []);  (* declare invalidate actions to prevent invalidating globals when extern in regression tests *)
     ("__VERIFIER_nondet_size_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *)
+    ("__VERIFIER_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if definition missing (e.g. in evalAssert transformed output) or extraspecial *)
   ]
 [@@coverage off]
 

diff --git a/tests/regression/29-svcomp/33-verifier-assert-undef.t b/tests/regression/29-svcomp/33-verifier-assert-undef.t
@@ -1,15 +1,11 @@
   $ goblint --enable ana.sv-comp.functions 33-verifier-assert-undef.c
-  [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:5:3-5:23)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:5:3-5:23)
-  [Info][Imprecise] Invalidating expressions: 1 (33-verifier-assert-undef.c:5:3-5:23)
-  [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:6:3-6:23)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:6:3-6:23)
-  [Info][Imprecise] Invalidating expressions: r (33-verifier-assert-undef.c:6:3-6:23)
-  [Error][Imprecise][Unsound] Function definition missing for __VERIFIER_assert (33-verifier-assert-undef.c:7:3-7:23)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (33-verifier-assert-undef.c:7:3-7:23)
-  [Info][Imprecise] Invalidating expressions: 0 (33-verifier-assert-undef.c:7:3-7:23)
-  [Info][Deadcode] Logical lines of code (LLoC) summary:
-    live: 5
-    dead: 0
+  [Success][Assert] Assertion "1" will succeed (33-verifier-assert-undef.c:5:3-5:23)
+  [Warning][Assert] Assertion "r" is unknown. (33-verifier-assert-undef.c:6:3-6:23)
+  [Error][Assert] Assertion "0" will fail. (33-verifier-assert-undef.c:7:3-7:23)
+  [Warning][Deadcode] Function 'main' does not return
+  [Warning][Deadcode] Function 'main' has dead code:
+    on line 8 (33-verifier-assert-undef.c:8-8)
+  [Warning][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 1
     total lines: 5
-  [Error][Imprecise][Unsound] Function definition missing
diff --git a/tests/regression/29-svcomp/34-verifier-assert-def.c b/tests/regression/29-svcomp/34-verifier-assert-def.c
@@ -1,6 +1,6 @@
 // PARAM: --enable ana.sv-comp.functions --enable ana.int.interval
 
-void __VERIFIER_assert(int cond) {
+void __VERIFIER_assert(int cond) { // NOWARN (update_suite assert detection spurious)
   int x = 1 << 80;
 }
 

diff --git a/tests/regression/29-svcomp/34-verifier-assert-def.t b/tests/regression/29-svcomp/34-verifier-assert-def.t
@@ -7,16 +7,16 @@
 
   $ goblint --enable ana.sv-comp.functions --set exp.extraspecials[+] __VERIFIER_assert 34-verifier-assert-def.c
   [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:9:3-9:23)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:9:3-9:23)
-  [Info][Imprecise] Invalidating expressions: 1 (34-verifier-assert-def.c:9:3-9:23)
+  [Success][Assert] Assertion "1" will succeed (34-verifier-assert-def.c:9:3-9:23)
   [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:10:3-10:23)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:10:3-10:23)
-  [Info][Imprecise] Invalidating expressions: r (34-verifier-assert-def.c:10:3-10:23)
+  [Warning][Assert] Assertion "r" is unknown. (34-verifier-assert-def.c:10:3-10:23)
   [Info][Analyzer] Using special for defined function __VERIFIER_assert (34-verifier-assert-def.c:11:3-11:23)
-  [Info][Imprecise] INVALIDATING ALL GLOBALS! (34-verifier-assert-def.c:11:3-11:23)
-  [Info][Imprecise] Invalidating expressions: 0 (34-verifier-assert-def.c:11:3-11:23)
+  [Error][Assert] Assertion "0" will fail. (34-verifier-assert-def.c:11:3-11:23)
   [Warning][Deadcode] Function '__VERIFIER_assert' is uncalled: 2 LLoC (34-verifier-assert-def.c:3:1-5:1)
-  [Info][Deadcode] Logical lines of code (LLoC) summary:
-    live: 5
-    dead: 2 (2 in uncalled functions)
+  [Warning][Deadcode] Function 'main' does not return
+  [Warning][Deadcode] Function 'main' has dead code:
+    on line 12 (34-verifier-assert-def.c:12-12)
+  [Warning][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 3 (2 in uncalled functions)
     total lines: 7