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"]=
155 if(!fct.second.is_inlined())
159 json_result[
"properties"] = json_properties;
160 msg.
result() << json_result;
173 if(!fct.second.is_inlined())
const std::string & id2string(const irep_idt &d)
std::string comment(const rw_set_baset::entryt &entry, bool write)
Goto Programs with Functions.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
static mstreamt & eom(mstreamt &m)
xmlt xml(const source_locationt &location)
jsont & push_back(const jsont &json)
source_locationt source_location
nonstd::optional< T > optionalt
instructionst instructions
The list of instructions in the goto program.
void set_attribute(const std::string &attribute, unsigned value)
const irep_idt & get_basic_block_covered_lines() const
xmlt & new_element(const std::string &name)
A generic container class for the GOTO intermediate representation of one function.
mstreamt & result() const
goto_programt & goto_program
json_objectt & make_object()
goto_programt coverage_criteriont message_handlert & message_handler
const irep_idt & get_comment() const
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
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
goto_functionst goto_functions
GOTO functions.
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. ...
json_objectt json(const source_locationt &location)
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)