Go to the documentation of this file.
30 const std::vector<static_verifier_resultt> &results,
38 for(
const auto &result : results)
61 j[
"sourceLocation"] =
json(result.source_location);
68 const std::vector<static_verifier_resultt> &results,
76 for(
const auto &result : results)
101 "description",
id2string(result.source_location.get_comment()));
108 const std::vector<static_verifier_resultt> &results,
114 for(
const auto &result : results)
116 if(last_function_id != result.function_id)
118 if(!last_function_id.
empty())
120 last_function_id = result.function_id;
121 const auto &symbol = ns.
lookup(last_function_id);
122 out <<
"******** Function " << symbol.display_name() <<
'\n';
125 out <<
'[' << result.source_location.get_property_id() <<
']' <<
' ';
127 out << result.source_location;
129 if(!result.source_location.get_comment().empty())
130 out <<
", " << result.source_location.get_comment();
134 switch(result.status)
141 out <<
"Failure (if reachable)";
145 out <<
"Success (unreachable)";
158 const std::vector<static_verifier_resultt> &results,
165 for(
const auto &result : results)
167 if(last_function_id != result.function_id)
169 if(!last_function_id.
empty())
171 last_function_id = result.function_id;
172 const auto &symbol = ns.
lookup(last_function_id);
174 function_file = symbol.location.get_file();
175 if(!function_file.
empty())
176 m.
status() <<
' ' << function_file;
177 if(!symbol.location.get_line().empty())
178 m.
status() <<
':' << symbol.location.get_line();
183 << result.source_location.get_property_id() <<
']'
187 !result.source_location.get_file().empty() &&
188 result.source_location.get_file() != function_file)
193 if(!result.source_location.get_line().empty())
196 if(!result.source_location.get_comment().empty())
201 switch(result.status)
241 std::size_t pass = 0, fail = 0, unknown = 0;
248 std::vector<static_verifier_resultt> results;
252 const auto &symbol = ns.
lookup(f.first);
256 if(!f.second.body.has_assertion())
261 if(!i_it->is_assert())
264 exprt e(i_it->guard);
270 auto &result = results.back();
293 result.source_location = i_it->source_location;
294 result.function_id = f.first;
317 << fail <<
" fail if reachable, "
318 << unknown <<
" unknown"
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_comment() const
json_objectt json(const source_locationt &location)
static const commandt reset
return to default formatting, as defined by the terminal
mstreamt & status() const
static void static_verifier_json(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
bool static_verifier(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Runs the analyzer and then prints out the domain.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
source_locationt source_location
function_mapt function_map
json_objectt & make_object()
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)
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)
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
enum static_verifier_resultt::@0 status
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
The basic interface of an abstract interpreter.
const irep_idt & get_file() const
static const commandt underline
render underlined text
mstreamt & progress() const
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.
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)