Add updated no-overflow verdicts from PR sosy-lab#1204

MartinSpiessl · Oct 30, 2020 · 0e11306 · 0e11306
1 parent 525e3b0
commit 0e11306
Show file tree

Hide file tree

Showing 112 changed files with 224 additions and 0 deletions.
diff --git a/c/nla-digbench-scaling/divbin2_unwindbound1.yml b/c/nla-digbench-scaling/divbin2_unwindbound1.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_unwindbound1.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_unwindbound10.yml b/c/nla-digbench-scaling/divbin2_unwindbound10.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_unwindbound10.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_unwindbound100.yml b/c/nla-digbench-scaling/divbin2_unwindbound100.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_unwindbound100.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_unwindbound2.yml b/c/nla-digbench-scaling/divbin2_unwindbound2.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_unwindbound2.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_unwindbound20.yml b/c/nla-digbench-scaling/divbin2_unwindbound20.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_unwindbound20.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_unwindbound5.yml b/c/nla-digbench-scaling/divbin2_unwindbound5.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_unwindbound5.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_unwindbound50.yml b/c/nla-digbench-scaling/divbin2_unwindbound50.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_unwindbound50.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_valuebound1.yml b/c/nla-digbench-scaling/divbin2_valuebound1.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_valuebound1.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_valuebound10.yml b/c/nla-digbench-scaling/divbin2_valuebound10.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_valuebound10.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_valuebound100.yml b/c/nla-digbench-scaling/divbin2_valuebound100.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_valuebound100.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_valuebound2.yml b/c/nla-digbench-scaling/divbin2_valuebound2.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_valuebound2.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_valuebound20.yml b/c/nla-digbench-scaling/divbin2_valuebound20.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_valuebound20.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_valuebound5.yml b/c/nla-digbench-scaling/divbin2_valuebound5.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_valuebound5.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin2_valuebound50.yml b/c/nla-digbench-scaling/divbin2_valuebound50.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2_valuebound50.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_unwindbound1.yml b/c/nla-digbench-scaling/divbin_unwindbound1.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_unwindbound1.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_unwindbound10.yml b/c/nla-digbench-scaling/divbin_unwindbound10.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_unwindbound10.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_unwindbound100.yml b/c/nla-digbench-scaling/divbin_unwindbound100.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_unwindbound100.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_unwindbound2.yml b/c/nla-digbench-scaling/divbin_unwindbound2.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_unwindbound2.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_unwindbound20.yml b/c/nla-digbench-scaling/divbin_unwindbound20.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_unwindbound20.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_unwindbound5.yml b/c/nla-digbench-scaling/divbin_unwindbound5.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_unwindbound5.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_unwindbound50.yml b/c/nla-digbench-scaling/divbin_unwindbound50.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_unwindbound50.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_valuebound1.yml b/c/nla-digbench-scaling/divbin_valuebound1.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_valuebound1.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_valuebound10.yml b/c/nla-digbench-scaling/divbin_valuebound10.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_valuebound10.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_valuebound100.yml b/c/nla-digbench-scaling/divbin_valuebound100.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_valuebound100.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_valuebound2.yml b/c/nla-digbench-scaling/divbin_valuebound2.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_valuebound2.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_valuebound20.yml b/c/nla-digbench-scaling/divbin_valuebound20.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_valuebound20.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_valuebound5.yml b/c/nla-digbench-scaling/divbin_valuebound5.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_valuebound5.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/divbin_valuebound50.yml b/c/nla-digbench-scaling/divbin_valuebound50.yml
@@ -3,6 +3,8 @@ input_files: 'divbin_valuebound50.i'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_unwindbound1.yml b/c/nla-digbench-scaling/freire1_unwindbound1.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_unwindbound1.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_unwindbound10.yml b/c/nla-digbench-scaling/freire1_unwindbound10.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_unwindbound10.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_unwindbound100.yml b/c/nla-digbench-scaling/freire1_unwindbound100.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_unwindbound100.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_unwindbound2.yml b/c/nla-digbench-scaling/freire1_unwindbound2.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_unwindbound2.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_unwindbound20.yml b/c/nla-digbench-scaling/freire1_unwindbound20.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_unwindbound20.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_unwindbound5.yml b/c/nla-digbench-scaling/freire1_unwindbound5.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_unwindbound5.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_unwindbound50.yml b/c/nla-digbench-scaling/freire1_unwindbound50.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_unwindbound50.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_valuebound1.yml b/c/nla-digbench-scaling/freire1_valuebound1.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_valuebound1.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_valuebound10.yml b/c/nla-digbench-scaling/freire1_valuebound10.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_valuebound10.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_valuebound100.yml b/c/nla-digbench-scaling/freire1_valuebound100.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_valuebound100.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_valuebound2.yml b/c/nla-digbench-scaling/freire1_valuebound2.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_valuebound2.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_valuebound20.yml b/c/nla-digbench-scaling/freire1_valuebound20.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_valuebound20.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_valuebound5.yml b/c/nla-digbench-scaling/freire1_valuebound5.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_valuebound5.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire1_valuebound50.yml b/c/nla-digbench-scaling/freire1_valuebound50.yml
@@ -3,6 +3,8 @@ input_files: 'freire1_valuebound50.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire2_unwindbound1.yml b/c/nla-digbench-scaling/freire2_unwindbound1.yml
@@ -3,6 +3,8 @@ input_files: 'freire2_unwindbound1.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/freire2_unwindbound10.yml b/c/nla-digbench-scaling/freire2_unwindbound10.yml
@@ -3,6 +3,8 @@ input_files: 'freire2_unwindbound10.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C