Skip to content

Always report exception output in __CPROVER_start #814

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 14, 2017
Merged

Always report exception output in __CPROVER_start #814

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 41 additions & 6 deletions src/goto-programs/remove_exceptions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,6 +192,39 @@ void remove_exceptionst::instrument_exception_handler(

/*******************************************************************\

Function: get_exceptional_output

Inputs:

Outputs:

Purpose: finds the instruction where the exceptional output is set
or the end of the function if no such output exists

\*******************************************************************/

static goto_programt::targett get_exceptional_output(
goto_programt &goto_program)
{
Forall_goto_program_instructions(it, goto_program)
{
const irep_idt &statement=it->code.get_statement();
if(statement==ID_output)
{
assert(it->code.operands().size()>=2);
const exprt &expr=it->code.op1();
assert(expr.id()==ID_symbol);
const symbol_exprt &symbol=to_symbol_expr(expr);
if(id2string(symbol.get_identifier()).find(EXC_SUFFIX)
!=std::string::npos)
return it;
}
}
return goto_program.get_end_function();
}

/*******************************************************************\

Function: remove_exceptionst::instrument_throw

Inputs:
Expand All @@ -217,13 +250,14 @@ void remove_exceptionst::instrument_throw(
assert(instr_it->code.operands().size()==1);

// find the end of the function
goto_programt::targett end_function=goto_program.get_end_function();
if(end_function!=instr_it)
goto_programt::targett exceptional_output=
get_exceptional_output(goto_program);
if(exceptional_output!=instr_it)
{
// jump to the end of the function
// this will appear after the GOTO-based dynamic dispatch below
goto_programt::targett t_end=goto_program.insert_after(instr_it);
t_end->make_goto(end_function);
t_end->make_goto(exceptional_output);
t_end->source_location=instr_it->source_location;
t_end->function=instr_it->function;
}
Expand Down Expand Up @@ -322,13 +356,14 @@ void remove_exceptionst::instrument_function_call(
symbol_exprt callee_exc=callee_exc_symbol.symbol_expr();

// find the end of the function
goto_programt::targett end_function=goto_program.get_end_function();
if(end_function!=instr_it)
goto_programt::targett exceptional_output=
get_exceptional_output(goto_program);
if(exceptional_output!=instr_it)
{
// jump to the end of the function
// this will appear after the GOTO-based dynamic dispatch below
goto_programt::targett t_end=goto_program.insert_after(instr_it);
t_end->make_goto(end_function);
t_end->make_goto(exceptional_output);
t_end->source_location=instr_it->source_location;
t_end->function=instr_it->function;
}
Expand Down