74 for(std::list<linet>::const_iterator it=
lines.begin();
75 it!=
lines.end(); it++)
77 for(std::size_t j=0; j<
strip && j<it->text.size(); j++)
87 for(std::list<linet>::iterator it=
lines.begin();
88 it!=
lines.end(); it++)
90 if(it->text.size()>=
strip)
91 it->text=std::string(it->text,
strip, std::string::npos);
94 it->text=std::string(it->text, 0,
MAXWIDTH);
103 for(std::size_t i=0; i<s.size(); i++)
105 if(s[i]==
'\\' || s[i]==
'{' || s[i]==
'}')
109 (s[i]==
'_' || s[i]==
'$' || s[i]==
'~' ||
110 s[i]==
'^' || s[i]==
'%' || s[i]==
'#' ||
124 for(std::size_t i=0; i<s.size(); i++)
128 case '&': dest+=
"&";
break;
129 case '<': dest+=
"<";
break;
130 case '>': dest+=
">";
break;
140 for(std::size_t i=0; i<s.size(); i++)
162 dest+=
"ERROR: unable to open ";
181 std::getline(in,
tmp);
186 std::list<linet>
lines;
192 std::string &line=
lines.back().text;
193 std::getline(in, line);
195 if(!line.empty() && line[line.size()-1]==
'\r')
196 line.resize(line.size()-1);
198 lines.back().line_number=l;
203 for(std::list<linet>::iterator it=
lines.begin();
212 for(std::list<linet>::iterator it=
lines.end();
233 for(std::list<linet>::iterator it=
lines.begin();
234 it!=
lines.end(); it++)
236 std::string line_no=std::to_string(it->line_number);
257 line_no=
" "+line_no;
259 line_no +=
" ";
269 dest += line_no +
tmp +
"\n";
277 typedef std::map<source_locationt, doc_claimt>
claim_sett;
284 for(
const auto &instruction : goto_program.
instructions)
286 if(instruction.is_assert())
288 const auto &source_location = instruction.source_location();
296 source_location.get_comment());
301 for(claim_sett::const_iterator it=
claim_set.begin();
306 std::string code =
get_code(source_location);
311 out <<
"\\claimlocation{File "
319 for(std::set<irep_idt>::const_iterator
320 s_it=it->second.comment_set.begin();
321 s_it!=it->second.comment_set.end();
328 out <<
"\\begin{alltt}\\claimcode\n"
337 out <<
"<div class=\"claim\">\n"
338 <<
"<div class=\"location\">File "
346 for(std::set<irep_idt>::const_iterator
347 s_it=it->second.comment_set.begin();
348 s_it!=it->second.comment_set.end();
350 out <<
"<div class=\"description\">\n"
356 out <<
"<div class=\"code\">\n"
358 <<
"</div> <!-- code -->\n";
360 out <<
"</div> <!-- claim -->\n";
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
A collection of goto functions.
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_idt &name) const
const irep_idt & get_file() const
const irep_idt & get_line() const
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::set< irep_idt > comment_set