22std::optional<source_locationt>
33 if(
ins.source_location().get_property_id() ==
property)
35 return ins.source_location();
110 msg.result() <<
"Property " << property_id <<
":\n";
112 msg.result() <<
" " <<
ins.source_location() <<
'\n'
113 <<
" " << description <<
'\n'
149 {
"sourceLocation",
json(source_location)},
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_property_id() const
const irept & get_basic_block_source_lines() const
const irep_idt & get_property_class() const
const irep_idt & get_comment() const
virtual uit get_ui() const
void set_attribute(const std::string &attribute, unsigned value)
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void show_properties_json(const namespacet &ns, message_handlert &message_handler, const goto_functionst &goto_functions)
void convert_properties_json(json_arrayt &json_properties, const namespacet &ns, const irep_idt &identifier, const goto_programt &goto_program)
Collects the properties in the goto program into a json_arrayt
std::optional< source_locationt > find_property(const irep_idt &property, const goto_functionst &goto_functions)
Returns a source_locationt that corresponds to the property given by an irep_idt.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
#define UNREACHABLE
This should be used to mark dead code.