CBMC
insert_final_assert_false.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Insert assert(false) at end of entry function
4 
5 Author: Nathan Chong, Kareem Khazem
6 
7 \*******************************************************************/
8 
11 
13 
15 #include <util/irep.h>
16 
17 #include <iterator>
18 #include <list>
19 
21  message_handlert &_message_handler)
22  : log(_message_handler)
23 {
24 }
25 
27 operator()(goto_modelt &goto_model, const std::string &function_to_instrument)
28 {
29  const irep_idt entry(function_to_instrument);
30  auto it = goto_model.goto_functions.function_map.find(entry);
31  if(it == goto_model.goto_functions.function_map.end())
32  {
33  log.error() << "insert-final-assert-false: could not find function "
34  << "'" << function_to_instrument << "'" << messaget::eom;
35  return true;
36  }
37  goto_programt &entry_function = (it->second).body;
38  goto_programt::instructionst &instructions = entry_function.instructions;
39  auto instr_it = instructions.end();
40  auto last_instruction = std::prev(instr_it);
42  last_instruction->is_end_function(),
43  "last instruction in function should be END_FUNCTION");
44  source_locationt assert_location = last_instruction->source_location();
45  assert_location.set_property_class(ID_assertion);
46  assert_location.set_comment("insert-final-assert-false (should fail) ");
47  goto_programt::instructiont false_assert =
48  goto_programt::make_assertion(false_exprt(), assert_location);
49  entry_function.insert_before_swap(last_instruction, false_assert);
50  return false;
51 }
52 
54  goto_modelt &goto_model,
55  const std::string &function_to_instrument,
56  message_handlert &message_handler)
57 {
58  insert_final_assert_falset ifaf(message_handler);
59  return ifaf(goto_model, function_to_instrument);
60 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
The Boolean constant false.
Definition: std_expr.h:3072
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
std::list< instructiont > instructionst
Definition: goto_program.h:612
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
bool operator()(goto_modelt &, const std::string &)
insert_final_assert_falset(message_handlert &_message_handler)
mstreamt & error() const
Definition: message.h:391
static eomt eom
Definition: message.h:289
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Symbol Table + CFG.
bool insert_final_assert_false(goto_modelt &goto_model, const std::string &function_to_instrument, message_handlert &message_handler)
Transform a goto program by inserting assert(false) at the end of a given function function_to_instru...
Insert final assert false into a function.
double log(double x)
Definition: math.c:2776
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534