Add cram test for SV-COMP architecture

goblint · Sep 25, 2024 · f7e4462 · f7e4462
1 parent bcb15a1
commit f7e4462
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 0 deletions.
diff --git a/tests/regression/29-svcomp/36-svcomp-arch.c b/tests/regression/29-svcomp/36-svcomp-arch.c
@@ -0,0 +1,8 @@
+// CRAM
+#include <limits.h>
+
+int main() {
+  long k = INT_MAX;
+  long n = k * k;
+  return 0;
+}
diff --git a/tests/regression/29-svcomp/36-svcomp-arch.t b/tests/regression/29-svcomp/36-svcomp-arch.t
@@ -0,0 +1,22 @@
+There should be overflow on ILP32:
+
+  $ goblint --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" --set exp.architecture 32bit 36-svcomp-arch.c
+  [Info] Setting "ana.int.interval" to true
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (36-svcomp-arch.c:6:8-6:17)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  SV-COMP result: unknown
+
+There shouldn't be an overflow on LP64:
+
+  $ goblint --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" --set exp.architecture 64bit 36-svcomp-arch.c
+  [Info] Setting "ana.int.interval" to true
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  SV-COMP result: true