replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #2728 from tautschnig/symex-assertions-debug 

goto-symex: Print (at debug level) the current assertion being converted
This commit is contained in:
Michael Tautschnig 2018-09-04 10:02:28 +01:00 committed by GitHub
parent 156faa19c6 cf4c31770d
commit 84170dfe02
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 17 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
src/goto-symex/symex_target_equation.cpp
View File

@ -410,9 +410,8 @@ void symex_target_equationt::convert_assignments(
decision_procedure.conditional_output(
decision_procedure.debug(),
[&step](messaget::mstreamt &mstream) {
std::ostringstream oss;
step.output(oss);
mstream << oss.str() << messaget::eom;
step.output(mstream);
mstream << messaget::eom;
});
decision_procedure.set_to_true(step.cond_expr);
@ -459,9 +458,8 @@ void symex_target_equationt::convert_guards(
prop_conv.conditional_output(
prop_conv.debug(),
[&step](messaget::mstreamt &mstream) {
std::ostringstream oss;
step.output(oss);
mstream << oss.str() << messaget::eom;
step.output(mstream);
mstream << messaget::eom;
});
try
@ -494,9 +492,8 @@ void symex_target_equationt::convert_assumptions(
prop_conv.conditional_output(
prop_conv.debug(),
[&step](messaget::mstreamt &mstream) {
std::ostringstream oss;
step.output(oss);
mstream << oss.str() << messaget::eom;
step.output(mstream);
mstream << messaget::eom;
});
try
@ -530,9 +527,8 @@ void symex_target_equationt::convert_goto_instructions(
prop_conv.conditional_output(
prop_conv.debug(),
[&step](messaget::mstreamt &mstream) {
std::ostringstream oss;
step.output(oss);
mstream << oss.str() << messaget::eom;
step.output(mstream);
mstream << messaget::eom;
});
try
@ -565,9 +561,8 @@ void symex_target_equationt::convert_constraints(
decision_procedure.conditional_output(
decision_procedure.debug(),
[&step](messaget::mstreamt &mstream) {
std::ostringstream oss;
step.output(oss);
mstream << oss.str() << messaget::eom;
step.output(mstream);
mstream << messaget::eom;
});
try
@ -626,6 +621,13 @@ void symex_target_equationt::convert_assertions(
{
if(step.is_assert())
{
prop_conv.conditional_output(
prop_conv.debug(),
[&step](messaget::mstreamt &mstream) {
step.output(mstream);
mstream << messaget::eom;
});
implies_exprt implication(
assumption,
step.cond_expr);