cprover
property_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Property Checker Interface
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "property_checker.h"
13 
15 {
16  switch(result)
17  {
18  case property_checkert::resultt::PASS: return "OK";
19  case property_checkert::resultt::FAIL: return "FAILURE";
20  case property_checkert::resultt::ERROR: return "ERROR";
21  case property_checkert::resultt::UNKNOWN: return "UNKNOWN";
22  }
23 
24  return "";
25 }
26 
28  message_handlert &_message_handler):
29  messaget(_message_handler)
30 {
31 }
32 
34  const goto_functionst &goto_functions)
35 {
36  forall_goto_functions(it, goto_functions)
37  if(!it->second.is_inlined() ||
38  it->first==goto_functions.entry_point())
39  {
40  const goto_programt &goto_program=it->second.body;
41 
42  forall_goto_program_instructions(i_it, goto_program)
43  {
44  if(!i_it->is_assert())
45  continue;
46 
47  const source_locationt &source_location=i_it->source_location;
48 
49  irep_idt property_id=source_location.get_property_id();
50 
51  property_statust &property_status=property_map[property_id];
52  property_status.result=resultt::UNKNOWN;
53  property_status.location=i_it;
54  }
55  }
56 }
void initialize_property_map(const goto_functionst &)
static std::string as_string(resultt)
A collection of goto functions.
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Property Checker Interface.
property_mapt property_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
mstreamt & result() const
Definition: message.h:396
goto_programt::const_targett location
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804