Skip to content

Commit b866015

Browse files
author
thk123
committed
Provide the original goto statement in the error
This required the symex target_equation having the namespace to resolve names
1 parent a97bc28 commit b866015

File tree

5 files changed

+13
-4
lines changed

5 files changed

+13
-4
lines changed

src/cbmc/bmc.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ class bmct:public safety_checkert
7878
options(_options),
7979
outer_symbol_table(outer_symbol_table),
8080
ns(outer_symbol_table, symex_symbol_table),
81-
equation(),
81+
equation(ns),
8282
branch_worklist(_branch_worklist),
8383
symex(_message_handler, outer_symbol_table, equation, branch_worklist),
8484
prop_conv(_prop_conv),

src/goto-instrument/accelerate/scratch_program.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ class scratch_programt:public goto_programt
4040
symbol_table(_symbol_table),
4141
symex_symbol_table(),
4242
ns(symbol_table, symex_symbol_table),
43-
equation(),
43+
equation(ns),
4444
branch_worklist(),
4545
symex(mh, symbol_table, equation, branch_worklist),
4646
satcheck(util_make_unique<satcheckt>()),

src/goto-symex/equation_conversion_exceptions.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Diffblue Ltd.
1414

1515
#include <ostream>
1616
#include <util/namespace.h>
17+
#include <langapi/language_util.h>
1718
#include "symex_target_equation.h"
1819

1920
class guard_conversion_exceptiont : public std::runtime_error
@@ -26,6 +27,8 @@ class guard_conversion_exceptiont : public std::runtime_error
2627
{
2728
std::ostringstream error_msg;
2829
error_msg << runtime_error::what();
30+
error_msg << "\nSource GOTO statement: "
31+
<< from_expr(ns, "java", step.source.pc->code);
2932
error_msg << "\nStep:\n";
3033
step.output(ns, error_msg);
3134
error_message = error_msg.str();

src/goto-symex/symex_target_equation.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -437,7 +437,7 @@ void symex_target_equationt::convert_guards(
437437
}
438438
catch(const bitvector_conversion_exceptiont &conversion_exception)
439439
{
440-
std::throw_with_nested(guard_conversion_exceptiont(step));
440+
std::throw_with_nested(guard_conversion_exceptiont(step, ns));
441441
}
442442
}
443443
}

src/goto-symex/symex_target_equation.h

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,10 @@ class prop_convt;
3232
class symex_target_equationt:public symex_targett
3333
{
3434
public:
35-
symex_target_equationt() = default;
35+
explicit symex_target_equationt(const namespacet &ns) : ns(ns)
36+
{
37+
}
38+
3639
virtual ~symex_target_equationt() = default;
3740

3841
// read event
@@ -320,6 +323,9 @@ class symex_target_equationt:public symex_targett
320323
// for enforcing sharing in the expressions stored
321324
merge_irept merge_irep;
322325
void merge_ireps(SSA_stept &SSA_step);
326+
327+
private:
328+
const namespacet &ns;
323329
};
324330

325331
inline bool operator<(

0 commit comments

Comments
 (0)