Make gen. script work for base case(no cov. prop.)

sim642 · Nov 10, 2020 · e0661f6 · e0661f6
1 parent eba6892
commit e0661f6
Show file tree

Hide file tree

Showing 27 changed files with 14 additions and 31 deletions.
diff --git a/c/nla-digbench-scaling/cohencu-ll_unwindbound1.yml b/c/nla-digbench-scaling/cohencu-ll_unwindbound1.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/cohencu-ll_unwindbound10.yml b/c/nla-digbench-scaling/cohencu-ll_unwindbound10.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/cohencu-ll_unwindbound100.yml b/c/nla-digbench-scaling/cohencu-ll_unwindbound100.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/cohencu-ll_unwindbound2.yml b/c/nla-digbench-scaling/cohencu-ll_unwindbound2.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/cohencu-ll_unwindbound20.yml b/c/nla-digbench-scaling/cohencu-ll_unwindbound20.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/cohencu-ll_unwindbound5.yml b/c/nla-digbench-scaling/cohencu-ll_unwindbound5.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/cohencu-ll_unwindbound50.yml b/c/nla-digbench-scaling/cohencu-ll_unwindbound50.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/dijkstra-u_unwindbound10.yml b/c/nla-digbench-scaling/dijkstra-u_unwindbound10.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/dijkstra-u_unwindbound100.yml b/c/nla-digbench-scaling/dijkstra-u_unwindbound100.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/dijkstra-u_unwindbound20.yml b/c/nla-digbench-scaling/dijkstra-u_unwindbound20.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/dijkstra-u_unwindbound5.yml b/c/nla-digbench-scaling/dijkstra-u_unwindbound5.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/dijkstra-u_unwindbound50.yml b/c/nla-digbench-scaling/dijkstra-u_unwindbound50.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/generate.py b/c/nla-digbench-scaling/generate.py
@@ -1,9 +1,9 @@
 #!/usr/bin/env python3
 # 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
 
 """
@@ -110,6 +110,7 @@ def p(s: str) -> str:
         template = templatefun(fullpath)
         abort = False
         ymlcontent = open(join(NLADIR, file[:-2] + ".yml"), "r").read()
+        consider_coverage = "coverage-branches" in ymlcontent
 
         if (
             any(re.search(entry, file) for entry in healed_by_valuebound)
@@ -131,8 +132,14 @@ def p(s: str) -> str:
             and name == "_unwindbound"
         ):
             ymlcontent = re.sub(REACH + "true", REACH + "false", ymlcontent)
-            marker = "  - property_file: ../properties/no-overflow.prp\n    expected_verdict: true"
-            ymlcontent = re.sub(marker,marker+"\n  - property_file: ../properties/coverage-error-call.prp", ymlcontent)
+            if consider_coverage:
+                marker = "  - property_file: ../properties/no-overflow.prp\n    expected_verdict: true"
+                ymlcontent = re.sub(
+                    marker,
+                    marker
+                    + "\n  - property_file: ../properties/coverage-error-call.prp",
+                    ymlcontent,
+                )
         properties = re.findall("property_file: (.*)", ymlcontent)
         has_overflow_property = False
         for m in properties:
@@ -142,7 +149,9 @@ def p(s: str) -> str:
             if "no-overflow" in m:
                 has_overflow_property = True
         if (
-            len(properties) == 2 and has_overflow_property
+            len(properties) == 1
+            and has_overflow_property
+            or (consider_coverage and len(properties) == 2 and has_overflow_property)
         ):  # overflow is only property -> verdict false
             abort = True
         if abort:

diff --git a/c/nla-digbench-scaling/hard-ll_unwindbound1.yml b/c/nla-digbench-scaling/hard-ll_unwindbound1.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/hard-ll_unwindbound10.yml b/c/nla-digbench-scaling/hard-ll_unwindbound10.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/hard-ll_unwindbound100.yml b/c/nla-digbench-scaling/hard-ll_unwindbound100.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/hard-ll_unwindbound2.yml b/c/nla-digbench-scaling/hard-ll_unwindbound2.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/hard-ll_unwindbound20.yml b/c/nla-digbench-scaling/hard-ll_unwindbound20.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/hard-ll_unwindbound5.yml b/c/nla-digbench-scaling/hard-ll_unwindbound5.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/hard-ll_unwindbound50.yml b/c/nla-digbench-scaling/hard-ll_unwindbound50.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/lcm1_unwindbound1.yml b/c/nla-digbench-scaling/lcm1_unwindbound1.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/lcm1_unwindbound10.yml b/c/nla-digbench-scaling/lcm1_unwindbound10.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/lcm1_unwindbound100.yml b/c/nla-digbench-scaling/lcm1_unwindbound100.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/lcm1_unwindbound2.yml b/c/nla-digbench-scaling/lcm1_unwindbound2.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/lcm1_unwindbound20.yml b/c/nla-digbench-scaling/lcm1_unwindbound20.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/lcm1_unwindbound5.yml b/c/nla-digbench-scaling/lcm1_unwindbound5.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C

diff --git a/c/nla-digbench-scaling/lcm1_unwindbound50.yml b/c/nla-digbench-scaling/lcm1_unwindbound50.yml
@@ -5,7 +5,6 @@ properties:
     expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
-  - property_file: ../properties/coverage-error-call.prp
 
 options:
   language: C