cprover
Loading...
Searching...
No Matches
document_properties.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Subgoal Documentation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "document_properties.h"
13
14#include <fstream>
15
16#include <util/string2int.h>
17
19
20#define MAXWIDTH 62
21
23{
24public:
26 const goto_functionst &_goto_functions,
27 std::ostream &_out):
28 goto_functions(_goto_functions),
29 out(_out),
31 {
32 }
33
34 void html()
35 {
37 doit();
38 }
39
40 void latex()
41 {
43 doit();
44 }
45
46private:
48 std::ostream &out;
49
50 struct linet
51 {
52 std::string text;
54 };
55
56 static void strip_space(std::list<linet> &lines);
57
58 std::string get_code(const source_locationt &source_location);
59
61 {
62 std::set<irep_idt> comment_set;
63 };
64
65 enum { HTML, LATEX } format;
66
67 void doit();
68};
69
70void document_propertiest::strip_space(std::list<linet> &lines)
71{
72 unsigned strip=50;
73
74 for(std::list<linet>::const_iterator it=lines.begin();
75 it!=lines.end(); it++)
76 {
77 for(std::size_t j=0; j<strip && j<it->text.size(); j++)
78 if(it->text[j]!=' ')
79 {
80 strip=j;
81 break;
82 }
83 }
84
85 if(strip!=0)
86 {
87 for(std::list<linet>::iterator it=lines.begin();
88 it!=lines.end(); it++)
89 {
90 if(it->text.size()>=strip)
91 it->text=std::string(it->text, strip, std::string::npos);
92
93 if(it->text.size()>=MAXWIDTH)
94 it->text=std::string(it->text, 0, MAXWIDTH);
95 }
96 }
97}
98
99std::string escape_latex(const std::string &s, bool alltt)
100{
101 std::string dest;
102
103 for(std::size_t i=0; i<s.size(); i++)
104 {
105 if(s[i]=='\\' || s[i]=='{' || s[i]=='}')
106 dest+="\\";
107
108 if(!alltt &&
109 (s[i]=='_' || s[i]=='$' || s[i]=='~' ||
110 s[i]=='^' || s[i]=='%' || s[i]=='#' ||
111 s[i]=='&'))
112 dest+="\\";
113
114 dest+=s[i];
115 }
116
117 return dest;
118}
119
120std::string escape_html(const std::string &s)
121{
122 std::string dest;
123
124 for(std::size_t i=0; i<s.size(); i++)
125 {
126 switch(s[i])
127 {
128 case '&': dest+="&amp;"; break;
129 case '<': dest+="&lt;"; break;
130 case '>': dest+="&gt;"; break;
131 default: dest+=s[i];
132 }
133 }
134
135 return dest;
136}
137
138bool is_empty(const std::string &s)
139{
140 for(std::size_t i=0; i<s.size(); i++)
141 if(isgraph(s[i]))
142 return false;
143
144 return true;
145}
146
147std::string
149{
150 const irep_idt &file=source_location.get_file();
151 const irep_idt &source_line = source_location.get_line();
152
153 if(file.empty() || source_line.empty())
154 return "";
155
156 std::ifstream in(id2string(file));
157
158 std::string dest;
159
160 if(!in)
161 {
162 dest+="ERROR: unable to open ";
163 dest+=id2string(file);
164 dest+="\n";
165 return dest;
166 }
167
168 int line_int = unsafe_string2int(id2string(source_line));
169
170 int line_start=line_int-3,
171 line_end=line_int+3;
172
173 if(line_start<=1)
174 line_start=1;
175
176 // skip line_start-1 lines
177
178 for(int l=0; l<line_start-1; l++)
179 {
180 std::string tmp;
181 std::getline(in, tmp);
182 }
183
184 // read till line_end
185
186 std::list<linet> lines;
187
188 for(int l=line_start; l<=line_end && in; l++)
189 {
190 lines.push_back(linet());
191
192 std::string &line=lines.back().text;
193 std::getline(in, line);
194
195 if(!line.empty() && line[line.size()-1]=='\r')
196 line.resize(line.size()-1);
197
198 lines.back().line_number=l;
199 }
200
201 // remove empty lines at the end and at the beginning
202
203 for(std::list<linet>::iterator it=lines.begin();
204 it!=lines.end();)
205 {
206 if(is_empty(it->text))
207 it=lines.erase(it);
208 else
209 break;
210 }
211
212 for(std::list<linet>::iterator it=lines.end();
213 it!=lines.begin();)
214 {
215 it--;
216
217 if(is_empty(it->text))
218 it=lines.erase(it);
219 else
220 break;
221 }
222
223 // strip space
224 strip_space(lines);
225
226 // build dest
227
228 for(std::list<linet>::iterator it=lines.begin();
229 it!=lines.end(); it++)
230 {
231 std::string line_no=std::to_string(it->line_number);
232
233 std::string tmp;
234
235 switch(format)
236 {
237 case LATEX:
238 while(line_no.size()<4)
239 line_no=" "+line_no;
240
241 line_no+" ";
242
243 tmp+=escape_latex(it->text, true);
244
245 if(it->line_number==line_int)
246 tmp="{\\ttb{}"+tmp+"}";
247
248 break;
249
250 case HTML:
251 while(line_no.size()<4)
252 line_no="&nbsp;"+line_no;
253
254 line_no+"&nbsp;&nbsp;";
255
256 tmp+=escape_html(it->text);
257
258 if(it->line_number==line_int)
259 tmp="<em>"+tmp+"</em>";
260
261 break;
262 }
263
264 dest+=tmp+"\n";
265 }
266
267 return dest;
268}
269
271{
272 typedef std::map<source_locationt, doc_claimt> claim_sett;
273 claim_sett claim_set;
274
275 for(const auto &gf_entry : goto_functions.function_map)
276 {
277 const goto_programt &goto_program = gf_entry.second.body;
278
279 for(const auto &instruction : goto_program.instructions)
280 {
281 if(instruction.is_assert())
282 {
283 const auto &source_location = instruction.source_location();
284 source_locationt new_source_location;
285
286 new_source_location.set_file(source_location.get_file());
287 new_source_location.set_line(source_location.get_line());
288 new_source_location.set_function(source_location.get_function());
289
290 claim_set[new_source_location].comment_set.insert(
291 source_location.get_comment());
292 }
293 }
294 }
295
296 for(claim_sett::const_iterator it=claim_set.begin();
297 it!=claim_set.end(); it++)
298 {
299 const source_locationt &source_location=it->first;
300
301 std::string code = get_code(source_location);
302
303 switch(format)
304 {
305 case LATEX:
306 out << "\\claimlocation{File "
307 << escape_latex(source_location.get_string("file"), false)
308 << " function "
309 << escape_latex(source_location.get_string("function"), false)
310 << "}\n";
311
312 out << '\n';
313
314 for(std::set<irep_idt>::const_iterator
315 s_it=it->second.comment_set.begin();
316 s_it!=it->second.comment_set.end();
317 s_it++)
318 out << "\\claim{" << escape_latex(id2string(*s_it), false)
319 << "}\n";
320
321 out << '\n';
322
323 out << "\\begin{alltt}\\claimcode\n"
324 << code
325 << "\\end{alltt}\n";
326
327 out << '\n';
328 out << '\n';
329 break;
330
331 case HTML:
332 out << "<div class=\"claim\">\n"
333 << "<div class=\"location\">File "
334 << escape_html(source_location.get_string("file"))
335 << " function "
336 << escape_html(source_location.get_string("function"))
337 << "</div>\n";
338
339 out << '\n';
340
341 for(std::set<irep_idt>::const_iterator
342 s_it=it->second.comment_set.begin();
343 s_it!=it->second.comment_set.end();
344 s_it++)
345 out << "<div class=\"description\">\n"
346 << escape_html(id2string(*s_it)) << '\n'
347 << "</div>\n";
348
349 out << '\n';
350
351 out << "<div class=\"code\">\n"
352 << code
353 << "</div> <!-- code -->\n";
354
355 out << "</div> <!-- claim -->\n";
356 out << '\n';
357 break;
358 }
359 }
360}
361
363 const goto_modelt &goto_model,
364 std::ostream &out)
365{
366 document_propertiest(goto_model.goto_functions, out).html();
367}
368
370 const goto_modelt &goto_model,
371 std::ostream &out)
372{
373 document_propertiest(goto_model.goto_functions, out).latex();
374}
std::string get_code(const source_locationt &source_location)
document_propertiest(const goto_functionst &_goto_functions, std::ostream &_out)
static void strip_space(std::list< linet > &lines)
enum document_propertiest::@4 format
const goto_functionst & goto_functions
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
A collection of goto functions.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
const std::string & get_string(const irep_idt &name) const
Definition: irep.h:409
const irep_idt & get_file() const
const irep_idt & get_line() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
bool is_empty(const std::string &s)
std::string escape_latex(const std::string &s, bool alltt)
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
std::string escape_html(const std::string &s)
#define MAXWIDTH
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
Documentation of Properties.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:30
Definition: kdev_t.h:19