Update nla-digbench-scaling, account for recently found overflows in nla-digbench

c/nla-digbench-scaling/Makefile

@@ -6,6 +6,8 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
+CLANG_WARNINGS := -Wno-error=tautological-compare
+
 LEVEL := ../
 include $(LEVEL)/Makefile.config
 

c/nla-digbench-scaling/README.md

@@ -1,3 +1,11 @@
+<!--
+This file is part of the SV-Benchmarks collection of verification tasks:
+https://github.com/sosy-lab/sv-benchmarks
+
+SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
+
+SPDX-License-Identifier: Apache-2.0
+-->
 The benchmarks in this directory were generated
 by Martin Spiessl based on the tasks in the nla-digbench folder,
 which were originally were submitted by

c/nla-digbench-scaling/bresenham-ll_unwindbound1.c

@@ -0,0 +1,52 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int counter = 0;
+int main() {
+    int X, Y;
+    long long x, y, v, xy, yx;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (counter++<1) {
+        yx = (long long) Y*x;
+        xy = (long long) X*y;
+	__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + (long long) 2 * Y;
+        } else {
+            v = v + 2 * ((long long) Y - X);
+            y++;
+        }
+        x++;
+    }
+    xy = (long long) x*y;
+    yx = (long long) Y*x;
+    __VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
+
+    return 0;
+}

c/nla-digbench-scaling/bresenham-ll_unwindbound1.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'bresenham-ll_unwindbound1.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench-scaling/bresenham-ll_unwindbound10.c

@@ -0,0 +1,52 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int counter = 0;
+int main() {
+    int X, Y;
+    long long x, y, v, xy, yx;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (counter++<10) {
+        yx = (long long) Y*x;
+        xy = (long long) X*y;
+	__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + (long long) 2 * Y;
+        } else {
+            v = v + 2 * ((long long) Y - X);
+            y++;
+        }
+        x++;
+    }
+    xy = (long long) x*y;
+    yx = (long long) Y*x;
+    __VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
+
+    return 0;
+}

c/nla-digbench-scaling/bresenham-ll_unwindbound10.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'bresenham-ll_unwindbound10.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench-scaling/bresenham-ll_unwindbound100.c

@@ -0,0 +1,52 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int counter = 0;
+int main() {
+    int X, Y;
+    long long x, y, v, xy, yx;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (counter++<100) {
+        yx = (long long) Y*x;
+        xy = (long long) X*y;
+	__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + (long long) 2 * Y;
+        } else {
+            v = v + 2 * ((long long) Y - X);
+            y++;
+        }
+        x++;
+    }
+    xy = (long long) x*y;
+    yx = (long long) Y*x;
+    __VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
+
+    return 0;
+}

c/nla-digbench-scaling/bresenham-ll_unwindbound100.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'bresenham-ll_unwindbound100.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench-scaling/bresenham-ll_unwindbound2.c

@@ -0,0 +1,52 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int counter = 0;
+int main() {
+    int X, Y;
+    long long x, y, v, xy, yx;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (counter++<2) {
+        yx = (long long) Y*x;
+        xy = (long long) X*y;
+	__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + (long long) 2 * Y;
+        } else {
+            v = v + 2 * ((long long) Y - X);
+            y++;
+        }
+        x++;
+    }
+    xy = (long long) x*y;
+    yx = (long long) Y*x;
+    __VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
+
+    return 0;
+}

c/nla-digbench-scaling/bresenham-ll_unwindbound2.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'bresenham-ll_unwindbound2.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench-scaling/bresenham-ll_unwindbound20.c

@@ -0,0 +1,52 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int counter = 0;
+int main() {
+    int X, Y;
+    long long x, y, v, xy, yx;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (counter++<20) {
+        yx = (long long) Y*x;
+        xy = (long long) X*y;
+	__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + (long long) 2 * Y;
+        } else {
+            v = v + 2 * ((long long) Y - X);
+            y++;
+        }
+        x++;
+    }
+    xy = (long long) x*y;
+    yx = (long long) Y*x;
+    __VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
+
+    return 0;
+}

c/nla-digbench-scaling/bresenham-ll_unwindbound20.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'bresenham-ll_unwindbound20.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench-scaling/bresenham-ll_unwindbound5.c

@@ -0,0 +1,52 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int counter = 0;
+int main() {
+    int X, Y;
+    long long x, y, v, xy, yx;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (counter++<5) {
+        yx = (long long) Y*x;
+        xy = (long long) X*y;
+	__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + (long long) 2 * Y;
+        } else {
+            v = v + 2 * ((long long) Y - X);
+            y++;
+        }
+        x++;
+    }
+    xy = (long long) x*y;
+    yx = (long long) Y*x;
+    __VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
+
+    return 0;
+}