cprover
document_properties.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Subgoal Documentation
4 
5 Author: 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 
18 #include <ansi-c/expr2c.h>
19 
20 #define MAXWIDTH 62
21 
23 {
24 public:
26  const goto_functionst &_goto_functions,
27  std::ostream &_out):
28  goto_functions(_goto_functions),
29  out(_out)
30  {
31  }
32 
33  void html()
34  {
35  format=HTML;
36  doit();
37  }
38 
39  void latex()
40  {
41  format=LATEX;
42  doit();
43  }
44 
45 private:
47  std::ostream &out;
48 
49  struct linet
50  {
51  std::string text;
53  };
54 
55  static void strip_space(std::list<linet> &lines);
56 
57  void get_code(
58  const source_locationt &source_location,
59  std::string &dest);
60 
61  struct doc_claimt
62  {
63  std::set<irep_idt> comment_set;
64  };
65 
66  enum { HTML, LATEX } format;
67 
68  void doit();
69 };
70 
71 void document_propertiest::strip_space(std::list<linet> &lines)
72 {
73  unsigned strip=50;
74 
75  for(std::list<linet>::const_iterator it=lines.begin();
76  it!=lines.end(); it++)
77  {
78  for(unsigned j=0; j<strip && j<it->text.size(); j++)
79  if(it->text[j]!=' ')
80  {
81  strip=j;
82  break;
83  }
84  }
85 
86  if(strip!=0)
87  {
88  for(std::list<linet>::iterator it=lines.begin();
89  it!=lines.end(); it++)
90  {
91  if(it->text.size()>=strip)
92  it->text=std::string(it->text, strip, std::string::npos);
93 
94  if(it->text.size()>=MAXWIDTH)
95  it->text=std::string(it->text, 0, MAXWIDTH);
96  }
97  }
98 }
99 
100 std::string escape_latex(const std::string &s, bool alltt)
101 {
102  std::string dest;
103 
104  for(unsigned i=0; i<s.size(); i++)
105  {
106  if(s[i]=='\\' || s[i]=='{' || s[i]=='}')
107  dest+="\\";
108 
109  if(!alltt &&
110  (s[i]=='_' || s[i]=='$' || s[i]=='~' ||
111  s[i]=='^' || s[i]=='%' || s[i]=='#' ||
112  s[i]=='&'))
113  dest+="\\";
114 
115  dest+=s[i];
116  }
117 
118  return dest;
119 }
120 
121 std::string escape_html(const std::string &s)
122 {
123  std::string dest;
124 
125  for(unsigned i=0; i<s.size(); i++)
126  {
127  switch(s[i])
128  {
129  case '&': dest+="&amp;"; break;
130  case '<': dest+="&lt;"; break;
131  case '>': dest+="&gt;"; break;
132  default: dest+=s[i];
133  }
134  }
135 
136  return dest;
137 }
138 
139 bool is_empty(const std::string &s)
140 {
141  for(unsigned i=0; i<s.size(); i++)
142  if(isgraph(s[i]))
143  return false;
144 
145  return true;
146 }
147 
149  const source_locationt &source_location,
150  std::string &dest)
151 {
152  dest="";
153 
154  const irep_idt &file=source_location.get_file();
155  const irep_idt &line=source_location.get_line();
156 
157  if(file=="" || line=="")
158  return;
159 
160  std::ifstream in(id2string(file));
161 
162  if(!in)
163  {
164  dest+="ERROR: unable to open ";
165  dest+=id2string(file);
166  dest+="\n";
167  return;
168  }
169 
170  int line_int=unsafe_string2int(id2string(line));
171 
172  int line_start=line_int-3,
173  line_end=line_int+3;
174 
175  if(line_start<=1)
176  line_start=1;
177 
178  // skip line_start-1 lines
179 
180  for(int l=0; l<line_start-1; l++)
181  {
182  std::string tmp;
183  std::getline(in, tmp);
184  }
185 
186  // read till line_end
187 
188  std::list<linet> lines;
189 
190  for(int l=line_start; l<=line_end && in; l++)
191  {
192  lines.push_back(linet());
193 
194  std::string &line=lines.back().text;
195  std::getline(in, line);
196 
197  if(!line.empty() && line[line.size()-1]=='\r')
198  line.resize(line.size()-1);
199 
200  lines.back().line_number=l;
201  }
202 
203  // remove empty lines at the end and at the beginning
204 
205  for(std::list<linet>::iterator it=lines.begin();
206  it!=lines.end();)
207  {
208  if(is_empty(it->text))
209  it=lines.erase(it);
210  else
211  break;
212  }
213 
214  for(std::list<linet>::iterator it=lines.end();
215  it!=lines.begin();)
216  {
217  it--;
218 
219  if(is_empty(it->text))
220  it=lines.erase(it);
221  else
222  break;
223  }
224 
225  // strip space
226  strip_space(lines);
227 
228  // build dest
229 
230  for(std::list<linet>::iterator it=lines.begin();
231  it!=lines.end(); it++)
232  {
233  std::string line_no=std::to_string(it->line_number);
234 
235  std::string tmp;
236 
237  switch(format)
238  {
239  case LATEX:
240  while(line_no.size()<4)
241  line_no=" "+line_no;
242 
243  line_no+" ";
244 
245  tmp+=escape_latex(it->text, true);
246 
247  if(it->line_number==line_int)
248  tmp="{\\ttb{}"+tmp+"}";
249 
250  break;
251 
252  case HTML:
253  while(line_no.size()<4)
254  line_no="&nbsp;"+line_no;
255 
256  line_no+"&nbsp;&nbsp;";
257 
258  tmp+=escape_html(it->text);
259 
260  if(it->line_number==line_int)
261  tmp="<em>"+tmp+"</em>";
262 
263  break;
264  }
265 
266  dest+=tmp+"\n";
267  }
268 }
269 
271 {
272  typedef std::map<source_locationt, doc_claimt> claim_sett;
273  claim_sett claim_set;
274 
276  {
277  const goto_programt &goto_program=f_it->second.body;
278 
279  forall_goto_program_instructions(i_it, goto_program)
280  {
281  if(i_it->is_assert())
282  {
283  source_locationt new_source_location;
284 
285  new_source_location.set_file(i_it->source_location.get_file());
286  new_source_location.set_line(i_it->source_location.get_line());
287  new_source_location.set_function(i_it->source_location.get_function());
288 
289  claim_set[new_source_location].comment_set.
290  insert(i_it->source_location.get_comment());
291  }
292  }
293  }
294 
295  for(claim_sett::const_iterator it=claim_set.begin();
296  it!=claim_set.end(); it++)
297  {
298  std::string code;
299  const source_locationt &source_location=it->first;
300 
301  get_code(source_location, code);
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 
364  std::ostream &out)
365 {
366  document_propertiest(goto_functions, out).html();
367 }
368 
371  std::ostream &out)
372 {
373  document_propertiest(goto_functions, out).latex();
374 }
std::string escape_latex(const std::string &s, bool alltt)
void set_function(const irep_idt &function)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
enum document_propertiest::@3 format
document_propertiest(const goto_functionst &_goto_functions, std::ostream &_out)
Documentation of Properties.
const irep_idt & get_line() const
void set_file(const irep_idt &file)
#define MAXWIDTH
void set_line(const irep_idt &line)
void get_code(const source_locationt &source_location, std::string &dest)
const goto_functionst & goto_functions
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void document_properties_latex(const goto_functionst &goto_functions, std::ostream &out)
std::string escape_html(const std::string &s)
const irep_idt & get_file() const
static void strip_space(std::list< linet > &lines)
bool is_empty(const std::string &s)
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
#define forall_goto_functions(it, functions)
void document_properties_html(const goto_functionst &goto_functions, std::ostream &out)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
Definition: kdev_t.h:19