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;
190 lines.push_back(
linet());
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();
228 for(std::list<linet>::iterator it=lines.begin();
229 it!=lines.end(); it++)
231 std::string line_no=std::to_string(it->line_number);
238 while(line_no.size()<4)
251 while(line_no.size()<4)
252 line_no=
" "+line_no;
254 line_no+
" ";
272 typedef std::map<source_locationt, doc_claimt>
claim_sett;
279 for(
const auto &instruction : goto_program.
instructions)
281 if(instruction.is_assert())
283 const auto &source_location = instruction.source_location();
291 source_location.get_comment());
296 for(claim_sett::const_iterator it=
claim_set.begin();
301 std::string code =
get_code(source_location);
306 out <<
"\\claimlocation{File "
314 for(std::set<irep_idt>::const_iterator
315 s_it=it->second.comment_set.begin();
316 s_it!=it->second.comment_set.end();
323 out <<
"\\begin{alltt}\\claimcode\n"
332 out <<
"<div class=\"claim\">\n"
333 <<
"<div class=\"location\">File "
341 for(std::set<irep_idt>::const_iterator
342 s_it=it->second.comment_set.begin();
343 s_it!=it->second.comment_set.end();
345 out <<
"<div class=\"description\">\n"
351 out <<
"<div class=\"code\">\n"
353 <<
"</div> <!-- code -->\n";
355 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.
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_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