Go to the documentation of this file.
34 return "FAILURE (if reachable)";
36 return "SUCCESS (unreachable)";
54 for(
const auto &trace_ptr : this->unknown_histories)
55 unknown_json.
push_back(trace_ptr->output_json());
58 for(
const auto &trace_ptr : this->false_histories)
59 false_json.
push_back(trace_ptr->output_json());
63 {
"sourceLocation",
json(this->source_location)},
64 {
"unknownHistories", unknown_json},
65 {
"falseHistories", false_json},
88 for(
const auto &trace_ptr : this->unknown_histories)
92 for(
const auto &trace_ptr : this->false_histories)
104 return statust::BOTTOM;
133 exprt e(assert_location->get_condition());
140 const auto &trace_set = *trace_set_pointer;
142 if(trace_set.size() == 0)
144 result.
status = statust::BOTTOM;
146 else if(trace_set.size() == 1)
163 std::size_t unreachable_traces = 0;
164 std::size_t true_traces = 0;
165 std::size_t false_traces = 0;
166 std::size_t unknown_traces = 0;
168 for(
const auto &trace_ptr : trace_set)
175 case statust::BOTTOM:
176 ++unreachable_traces;
195 if(unknown_traces != 0)
202 if(false_traces == 0)
209 unreachable_traces == trace_set.size(),
210 "All traces must not reach the assertion");
211 result.
status = statust::BOTTOM;
258 for(
auto &property : properties)
260 auto &property_status =
property.second.status;
265 switch(result.status)
269 property_status = property_statust::PASS;
273 property_status = property_statust::FAIL;
275 case statust::BOTTOM:
278 property_status = property_statust::NOT_REACHABLE;
292 const std::vector<static_verifier_resultt> &results,
301 .collect<json_arrayt>();
305 const std::vector<static_verifier_resultt> &results,
311 xmlt xml_result{
"cprover"};
312 for(
const auto &result : results)
319 const std::vector<static_verifier_resultt> &results,
325 for(
const auto &result : results)
327 if(last_function_id != result.function_id)
329 if(!last_function_id.
empty())
331 last_function_id = result.function_id;
332 const auto &symbol = ns.
lookup(last_function_id);
333 out <<
"******** Function " << symbol.display_name() <<
'\n';
336 out <<
'[' << result.source_location.get_property_id() <<
']' <<
' ';
338 out << result.source_location;
340 if(!result.source_location.get_comment().empty())
341 out <<
", " << result.source_location.get_comment();
343 out <<
": " <<
message(result.status) <<
'\n';
348 const std::vector<static_verifier_resultt> &results,
355 for(
const auto &result : results)
357 if(last_function_id != result.function_id)
359 if(!last_function_id.
empty())
361 last_function_id = result.function_id;
362 const auto &symbol = ns.
lookup(last_function_id);
364 function_file = symbol.location.get_file();
365 if(!function_file.
empty())
366 m.
status() <<
' ' << function_file;
367 if(!symbol.location.get_line().empty())
368 m.
status() <<
':' << symbol.location.get_line();
373 << result.source_location.get_property_id() <<
']'
377 !result.source_location.get_file().empty() &&
378 result.source_location.get_file() != function_file)
383 if(!result.source_location.get_line().empty())
386 if(!result.source_location.get_comment().empty())
391 switch(result.status)
401 case statust::BOTTOM:
431 std::size_t pass = 0, fail = 0, unknown = 0;
438 std::vector<static_verifier_resultt> results;
442 const auto &symbol = ns.
lookup(f.first);
446 if(!f.second.body.has_assertion())
451 if(!i_it->is_assert())
456 switch(results.back().status)
458 case statust::BOTTOM:
495 << fail <<
" fail if reachable, "
496 << unknown <<
" unknown"
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.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
const irep_idt & get_comment() const
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
static const commandt reset
return to default formatting, as defined by the terminal
void static_verifier(const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
Use the information from the abstract interpreter to fill out the statuses of the passed properties.
mstreamt & status() const
static void static_verifier_json(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
Base class for all expressions.
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
bool is_true() const
Return whether the expression is a constant representing true.
source_locationt source_location
function_mapt function_map
virtual bool is_bottom() const =0
const irep_idt & get_line() const
bool is_false() const
Return whether the expression is a constant representing false.
static statust check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
static const commandt green
render text with green foreground color
std::set< trace_ptrt, compare_historyt > trace_sett
static const char * message(const statust &status)
Makes a status message string from a status.
mstreamt & result() const
static const commandt faint
render text with faint font
static const commandt bold
render text with bold font
static const commandt yellow
render text with yellow foreground color
const std::string & id2string(const irep_idt &d)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
static void static_verifier_text(const std::vector< static_verifier_resultt > &results, const namespacet &ns, std::ostream &out)
source_locationt source_location
static void static_verifier_console(const std::vector< static_verifier_resultt > &results, const namespacet &ns, messaget &m)
#define PRECONDITION(CONDITION)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const
Returns all of the histories that have reached the start of the instruction.
ai_history_baset::trace_sett unknown_histories
Ranges: pair of begin and end iterators, which can be initialized from containers,...
xmlt output_xml(void) const
@ UNKNOWN
The checker was unable to determine the status of the property.
static const commandt red
render text with red foreground color
goto_functionst goto_functions
GOTO functions.
void set_attribute(const std::string &attribute, unsigned value)
ai_history_baset::trace_sett false_histories
bool get_bool_option(const std::string &option) const
This is the basic interface of the abstract interpreter with default implementations of the core func...
const irep_idt & get_file() const
static const commandt underline
render underlined text
instructionst::const_iterator const_targett
Abstract interface to eager or lazy GOTO models.
mstreamt & progress() const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
jsont output_json(void) const
symbol_tablet symbol_table
Symbol table.
ranget< iteratort > make_range(iteratort begin, iteratort end)
static void static_verifier_xml(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
jsont & push_back(const jsont &json)
#define forall_goto_program_instructions(it, program)
xmlt & new_element(const std::string &key)