Go to the documentation of this file.
38 for(
auto &property : properties)
40 auto &property_status =
property.second.status;
42 exprt condition = property_location->get_condition();
43 const std::shared_ptr<const ai_baset::statet> predecessor_state_copy =
60 else if(predecessor_state_copy->
is_bottom())
81 return "FAILURE (if reachable)";
83 return "SUCCESS (unreachable)";
91 const std::vector<static_verifier_resultt> &results,
102 .collect<json_arrayt>();
106 const std::vector<static_verifier_resultt> &results,
112 xmlt xml_result{
"cprover"};
114 for(
const auto &result : results)
118 switch(result.status)
139 "description",
id2string(result.source_location.get_comment()));
146 const std::vector<static_verifier_resultt> &results,
152 for(
const auto &result : results)
154 if(last_function_id != result.function_id)
156 if(!last_function_id.
empty())
158 last_function_id = result.function_id;
159 const auto &symbol = ns.
lookup(last_function_id);
160 out <<
"******** Function " << symbol.display_name() <<
'\n';
163 out <<
'[' << result.source_location.get_property_id() <<
']' <<
' ';
165 out << result.source_location;
167 if(!result.source_location.get_comment().empty())
168 out <<
", " << result.source_location.get_comment();
172 switch(result.status)
179 out <<
"Failure (if reachable)";
183 out <<
"Success (unreachable)";
196 const std::vector<static_verifier_resultt> &results,
203 for(
const auto &result : results)
205 if(last_function_id != result.function_id)
207 if(!last_function_id.
empty())
209 last_function_id = result.function_id;
210 const auto &symbol = ns.
lookup(last_function_id);
212 function_file = symbol.location.get_file();
213 if(!function_file.
empty())
214 m.
status() <<
' ' << function_file;
215 if(!symbol.location.get_line().empty())
216 m.
status() <<
':' << symbol.location.get_line();
221 << result.source_location.get_property_id() <<
']'
225 !result.source_location.get_file().empty() &&
226 result.source_location.get_file() != function_file)
231 if(!result.source_location.get_line().empty())
234 if(!result.source_location.get_comment().empty())
239 switch(result.status)
304 std::size_t pass = 0, fail = 0, unknown = 0;
311 std::vector<static_verifier_resultt> results;
315 const auto &symbol = ns.
lookup(f.first);
319 if(!f.second.body.has_assertion())
324 if(!i_it->is_assert())
327 exprt e(i_it->get_condition());
330 auto &result = results.back();
335 const auto trace_set_pointer =
337 const auto &trace_set = *trace_set_pointer;
339 if(trace_set.size() == 0)
344 else if(trace_set.size() == 1)
349 switch(result.status)
370 std::size_t unreachable_traces = 0;
371 std::size_t true_traces = 0;
372 std::size_t false_traces = 0;
373 std::size_t unknown_traces = 0;
375 for(
const auto &trace_ptr : trace_set)
380 switch(result.status)
383 ++unreachable_traces;
400 if(unknown_traces != 0)
408 if(false_traces == 0)
416 unreachable_traces == trace_set.size(),
417 "All traces must not reach the assertion");
453 result.source_location = i_it->source_location;
454 result.function_id = f.first;
477 << fail <<
" fail if reachable, "
478 << 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
@ FAIL
The property was violated.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
static static_verifier_resultt::statust check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
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
@ NOT_REACHABLE
The property was proven to be unreachable.
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...
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
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)
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)
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.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
@ 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
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
@ PASS
The property was not violated.
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...
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)
enum static_verifier_resultt::statust status
#define forall_goto_program_instructions(it, program)
xmlt & new_element(const std::string &key)