28 ns(_goto_model.symbol_table),
52 status() <<
"performing interval analysis" <<
eom;
77 unsigned pass=0, fail=0, unknown=0;
81 if(!f_it->second.body.has_assertion())
84 if(f_it->first==
"__actual_thread_spawn")
87 status() <<
"******** Function " << f_it->first <<
eom;
91 if(!i_it->is_assert())
100 if(!i_it->source_location.get_comment().empty())
105 else if(
r.is_false())
113 else if(
r.is_false())
122 status() <<
"SUMMARY: " << pass <<
" pass, " << fail <<
" fail, " 123 << unknown <<
" unknown\n";
132 if(!f_it->second.body.has_assertion())
135 if(f_it->first==
"__actual_thread_spawn")
140 if(!i_it->is_assert())
149 else if(
r.is_false())
157 i_it->source_location.get_comment()));
161 std::ofstream out(file_name);
164 error() <<
"failed to open JSON output file `" 165 << file_name <<
"'" <<
eom;
169 status() <<
"Writing report to `" << file_name <<
"'" <<
eom;
179 if(!f_it->second.body.has_assertion())
182 if(f_it->first==
"__actual_thread_spawn")
187 if(!i_it->is_assert())
196 else if(
r.is_false())
204 "description",
id2string(i_it->source_location.get_comment()));
208 std::ofstream out(file_name);
211 error() <<
"failed to open XML output file `" 212 << file_name <<
"'" <<
eom;
216 status() <<
"Writing report to `" << file_name <<
"'" <<
eom;
226 goto_model, options, message_handler)();
const std::string & id2string(const irep_idt &d)
void assume(const exprt &, const namespacet &)
static mstreamt & eom(mstreamt &m)
void json_report(const std::string &)
jsont & push_back(const jsont &json)
instructionst::const_iterator const_targett
void show_intervals(const goto_modelt &goto_model, std::ostream &out)
source_locationt source_location
const std::string get_option(const std::string &option) const
void set_attribute(const std::string &attribute, unsigned value)
tvt eval(goto_programt::const_targett)
ait< interval_domaint > interval_analysis
xmlt & new_element(const std::string &name)
void xml_report(const std::string &)
Base class for all expressions.
bool static_analyzer(const goto_modelt &goto_model, const optionst &options, message_handlert &message_handler)
json_objectt & make_object()
const irep_idt & get_comment() const
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
#define forall_goto_program_instructions(it, program)
const goto_functionst & goto_functions
void interval_analysis(const namespacet &ns, goto_functionst &goto_functions)
static_analyzert(const goto_modelt &_goto_model, const optionst &_options, message_handlert &_message_handler)