Skip to content

Commit 9b416ca

Browse files
committed
Enable internal validation for C++ regression tests
We should perform as much sanity checking in regression tests as possible. This required cleaning up unused parameter identifiers and disabling sanity checking of names as is already done for Java, because we similarly have name mangling in C++.
1 parent dec941a commit 9b416ca

File tree

6 files changed

+16
-7
lines changed

6 files changed

+16
-7
lines changed

regression/cbmc-cpp/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ add_test_pl_tests(
44
)
55
else()
66
add_test_pl_tests(
7-
"$<TARGET_FILE:cbmc>"
7+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
88
)
99
endif()

regression/cbmc-cpp/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ else
1010
endif
1111

1212
test:
13-
@../test.pl -e -p -c ../../../src/cbmc/cbmc $(gcc_only)
13+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only)
1414

1515
tests.log: ../test.pl
16-
@../test.pl -e -p -c ../../../src/cbmc/cbmc $(gcc_only)
16+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(gcc_only)
1717

1818
show:
1919
@for dir in *; do \

regression/systemc/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:cbmc>"
2+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
33
)

regression/systemc/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -e -p -c ../../../src/cbmc/cbmc
4+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation"
55

66
tests.log: ../test.pl
7-
@../test.pl -e -p -c ../../../src/cbmc/cbmc
7+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation"
88

99
show:
1010
@for dir in *; do \

src/cpp/cpp_declarator_converter.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -472,6 +472,13 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
472472

473473
if(member_spec.is_inline())
474474
symbol.type.set(ID_C_inlined, true);
475+
476+
if(symbol.value.is_nil())
477+
{
478+
// we don't need the identifiers
479+
for(auto &parameter : to_code_type(symbol.type).parameters())
480+
parameter.set_identifier(irep_idt());
481+
}
475482
}
476483
else
477484
{

src/util/symbol.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,9 @@ bool symbolt::is_well_formed() const
142142
// Exception: Java symbols' base names do not have type signatures
143143
// (for example, they can have name "someclass.method:(II)V" and base name
144144
// "method")
145-
if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)
145+
if(
146+
!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java &&
147+
mode != ID_cpp)
146148
{
147149
bool criterion_must_hold = true;
148150

0 commit comments

Comments
 (0)