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)
133 exprt e(assert_location->get_condition());
140 const auto &trace_set = *trace_set_pointer;
142 if(trace_set.size() == 0)
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)
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");
258 for(
auto &property : properties)
260 auto &property_status =
property.second.status;
265 switch(result.status)
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)
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)
495 << fail <<
" fail if reachable, "
496 << unknown <<
" unknown"
Abstract interface to eager or lazy GOTO models.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
This is the basic interface of the abstract interpreter with default implementations of the core func...
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const
Returns all of the histories that have reached the start of the instruction.
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...
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
virtual bool is_bottom() const =0
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
std::set< trace_ptrt, compare_historyt > trace_sett
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
instructionst::const_iterator const_targett
jsont & push_back(const jsont &json)
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
static const commandt yellow
render text with yellow foreground color
static const commandt reset
return to default formatting, as defined by the terminal
mstreamt & status() const
static const commandt green
render text with green foreground color
static const commandt faint
render text with faint font
static const commandt bold
render text with bold font
static const commandt underline
render underlined text
mstreamt & progress() const
mstreamt & result() const
static const commandt red
render text with red foreground color
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().
bool get_bool_option(const std::string &option) const
const irep_idt & get_comment() const
const irep_idt & get_line() const
const irep_idt & get_file() const
void set_attribute(const std::string &attribute, unsigned value)
xmlt & new_element(const std::string &key)
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
@ UNKNOWN
The checker was unable to determine the status of the property.
@ NOT_REACHABLE
The property was proven to be unreachable.
@ PASS
The property was not violated.
@ FAIL
The property was violated.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
static void static_verifier_console(const std::vector< static_verifier_resultt > &results, const namespacet &ns, messaget &m)
static void static_verifier_xml(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
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.
static const char * message(const statust &status)
Makes a status message string from a status.
static statust check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
static void static_verifier_text(const std::vector< static_verifier_resultt > &results, const namespacet &ns, std::ostream &out)
static void static_verifier_json(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
jsont output_json(void) const
source_locationt source_location
ai_history_baset::trace_sett unknown_histories
ai_history_baset::trace_sett false_histories
xmlt output_xml(void) const