Go to the documentation of this file.
25 if(abstract_state->is_top())
28 if(loc->source_location.get_line().empty())
31 return loc->source_location.full_path();
35 static std::set<std::string>
38 std::set<std::string> files;
46 files.insert(
file.value());
55 const std::string &src,
56 const std::string &indent_line,
59 const std::size_t p = indent_line.find_first_not_of(
" \t");
60 const std::string indent =
61 p == std::string::npos ? std::string() : std::string(indent_line, 0, p);
62 std::istringstream in(src);
64 while(std::getline(in, src_line))
65 out << indent << src_line <<
'\n';
70 const std::string &source_file,
76 std::ifstream in(
widen(source_file));
78 std::ifstream in(source_file);
85 message.warning() <<
"Failed to open '" << source_file <<
"'"
90 std::map<std::size_t, ai_baset::locationt> line_map;
99 if(
file.has_value() &&
file.value() == source_file)
101 const std::size_t line_no =
102 stoull(
id2string(i_it->source_location.get_line()));
103 if(line_map.find(line_no) == line_map.end())
104 line_map[line_no] = i_it;
113 for(std::size_t line_no = 1; std::getline(in, line); line_no++)
115 const auto map_it = line_map.find(line_no);
116 if(map_it != line_map.end())
119 std::ostringstream state_str;
120 abstract_state->output(state_str, ai, ns);
121 if(!state_str.str().empty())
143 for(
const auto &source_file : source_files)
Class that provides messages with a built-in verbosity 'level'.
static const commandt reset
return to default formatting, as defined by the terminal
goto_programt::const_targett locationt
static std::set< std::string > get_source_files(const goto_modelt &goto_model, const ai_baset &ai)
get the source files with non-top abstract states
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...
static optionalt< std::string > show_location(const ai_baset &ai, ai_baset::locationt loc)
get the name of the file referred to at a location loc, if any
static void print_with_indent(const std::string &src, const std::string &indent_line, std::ostream &out)
print a string with indent to match given sample line
function_mapt function_map
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.
const std::string & id2string(const irep_idt &d)
std::wstring widen(const char *s)
nonstd::optional< T > optionalt
goto_functionst goto_functions
GOTO functions.
This is the basic interface of the abstract interpreter with default implementations of the core func...
void show_on_source(const std::string &source_file, const goto_modelt &goto_model, const ai_baset &ai, message_handlert &message_handler)
output source code annotated with abstract states for given file
symbol_tablet symbol_table
Symbol table.
static const commandt blue
render text with blue foreground color
#define forall_goto_program_instructions(it, program)