27 if(abstract_state->is_top())
30 if(loc->source_location.get_line().empty())
33 return loc->source_location.full_path();
37 static std::set<std::string>
40 std::set<std::string> files;
48 files.insert(
file.value());
57 const std::string &src,
58 const std::string &indent_line,
61 const std::size_t p = indent_line.find_first_not_of(
" \t");
62 const std::string indent =
63 p == std::string::npos ? std::string() : std::string(indent_line, 0, p);
64 std::istringstream in(src);
66 while(std::getline(in, src_line))
67 out << indent << src_line <<
'\n';
72 const std::string &source_file,
78 std::ifstream in(
widen(source_file));
80 std::ifstream in(source_file);
87 message.
warning() <<
"Failed to open '" << source_file <<
"'"
92 std::map<std::size_t, ai_baset::locationt> line_map;
101 if(
file.has_value() &&
file.value() == source_file)
103 const std::size_t line_no =
104 stoull(
id2string(i_it->source_location.get_line()));
105 if(line_map.find(line_no) == line_map.end())
106 line_map[line_no] = i_it;
115 for(std::size_t line_no = 1; std::getline(in, line); line_no++)
117 const auto map_it = line_map.find(line_no);
118 if(map_it != line_map.end())
121 std::ostringstream state_str;
122 abstract_state->output(state_str, ai, ns);
123 if(!state_str.str().empty())
145 for(
const auto &source_file : source_files)
This is the basic interface of the abstract interpreter with default implementations of the core func...
goto_programt::const_targett locationt
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...
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
static const commandt reset
return to default formatting, as defined by the terminal
mstreamt & result() const
static const commandt blue
render text with blue foreground color
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
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
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
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
std::wstring widen(const char *s)