diff --git a/tests/regression/issue-1356.t/issue-1356.c b/tests/regression/issue-1356.t/issue-1356.c new file mode 100644 index 0000000000..b773f6cf66 --- /dev/null +++ b/tests/regression/issue-1356.t/issue-1356.c @@ -0,0 +1,20 @@ +extern int __VERIFIER_nondet_int(void); + +extern void abort(void); +void assume_abort_if_not(int cond) { + if(!cond) {abort();} +} + +int minus(int a, int b) { + assume_abort_if_not(b <= 0 || a >= b - 2147483648); // there shouldn't be invariants 1 <= b and b != 0 before this line + assume_abort_if_not(b >= 0 || a <= b + 2147483647); // there shouldn't be invariants b <= -1 and b != 0 before this line + return a - b; +} + +int main() { + int x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + minus(x, y); + return 0; +} diff --git a/tests/regression/issue-1356.t/run.t b/tests/regression/issue-1356.t/run.t new file mode 100644 index 0000000000..7765c02b8d --- /dev/null +++ b/tests/regression/issue-1356.t/run.t @@ -0,0 +1,12 @@ + $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' issue-1356.c + [Warning][Integer > Overflow][CWE-190] Signed integer overflow (issue-1356.c:10:3-10:53) + [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:3-11:15) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 13 + dead: 0 + total lines: 13 + [Info][Witness] witness generation summary: + total generation entries: 0 + + $ yamlWitnessStrip < witness.yml + []