34 std::size_t pass=0, fail=0, unknown=0;
49 if(!f_it->second.body.has_assertion())
54 if(!i_it->is_assert())
85 j[
"sourceLocation"]=
json(i_it->source_location);
99 if(!f_it->second.body.has_assertion())
104 if(!i_it->is_assert())
107 exprt e(i_it->guard);
139 id2string(i_it->source_location.get_comment()));
154 if(!f_it->second.body.has_assertion())
157 out <<
"******** Function " << f_it->first <<
'\n';
161 if(!i_it->is_assert())
164 exprt e(i_it->guard);
169 out <<
'[' << i_it->source_location.get_property_id()
172 out << i_it->source_location;
174 if(!i_it->source_location.get_comment().empty())
175 out <<
", " << i_it->source_location.get_comment();
186 out <<
"Failure (if reachable)";
191 out <<
"Success (unreachable)";
209 << fail <<
" fail if reachable, " 210 << unknown <<
" unknown\n";
const std::string & id2string(const irep_idt &d)
mstreamt & progress() const
symbol_tablet symbol_table
Symbol table.
static mstreamt & eom(mstreamt &m)
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
virtual bool is_bottom() const =0
#define INVARIANT(CONDITION, REASON)
jsont & push_back(const jsont &json)
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
also add
bool get_bool_option(const std::string &option) const
void set_attribute(const std::string &attribute, unsigned value)
xmlt & new_element(const std::string &name)
bool static_verifier(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Runs the analyzer and then prints out the domain.
mstreamt & status() const
The basic interface of an abstract interpreter.
Base class for all expressions.
json_objectt & make_object()
goto_programt coverage_criteriont message_handlert & message_handler
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
goto_functionst goto_functions
GOTO functions.
json_objectt json(const source_locationt &location)