cprover
Loading...
Searching...
No Matches
show_on_source.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: goto-analyzer
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "show_on_source.h"
10
11#include <util/message.h>
12
13#ifdef _MSC_VER
14# include <util/unicode.h>
15#endif
16
17#include <analyses/ai.h>
18
19#include <fstream>
20
25{
26 const auto abstract_state = ai.abstract_state_before(loc);
27 if(abstract_state->is_top())
28 return {};
29
30 if(loc->source_location().get_line().empty())
31 return {};
32
33 return loc->source_location().full_path();
34}
35
37static std::set<std::string>
38get_source_files(const goto_modelt &goto_model, const ai_baset &ai)
39{
40 std::set<std::string> files;
41
42 for(const auto &f : goto_model.goto_functions.function_map)
43 {
45 {
46 const auto file = show_location(ai, i_it);
47 if(file.has_value())
48 files.insert(file.value());
49 }
50 }
51
52 return files;
53}
54
57 const std::string &src,
58 const std::string &indent_line,
59 std::ostream &out)
60{
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);
65 std::string src_line;
66 while(std::getline(in, src_line))
67 out << indent << src_line << '\n';
68}
69
72 const std::string &source_file,
73 const goto_modelt &goto_model,
74 const ai_baset &ai,
75 message_handlert &message_handler)
76{
77#ifdef _MSC_VER
78 std::ifstream in(widen(source_file));
79#else
80 std::ifstream in(source_file);
81#endif
82
83 messaget message(message_handler);
84
85 if(!in)
86 {
87 message.warning() << "Failed to open '" << source_file << "'"
89 return;
90 }
91
92 std::map<std::size_t, ai_baset::locationt> line_map;
93
94 // Collect line numbers with non-top abstract states.
95 // We pick the _first_ state for each line.
96 for(const auto &f : goto_model.goto_functions.function_map)
97 {
99 {
100 const auto file = show_location(ai, i_it);
101 if(file.has_value() && file.value() == source_file)
102 {
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;
107 }
108 }
109 }
110
111 // now print file to message handler
112 const namespacet ns(goto_model.symbol_table);
113
114 std::string line;
115 for(std::size_t line_no = 1; std::getline(in, line); line_no++)
116 {
117 const auto map_it = line_map.find(line_no);
118 if(map_it != line_map.end())
119 {
120 auto abstract_state = ai.abstract_state_before(map_it->second);
121 std::ostringstream state_str;
122 abstract_state->output(state_str, ai, ns);
123 if(!state_str.str().empty())
124 {
125 message.result() << messaget::blue;
126 print_with_indent(state_str.str(), line, message.result());
127 message.result() << messaget::reset;
128 }
129 }
130
131 message.result() << line << messaget::eom;
132 }
133}
134
137 const goto_modelt &goto_model,
138 const ai_baset &ai,
139 message_handlert &message_handler)
140{
141 // first gather the source files that have something to show
142 const auto source_files = get_source_files(goto_model, ai);
143
144 // now show file-by-file
145 for(const auto &source_file : source_files)
146 show_on_source(source_file, goto_model, ai, message_handler);
147}
Abstract Interpretation.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:119
goto_programt::const_targett locationt
Definition ai.h:126
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:40
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...
Definition ai.h:223
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static const commandt reset
return to default formatting, as defined by the terminal
Definition message.h:343
mstreamt & warning() const
Definition message.h:404
mstreamt & result() const
Definition message.h:409
static eomt eom
Definition message.h:297
static const commandt blue
render text with blue foreground color
Definition message.h:355
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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
Definition kdev_t.h:19
std::wstring widen(const char *s)
Definition unicode.cpp:49