Go to the documentation of this file.
37 if(ins.source_location.get_property_id() == property)
39 return ins.source_location;
80 property_l=
xml(source_location);
82 xml_property.new_element(
"description").data=
id2string(description);
83 xml_property.new_element(
"expression").data =
84 from_expr(ns, identifier, ins.get_condition());
86 msg.
result() << xml_property;
95 msg.
result() <<
"Property " << property_id <<
":\n";
98 <<
" " << description <<
'\n'
99 <<
" " <<
from_expr(ns, identifier, ins.get_condition())
134 {
"sourceLocation",
json(source_location)},
140 json_property[
"coveredLines"] =
143 json_properties.
push_back(std::move(json_property));
158 json_objectt json_result{{
"properties", json_properties}};
159 msg.
result() << json_result;
172 show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body);
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'.
#define UNREACHABLE
This should be used to mark dead code.
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
void show_properties_json(const namespacet &ns, message_handlert &message_handler, const goto_functionst &goto_functions)
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
function_mapt function_map
virtual uit get_ui() const
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)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
source_locationt source_location
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
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.
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.
Goto Programs with Functions.
A generic container class for the GOTO intermediate representation of one function.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
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)