Go to the documentation of this file.
29 case ai_verifier_statust::FALSE_IF_REACHABLE:
30 return "FAILURE (if reachable)";
31 case ai_verifier_statust::NOT_REACHABLE:
32 return "SUCCESS (unreachable)";
43 unknown_json.
push_back(trace_ptr->output_json());
47 false_json.
push_back(trace_ptr->output_json());
52 {
"unknownHistories", unknown_json},
53 {
"falseHistories", false_json},
91 return ai_verifier_statust::NOT_REACHABLE;
101 return ai_verifier_statust::FALSE_IF_REACHABLE;
118 exprt e(assert_location->get_condition());
125 const auto &trace_set = *trace_set_pointer;
127 if(trace_set.size() == 0)
129 status = ai_verifier_statust::NOT_REACHABLE;
131 else if(trace_set.size() == 1)
136 if(
status == ai_verifier_statust::FALSE_IF_REACHABLE)
148 std::size_t unreachable_traces = 0;
149 std::size_t true_traces = 0;
150 std::size_t false_traces = 0;
151 std::size_t unknown_traces = 0;
153 for(
const auto &trace_ptr : trace_set)
160 case ai_verifier_statust::NOT_REACHABLE:
161 ++unreachable_traces;
166 case ai_verifier_statust::FALSE_IF_REACHABLE:
180 if(unknown_traces != 0)
187 if(false_traces == 0)
194 unreachable_traces == trace_set.size(),
195 "All traces must not reach the assertion");
196 status = ai_verifier_statust::NOT_REACHABLE;
211 status = ai_verifier_statust::FALSE_IF_REACHABLE;
237 for(
auto &property : properties)
239 auto &property_status =
property.second.status;
248 property_status = property_statust::PASS;
250 case ai_verifier_statust::FALSE_IF_REACHABLE:
252 property_status = property_statust::FAIL;
254 case ai_verifier_statust::NOT_REACHABLE:
257 property_status = property_statust::NOT_REACHABLE;
271 const std::vector<static_verifier_resultt> &results,
280 .collect<json_arrayt>();
284 const std::vector<static_verifier_resultt> &results,
290 xmlt xml_result{
"cprover"};
291 for(
const auto &result : results)
298 const std::vector<static_verifier_resultt> &results,
304 for(
const auto &result : results)
306 if(last_function_id != result.function_id)
308 if(!last_function_id.
empty())
310 last_function_id = result.function_id;
311 const auto &symbol = ns.
lookup(last_function_id);
312 out <<
"******** Function " << symbol.display_name() <<
'\n';
315 out <<
'[' << result.source_location.get_property_id() <<
']' <<
' ';
317 out << result.source_location;
319 if(!result.source_location.get_comment().empty())
320 out <<
", " << result.source_location.get_comment();
322 out <<
": " <<
as_string(result.status) <<
'\n';
327 const std::vector<static_verifier_resultt> &results,
334 for(
const auto &result : results)
336 if(last_function_id != result.function_id)
338 if(!last_function_id.
empty())
340 last_function_id = result.function_id;
341 const auto &symbol = ns.
lookup(last_function_id);
343 function_file = symbol.location.get_file();
344 if(!function_file.
empty())
345 m.
status() <<
' ' << function_file;
346 if(!symbol.location.get_line().empty())
347 m.
status() <<
':' << symbol.location.get_line();
352 << result.source_location.get_property_id() <<
']'
356 !result.source_location.get_file().empty() &&
357 result.source_location.get_file() != function_file)
362 if(!result.source_location.get_line().empty())
365 if(!result.source_location.get_comment().empty())
370 switch(result.status)
376 case ai_verifier_statust::FALSE_IF_REACHABLE:
380 case ai_verifier_statust::NOT_REACHABLE:
410 std::size_t pass = 0, fail = 0, unknown = 0;
417 std::vector<static_verifier_resultt> results;
421 const auto &symbol = ns.
lookup(f.first);
425 if(!f.second.body.has_assertion())
430 if(!i_it->is_assert())
435 switch(results.back().status)
437 case ai_verifier_statust::NOT_REACHABLE:
443 case ai_verifier_statust::FALSE_IF_REACHABLE:
472 m.
status() << m.
bold <<
"Summary: " << pass <<
" pass, " << fail
473 <<
" fail if reachable, " << unknown <<
" unknown" << m.
reset
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.
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.
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
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)
ai_history_baset::trace_sett unknown_histories
The result of verifying a single assertion As well as the status of the assertion (see above),...
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.
static ai_verifier_statust check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
source_locationt source_location
@ 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)
bool get_bool_option(const std::string &option) const
ai_verifier_statust
An ai_baset contains zero or more histories that reach a location.
This is the basic interface of the abstract interpreter with default implementations of the core func...
ai_history_baset::trace_sett false_histories
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
jsont output_json(void) const
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'.
ai_verifier_statust status
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...
static_verifier_resultt(const ai_baset &ai, goto_programt::const_targett assert_location, irep_idt func_id, const namespacet &ns)
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)
xmlt output_xml(void) const