CBMC
document_propertiest Class Reference
+ Collaboration diagram for document_propertiest:

Classes

struct  doc_claimt
 
struct  linet
 

Public Member Functions

 document_propertiest (const goto_functionst &_goto_functions, std::ostream &_out)
 
void html ()
 
void latex ()
 

Private Types

enum  { HTML , LATEX }
 

Private Member Functions

std::string get_code (const source_locationt &source_location)
 
void doit ()
 

Static Private Member Functions

static void strip_space (std::list< linet > &lines)
 

Private Attributes

const goto_functionstgoto_functions
 
std::ostream & out
 
enum document_propertiest:: { ... }  format
 

Detailed Description

Definition at line 22 of file document_properties.cpp.

Member Enumeration Documentation

◆ anonymous enum

anonymous enum
private
Enumerator
HTML 
LATEX 

Definition at line 65 of file document_properties.cpp.

Constructor & Destructor Documentation

◆ document_propertiest()

document_propertiest::document_propertiest ( const goto_functionst _goto_functions,
std::ostream &  _out 
)
inline

Definition at line 25 of file document_properties.cpp.

Member Function Documentation

◆ doit()

void document_propertiest::doit ( )
private

Definition at line 275 of file document_properties.cpp.

◆ get_code()

std::string document_propertiest::get_code ( const source_locationt source_location)
private

Definition at line 148 of file document_properties.cpp.

◆ html()

void document_propertiest::html ( )
inline

Definition at line 34 of file document_properties.cpp.

◆ latex()

void document_propertiest::latex ( )
inline

Definition at line 40 of file document_properties.cpp.

◆ strip_space()

void document_propertiest::strip_space ( std::list< linet > &  lines)
staticprivate

Definition at line 70 of file document_properties.cpp.

Member Data Documentation

◆ 

enum { ... } document_propertiest::format

◆ goto_functions

const goto_functionst& document_propertiest::goto_functions
private

Definition at line 47 of file document_properties.cpp.

◆ out

std::ostream& document_propertiest::out
private

Definition at line 48 of file document_properties.cpp.


The documentation for this class was generated from the following file: