76 for(std::list<linet>::const_iterator it=lines.begin();
77 it!=lines.end(); it++)
79 for(std::size_t j=0; j<strip && j<it->text.size(); j++)
89 for(std::list<linet>::iterator it=lines.begin();
90 it!=lines.end(); it++)
92 if(it->text.size()>=strip)
93 it->text=std::string(it->text, strip, std::string::npos);
96 it->text=std::string(it->text, 0,
MAXWIDTH);
105 for(std::size_t i=0; i<s.size(); i++)
107 if(s[i]==
'\\' || s[i]==
'{' || s[i]==
'}')
111 (s[i]==
'_' || s[i]==
'$' || s[i]==
'~' ||
112 s[i]==
'^' || s[i]==
'%' || s[i]==
'#' ||
126 for(std::size_t i=0; i<s.size(); i++)
130 case '&': dest+=
"&";
break;
131 case '<': dest+=
"<";
break;
132 case '>': dest+=
">";
break;
142 for(std::size_t i=0; i<s.size(); i++)
164 dest+=
"ERROR: unable to open ";
172 int line_start=line_int-3,
180 for(
int l=0; l<line_start-1; l++)
183 std::getline(in, tmp);
188 std::list<linet> lines;
190 for(
int l=line_start; l<=line_end && in; l++)
192 lines.push_back(
linet());
194 std::string &line=lines.back().text;
195 std::getline(in, line);
197 if(!line.empty() && line[line.size()-1]==
'\r')
198 line.resize(line.size()-1);
200 lines.back().line_number=l;
205 for(std::list<linet>::iterator it=lines.begin();
214 for(std::list<linet>::iterator it=lines.end();
230 for(std::list<linet>::iterator it=lines.begin();
231 it!=lines.end(); it++)
240 while(line_no.size()<4)
247 if(it->line_number==line_int)
248 tmp=
"{\\ttb{}"+tmp+
"}";
253 while(line_no.size()<4)
254 line_no=
" "+line_no;
256 line_no+
" ";
260 if(it->line_number==line_int)
261 tmp=
"<em>"+tmp+
"</em>";
274 typedef std::map<source_locationt, doc_claimt> claim_sett;
275 claim_sett claim_set;
281 for(
const auto &instruction : goto_program.
instructions)
283 if(instruction.is_assert())
285 const auto &source_location = instruction.source_location;
288 new_source_location.
set_file(source_location.get_file());
289 new_source_location.
set_line(source_location.get_line());
290 new_source_location.
set_function(source_location.get_function());
292 claim_set[new_source_location].comment_set.insert(
293 source_location.get_comment());
298 for(claim_sett::const_iterator it=claim_set.begin();
299 it!=claim_set.end(); it++)
303 std::string code =
get_code(source_location);
308 out <<
"\\claimlocation{File "
316 for(std::set<irep_idt>::const_iterator
317 s_it=it->second.comment_set.begin();
318 s_it!=it->second.comment_set.end();
325 out <<
"\\begin{alltt}\\claimcode\n"
334 out <<
"<div class=\"claim\">\n"
335 <<
"<div class=\"location\">File "
343 for(std::set<irep_idt>::const_iterator
344 s_it=it->second.comment_set.begin();
345 s_it!=it->second.comment_set.end();
347 out <<
"<div class=\"description\">\n"
353 out <<
"<div class=\"code\">\n"
355 <<
"</div> <!-- code -->\n";
357 out <<
"</div> <!-- claim -->\n";
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)
const goto_functionst & goto_functions
enum document_propertiest::@5 format
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
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_namet &name) const
const irep_idt & get_line() const
const irep_idt & get_file() 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)
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
Documentation of Properties.
const std::string & id2string(const irep_idt &d)
int unsafe_string2int(const std::string &str, int base)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::set< irep_idt > comment_set