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;
223 status = ai_verifier_statust::FALSE_IF_REACHABLE;
241 for(
auto &property : properties)
243 auto &property_status =
property.second.status;
252 property_status = property_statust::PASS;
254 case ai_verifier_statust::FALSE_IF_REACHABLE:
256 property_status = property_statust::FAIL;
258 case ai_verifier_statust::NOT_REACHABLE:
261 property_status = property_statust::NOT_REACHABLE;
275 const std::vector<static_verifier_resultt> &results,
284 .collect<json_arrayt>();
288 const std::vector<static_verifier_resultt> &results,
294 xmlt xml_result{
"cprover"};
295 for(
const auto &result : results)
302 const std::vector<static_verifier_resultt> &results,
308 for(
const auto &result : results)
310 if(last_function_id != result.function_id)
312 if(!last_function_id.
empty())
314 last_function_id = result.function_id;
315 const auto &symbol = ns.
lookup(last_function_id);
316 out <<
"******** Function " << symbol.display_name() <<
'\n';
319 out <<
'[' << result.source_location.get_property_id() <<
']' <<
' ';
321 out << result.source_location;
323 if(!result.source_location.get_comment().empty())
324 out <<
", " << result.source_location.get_comment();
326 out <<
": " <<
as_string(result.status) <<
'\n';
331 const std::vector<static_verifier_resultt> &results,
338 for(
const auto &result : results)
340 if(last_function_id != result.function_id)
342 if(!last_function_id.
empty())
344 last_function_id = result.function_id;
345 const auto &symbol = ns.
lookup(last_function_id);
347 function_file = symbol.location.get_file();
348 if(!function_file.
empty())
349 m.
status() <<
' ' << function_file;
350 if(!symbol.location.get_line().empty())
351 m.
status() <<
':' << symbol.location.get_line();
356 << result.source_location.get_property_id() <<
']'
360 !result.source_location.get_file().empty() &&
361 result.source_location.get_file() != function_file)
366 if(!result.source_location.get_line().empty())
369 if(!result.source_location.get_comment().empty())
374 switch(result.status)
380 case ai_verifier_statust::FALSE_IF_REACHABLE:
384 case ai_verifier_statust::NOT_REACHABLE:
414 std::size_t pass = 0, fail = 0, unknown = 0;
421 std::vector<static_verifier_resultt> results;
425 const auto &symbol = ns.
lookup(f.first);
429 if(!f.second.body.has_assertion())
434 if(!i_it->is_assert())
439 switch(results.back().status)
441 case ai_verifier_statust::NOT_REACHABLE:
447 case ai_verifier_statust::FALSE_IF_REACHABLE:
478 << fail <<
" fail if reachable, "
479 << 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.
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