CBMC
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:
27 std::ostream &_out):
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
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
169
170 int line_start=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
225
226 // build dest
227
228 std::size_t max_line_number_width = 0;
229 if(!lines.empty())
230 {
231 max_line_number_width = std::to_string(lines.back().line_number).size();
232 }
233 for(std::list<linet>::iterator it=lines.begin();
234 it!=lines.end(); it++)
235 {
236 std::string line_no=std::to_string(it->line_number);
237
238 std::string tmp;
239
240 switch(format)
241 {
242 case LATEX:
243 while(line_no.size() < max_line_number_width)
244 line_no=" "+line_no;
245
246 line_no += " ";
247
248 tmp+=escape_latex(it->text, true);
249
250 if(it->line_number==line_int)
251 tmp="{\\ttb{}"+tmp+"}";
252
253 break;
254
255 case HTML:
256 while(line_no.size() < max_line_number_width)
257 line_no="&nbsp;"+line_no;
258
259 line_no += "&nbsp;&nbsp;";
260
261 tmp+=escape_html(it->text);
262
263 if(it->line_number==line_int)
264 tmp="<em>"+tmp+"</em>";
265
266 break;
267 }
268
269 dest += line_no + tmp + "\n";
270 }
271
272 return dest;
273}
274
276{
277 typedef std::map<source_locationt, doc_claimt> claim_sett;
279
280 for(const auto &gf_entry : goto_functions.function_map)
281 {
282 const goto_programt &goto_program = gf_entry.second.body;
283
284 for(const auto &instruction : goto_program.instructions)
285 {
286 if(instruction.is_assert())
287 {
288 const auto &source_location = instruction.source_location();
290
291 new_source_location.set_file(source_location.get_file());
292 new_source_location.set_line(source_location.get_line());
293 new_source_location.set_function(source_location.get_function());
294
295 claim_set[new_source_location].comment_set.insert(
296 source_location.get_comment());
297 }
298 }
299 }
300
301 for(claim_sett::const_iterator it=claim_set.begin();
302 it!=claim_set.end(); it++)
303 {
304 const source_locationt &source_location=it->first;
305
306 std::string code = get_code(source_location);
307
308 switch(format)
309 {
310 case LATEX:
311 out << "\\claimlocation{File "
312 << escape_latex(source_location.get_string("file"), false)
313 << " function "
314 << escape_latex(source_location.get_string("function"), false)
315 << "}\n";
316
317 out << '\n';
318
319 for(std::set<irep_idt>::const_iterator
320 s_it=it->second.comment_set.begin();
321 s_it!=it->second.comment_set.end();
322 s_it++)
323 out << "\\claim{" << escape_latex(id2string(*s_it), false)
324 << "}\n";
325
326 out << '\n';
327
328 out << "\\begin{alltt}\\claimcode\n"
329 << code
330 << "\\end{alltt}\n";
331
332 out << '\n';
333 out << '\n';
334 break;
335
336 case HTML:
337 out << "<div class=\"claim\">\n"
338 << "<div class=\"location\">File "
339 << escape_html(source_location.get_string("file"))
340 << " function "
341 << escape_html(source_location.get_string("function"))
342 << "</div>\n";
343
344 out << '\n';
345
346 for(std::set<irep_idt>::const_iterator
347 s_it=it->second.comment_set.begin();
348 s_it!=it->second.comment_set.end();
349 s_it++)
350 out << "<div class=\"description\">\n"
351 << escape_html(id2string(*s_it)) << '\n'
352 << "</div>\n";
353
354 out << '\n';
355
356 out << "<div class=\"code\">\n"
357 << code
358 << "</div> <!-- code -->\n";
359
360 out << "</div> <!-- claim -->\n";
361 out << '\n';
362 break;
363 }
364 }
365}
366
368 const goto_modelt &goto_model,
369 std::ostream &out)
370{
371 document_propertiest(goto_model.goto_functions, out).html();
372}
373
375 const goto_modelt &goto_model,
376 std::ostream &out)
377{
378 document_propertiest(goto_model.goto_functions, out).latex();
379}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:38
bool empty() const
Definition dstring.h:89
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
const irep_idt & get_file() const
const irep_idt & get_line() const
int isgraph(int c)
Definition ctype.c:29
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:44
int unsafe_string2int(const std::string &str, int base)