Skip to content

Commit 9129e09

Browse files
smowtonsmowton
authored
Merge pull request #3747 from smowton/smowton/feature/jbmc-validation
JBMC: enable model and SSA equation verification
2 parents 4c7f9fc + 4232b15 commit 9129e09

File tree

21 files changed

+104
-48
lines changed

21 files changed

+104
-48
lines changed

‎jbmc/regression/jbmc-concurrency/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:jbmc>"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)

‎jbmc/regression/jbmc-concurrency/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
9+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/jbmc-generics/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc>"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)
44

55
add_test_pl_profile(
66
"jbmc-generics-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/jbmc-generics/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
tests.log: ../$(CPROVER_DIR)/regression/test.pl
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
10+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
1212

1313
show:
1414
@for dir in *; do \

‎jbmc/regression/jbmc-inheritance/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:jbmc>"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)

‎jbmc/regression/jbmc-inheritance/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
9+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/jbmc-strings/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc>"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)
44

55
add_test_pl_profile(
66
"jbmc-strings-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/jbmc-strings/Makefile

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
testfuture:
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
10+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
1212

1313
testall:
14-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
15-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
14+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
15+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
18-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
19-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
18+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
19+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
2020

2121
show:
2222
@for dir in *; do \

‎jbmc/regression/jbmc/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc>"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)
44

55
add_test_pl_profile(
66
"jbmc-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/jbmc/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
tests.log: ../$(CPROVER_DIR)/regression/test.pl
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
10+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
1212

1313
show:
1414
@for dir in *; do \

‎jbmc/regression/strings-smoke-tests/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc>"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)
44

55
add_test_pl_profile(
66
"strings-smoke-tests-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/strings-smoke-tests/Makefile

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
testfuture:
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
10+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
1212

1313
testall:
14-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
15-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
14+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
15+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
18-
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
19-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
18+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
19+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
2020

2121
show:
2222
@for dir in *; do \

‎jbmc/src/java_bytecode/simple_method_stubbing.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -170,7 +170,8 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
170170
symbol_table);
171171
const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
172172
code_assignt get_argument(
173-
init_symbol_expression, symbol_exprt(this_argument.get_identifier()));
173+
init_symbol_expression,
174+
symbol_exprt(this_argument.get_identifier(), this_type));
174175
get_argument.add_source_location() = synthesized_source_location;
175176
new_instructions.add(get_argument);
176177
create_method_stub_at(

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -371,6 +371,16 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
371371
"symex-coverage-report",
372372
cmdline.get_value("symex-coverage-report"));
373373

374+
if(cmdline.isset("validate-ssa-equation"))
375+
{
376+
options.set_option("validate-ssa-equation", true);
377+
}
378+
379+
if(cmdline.isset("validate-goto-model"))
380+
{
381+
options.set_option("validate-goto-model", true);
382+
}
383+
374384
PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
375385

376386
if(cmdline.isset("no-lazy-methods"))
@@ -555,6 +565,11 @@ int jbmc_parse_optionst::doit()
555565
if(set_properties(goto_model))
556566
return 7; // should contemplate EX_USAGE from sysexits.h
557567

568+
if(cmdline.isset("validate-goto-model"))
569+
{
570+
goto_model.validate(validation_modet::INVARIANT);
571+
}
572+
558573
// The `configure_bmc` callback passed will enable enum-unwind-static if
559574
// applicable.
560575
return bmct::do_language_agnostic_bmc(
@@ -587,6 +602,11 @@ int jbmc_parse_optionst::doit()
587602
// particular function:
588603
add_failed_symbols(lazy_goto_model.symbol_table);
589604

605+
if(cmdline.isset("validate-goto-model"))
606+
{
607+
lazy_goto_model.validate(validation_modet::INVARIANT);
608+
}
609+
590610
// Provide show-goto-functions and similar dump functions after symex
591611
// executes. If --paths is active, these dump routines run after every
592612
// paths iteration. Its return value indicates that if we ran any dump
@@ -1143,6 +1163,7 @@ void jbmc_parse_optionst::help()
11431163
" --version show version and exit\n"
11441164
" --xml-ui use XML-formatted output\n"
11451165
" --json-ui use JSON-formatted output\n"
1166+
HELP_VALIDATE
11461167
HELP_GOTO_TRACE
11471168
HELP_FLUSH
11481169
" --verbosity # verbosity level\n"

‎jbmc/src/jbmc/jbmc_parse_options.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
1313
#define CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
1414

15-
#include <util/ui_message.h>
1615
#include <util/parse_options.h>
1716
#include <util/timestamper.h>
17+
#include <util/ui_message.h>
18+
#include <util/validation_interface.h>
1819

1920
#include <langapi/language.h>
2021

@@ -79,6 +80,7 @@ class optionst;
7980
"(localize-faults)(localize-faults-method):" \
8081
"(java-threading)" \
8182
OPT_GOTO_TRACE \
83+
OPT_VALIDATE \
8284
"(symex-driven-lazy-loading)"
8385
// clang-format on
8486

‎src/goto-programs/abstract_goto_model.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,12 @@ class abstract_goto_modelt
4949
/// underneath them, so this should only be used to lend a reference to code
5050
/// that cannot also call get_goto_function.
5151
virtual const symbol_tablet &get_symbol_table() const = 0;
52+
53+
/// Check that the goto model is well-formed
54+
///
55+
/// The validation mode indicates whether well-formedness check failures are
56+
/// reported via DATA_INVARIANT violations or exceptions.
57+
virtual void validate(const validation_modet vm) const = 0;
5258
};
5359

5460
#endif

‎src/goto-programs/goto_model.h

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ class goto_modelt : public abstract_goto_modelt
9494
///
9595
/// The validation mode indicates whether well-formedness check failures are
9696
/// reported via DATA_INVARIANT violations or exceptions.
97-
void validate(const validation_modet vm) const
97+
void validate(const validation_modet vm) const override
9898
{
9999
symbol_table.validate(vm);
100100

@@ -138,6 +138,18 @@ class wrapper_goto_modelt : public abstract_goto_modelt
138138
goto_functions.function_map.end();
139139
}
140140

141+
/// Check that the goto model is well-formed
142+
///
143+
/// The validation mode indicates whether well-formedness check failures are
144+
/// reported via DATA_INVARIANT violations or exceptions.
145+
void validate(const validation_modet vm) const override
146+
{
147+
symbol_table.validate(vm);
148+
149+
const namespacet ns(symbol_table);
150+
goto_functions.validate(ns, vm);
151+
}
152+
141153
private:
142154
const symbol_tablet &symbol_table;
143155
const goto_functionst &goto_functions;

‎src/goto-programs/lazy_goto_model.h

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -243,6 +243,15 @@ class lazy_goto_modelt : public abstract_goto_modelt
243243
return goto_functions.at(id);
244244
}
245245

246+
/// Check that the goto model is well-formed
247+
///
248+
/// The validation mode indicates whether well-formedness check failures are
249+
/// reported via DATA_INVARIANT violations or exceptions.
250+
void validate(const validation_modet vm) const override
251+
{
252+
goto_model->validate(vm);
253+
}
254+
246255
private:
247256
std::unique_ptr<goto_modelt> goto_model;
248257

‎src/goto-symex/symex_target_equation.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -961,15 +961,19 @@ void symex_target_equationt::SSA_stept::validate(
961961
case goto_trace_stept::typet::CONSTRAINT:
962962
validate_full_expr(cond_expr, ns, vm);
963963
break;
964-
case goto_trace_stept::typet::ASSIGNMENT:
965964
case goto_trace_stept::typet::DECL:
965+
validate_full_expr(ssa_lhs, ns, vm);
966+
validate_full_expr(ssa_full_lhs, ns, vm);
967+
validate_full_expr(original_full_lhs, ns, vm);
968+
break;
969+
case goto_trace_stept::typet::ASSIGNMENT:
966970
validate_full_expr(ssa_lhs, ns, vm);
967971
validate_full_expr(ssa_full_lhs, ns, vm);
968972
validate_full_expr(original_full_lhs, ns, vm);
969973
validate_full_expr(ssa_rhs, ns, vm);
970974
DATA_CHECK(
971975
vm,
972-
base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns),
976+
base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns),
973977
"Type inequality in SSA assignment\nlhs-type: " +
974978
ssa_lhs.get_original_expr().type().id_string() +
975979
"\nrhs-type: " + ssa_rhs.type().id_string());

‎src/util/std_code.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -296,14 +296,14 @@ class code_assignt:public codet
296296

297297
static void validate(
298298
const codet &code,
299-
const namespacet &,
299+
const namespacet &ns,
300300
const validation_modet vm = validation_modet::INVARIANT)
301301
{
302302
check(code, vm);
303303

304304
DATA_CHECK(
305305
vm,
306-
code.op0().type() == code.op1().type(),
306+
base_type_eq(code.op0().type(), code.op1().type(), ns),
307307
"lhs and rhs of assignment must have same type");
308308
}
309309

‎src/util/symbol.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -137,10 +137,11 @@ bool symbolt::is_well_formed() const
137137
// Well-formedness criterion number 2 is for a symbol
138138
// to have it's base name as a suffix to it's more
139139
// general name.
140-
if(!has_suffix(id2string(name), id2string(base_name)))
141-
{
140+
// Exception: Java symbols' base names do not have type signatures
141+
// (for example, they can have name "someclass.method:(II)V" and base name
142+
// "method")
143+
if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)
142144
return false;
143-
}
144145

145146
return true;
146147
}

0 commit comments

Comments
 (0)