Go to the documentation of this file.
39 if(ins.source_location.get_property_id() == property)
41 return ins.source_location;
76 xmlt xml_property(
"property");
81 property_l=
xml(source_location);
87 msg.
result() << xml_property;
96 msg.
result() <<
"Property " << property_id <<
":\n";
99 <<
" " << description <<
'\n'
100 <<
" " <<
from_expr(ns, identifier, ins.guard) <<
'\n';
137 json_property[
"coveredLines"] =
139 json_property[
"sourceLocation"]=
json(source_location);
140 json_property[
"description"] =
json_stringt(description);
141 json_property[
"expression"]=
158 json_result[
"properties"] = json_properties;
159 msg.
result() << json_result;
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
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_comment() const
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
json_objectt json(const source_locationt &location)
void show_properties_json(const namespacet &ns, message_handlert &message_handler, const goto_functionst &goto_functions)
std::string comment(const rw_set_baset::entryt &entry, bool write)
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
xmlt xml(const source_locationt &location)
function_mapt function_map
json_objectt & make_object()
#define UNREACHABLE
This should be used to mark dead code.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
mstreamt & result() const
const std::string & id2string(const irep_idt &d)
source_locationt source_location
const irep_idt & get_basic_block_covered_lines() const
nonstd::optional< T > optionalt
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
void set_attribute(const std::string &attribute, unsigned value)
optionalt< 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.
A generic container class for the GOTO intermediate representation of one function.
symbol_tablet symbol_table
Symbol table.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
jsont & push_back(const jsont &json)
xmlt & new_element(const std::string &key)