From f7e4462dda207367138b259fe0751ee061e86032 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 25 Sep 2024 15:48:25 +0300 Subject: [PATCH] Add cram test for SV-COMP architecture --- tests/regression/29-svcomp/36-svcomp-arch.c | 8 ++++++++ tests/regression/29-svcomp/36-svcomp-arch.t | 22 +++++++++++++++++++++ 2 files changed, 30 insertions(+) create mode 100644 tests/regression/29-svcomp/36-svcomp-arch.c create mode 100644 tests/regression/29-svcomp/36-svcomp-arch.t diff --git a/tests/regression/29-svcomp/36-svcomp-arch.c b/tests/regression/29-svcomp/36-svcomp-arch.c new file mode 100644 index 0000000000..ea68ba187c --- /dev/null +++ b/tests/regression/29-svcomp/36-svcomp-arch.c @@ -0,0 +1,8 @@ +// CRAM +#include + +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 new file mode 100644 index 0000000000..a0715e3872 --- /dev/null +++ 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