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)
const std::string & id2string(const irep_idt &d)
goto_programt::const_targett locationt
std::wstring widen(const char *s)
static const commandt blue
render text with blue foreground color
function_mapt function_map
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
mstreamt & warning() const
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
nonstd::optional< T > optionalt
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Class that provides messages with a built-in verbosity 'level'.
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
mstreamt & result() const
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
The basic interface of an abstract interpreter.
#define forall_goto_program_instructions(it, program)
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
goto_functionst goto_functions
GOTO functions.