Skip to content

Commit eb18f6f

Browse files
tautschnigtautschnig
authored
Merge pull request #736 from diffblue/smv-tests
move the SMV-related tests into a separate directory
2 parents b5ce8d2 + bd65f74 commit eb18f6f

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

75 files changed

+27
-0
lines changed

‎.github/workflows/ebmc-release.yaml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,8 @@ jobs:
7777
run: make -C regression/ebmc test
7878
- name: Run the verilog tests
7979
run: make -C regression/verilog test
80+
- name: Run the smv tests
81+
run: make -C regression/smv test
8082
- name: Print ccache stats
8183
run: ccache -s
8284
- name: Create .deb
@@ -160,6 +162,8 @@ jobs:
160162
make -C regression/ebmc test
161163
- name: Run the verilog tests
162164
run: make -C regression/verilog test
165+
- name: Run the smv tests
166+
run: make -C regression/smv test
163167
- name: Create .rpm
164168
id: create_packages
165169
run: |

‎.github/workflows/pull-request-checks.yaml‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,10 @@ jobs:
5151
run: make -C regression/verilog test
5252
- name: Run the verilog tests with Z3
5353
run: make -C regression/verilog test-z3
54+
- name: Run the smv tests
55+
run: make -C regression/smv test
56+
- name: Run the smv tests with Z3
57+
run: make -C regression/smv test-z3
5458
- name: Run the vlindex tests
5559
run: make -C regression/vlindex test
5660
- name: Print ccache stats
@@ -105,6 +109,10 @@ jobs:
105109
run: make -C regression/verilog test
106110
- name: Run the verilog tests with Z3
107111
run: make -C regression/verilog test-z3
112+
- name: Run the smv tests
113+
run: make -C regression/smv test
114+
- name: Run the smv tests with Z3
115+
run: make -C regression/smv test-z3
108116
- name: Run the vlindex tests
109117
run: make -C regression/vlindex test
110118
- name: Print ccache stats
@@ -185,6 +193,8 @@ jobs:
185193
make -C regression/ebmc test
186194
- name: Run the verilog tests
187195
run: make -C regression/verilog test
196+
- name: Run the smv tests
197+
run: make -C regression/smv test
188198
- name: Run the vlindex tests
189199
run: make -C regression/vlindex test
190200
- name: Print ccache stats
@@ -228,6 +238,10 @@ jobs:
228238
run: make -C regression/verilog test
229239
- name: Run the verilog tests with Z3
230240
run: make -C regression/verilog test-z3
241+
- name: Run the smv tests
242+
run: make -C regression/smv test
243+
- name: Run the smv tests with Z3
244+
run: make -C regression/smv test-z3
231245
- name: Run the vlindex tests
232246
run: make -C regression/vlindex test
233247
- name: Print ccache stats

‎regression/smv/Makefile‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
default: test
2+
3+
TEST_PL = ../../lib/cbmc/regression/test.pl
4+
5+
test:
6+
@$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc
7+
8+
test-z3:
9+
@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend

regression/ebmc/smv-netlist/smv_netlist1.desc renamed to regression/smv/smv-netlist/smv_netlist1.desc

File renamed without changes.

regression/ebmc/smv-netlist/smv_netlist1.v renamed to regression/smv/smv-netlist/smv_netlist1.v

File renamed without changes.

regression/ebmc/smv/bdd_unsupported_property.desc renamed to regression/smv/smv/bdd_unsupported_property.desc

File renamed without changes.

regression/ebmc/smv/bdd_unsupported_property.smv renamed to regression/smv/smv/bdd_unsupported_property.smv

File renamed without changes.

regression/ebmc/smv/bmc_unsupported_property1.desc renamed to regression/smv/smv/bmc_unsupported_property1.desc

File renamed without changes.

regression/ebmc/smv/bmc_unsupported_property1.smv renamed to regression/smv/smv/bmc_unsupported_property1.smv

File renamed without changes.

regression/ebmc/smv/bmc_unsupported_property2.desc renamed to regression/smv/smv/bmc_unsupported_property2.desc

File renamed without changes.

0 commit comments

Comments
 (0)