Add cram test for sv-comp no-ov verdict.

goblint · Nov 21, 2023 · 464cdd3 · 464cdd3
1 parent 4f7eb52
commit 464cdd3
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/tests/regression/29-svcomp/32-no-ov.t b/tests/regression/29-svcomp/32-no-ov.t
@@ -0,0 +1,16 @@
+  $ goblint --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )"  32-no-ov.c
+  SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
+  [Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (32-no-ov.c:5:6-5:159)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 3
+    dead: 0
+    total lines: 3
+  SV-COMP result: true
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
diff --git a/tests/regression/29-svcomp/dune b/tests/regression/29-svcomp/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))