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" virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
const std::string & id2string(const irep_idt &d)
static const commandt bold
render text with bold font
mstreamt & progress() const
bool is_false() const
Return whether the expression is a constant representing false.
static void static_verifier_xml(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
bool is_true() const
Return whether the expression is a constant representing true.
function_mapt function_map
enum static_verifier_resultt::@0 status
symbol_tablet symbol_table
Symbol table.
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...
static const commandt reset
return to default formatting, as defined by the terminal
virtual bool is_bottom() const =0
jsont & push_back(const jsont &json)
static const commandt underline
render underlined text
const irep_idt & get_line() const
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
source_locationt source_location
bool get_bool_option(const std::string &option) const
void set_attribute(const std::string &attribute, unsigned value)
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...
static void static_verifier_json(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
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.
static void static_verifier_text(const std::vector< static_verifier_resultt > &results, const namespacet &ns, std::ostream &out)
static const commandt faint
render text with faint font
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.
const irep_idt & get_file() const
mstreamt & result() const
xmlt & new_element(const std::string &key)
mstreamt & status() const
The basic interface of an abstract interpreter.
Base class for all expressions.
source_locationt source_location
json_objectt & make_object()
const irep_idt & get_comment() const
static const commandt green
render text with green foreground color
#define forall_goto_program_instructions(it, program)
static const commandt yellow
render text with yellow foreground color
goto_functionst goto_functions
GOTO functions.
json_objectt json(const source_locationt &location)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
static void static_verifier_console(const std::vector< static_verifier_resultt > &results, const namespacet &ns, messaget &m)