Merge pull request #1204 from hernanponcedeleon/missing-overflow

Added missing expected result for no-overflow property
sosy-lab · Oct 30, 2020 · c290f49 · c290f49
2 parents 835b3b1 + 43b4acf
commit c290f49
Show file tree

Hide file tree

Showing 8 changed files with 16 additions and 0 deletions.
diff --git a/c/nla-digbench/divbin.yml b/c/nla-digbench/divbin.yml
@@ -3,6 +3,8 @@ input_files: 'divbin.i'
 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/divbin2.yml b/c/nla-digbench/divbin2.yml
@@ -3,6 +3,8 @@ input_files: 'divbin2.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/freire1.yml b/c/nla-digbench/freire1.yml
@@ -3,6 +3,8 @@ input_files: 'freire1.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/freire2.yml b/c/nla-digbench/freire2.yml
@@ -3,6 +3,8 @@ input_files: 'freire2.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/knuth.yml b/c/nla-digbench/knuth.yml
@@ -3,6 +3,8 @@ input_files: 'knuth.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/lcm1.yml b/c/nla-digbench/lcm1.yml
@@ -3,6 +3,8 @@ input_files: 'lcm1.c'
 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/lcm2.yml b/c/nla-digbench/lcm2.yml
@@ -3,6 +3,8 @@ input_files: 'lcm2.c'
 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/mannadiv.yml b/c/nla-digbench/mannadiv.yml
@@ -3,6 +3,8 @@ input_files: 'mannadiv.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C