cprover
Loading...
Searching...
No Matches
ansi_c_parsert Class Reference

#include <ansi_c_parser.h>

+ Inheritance diagram for ansi_c_parsert:
+ Collaboration diagram for ansi_c_parsert:

Public Types

enum class  decl_typet { TAG , MEMBER , PARAMETER , OTHER }
 
typedef configt::ansi_ct::flavourt modet
 
typedef ansi_c_identifiert identifiert
 
typedef ansi_c_scopet scopet
 
typedef std::list< scopetscopest
 

Public Member Functions

 ansi_c_parsert ()
 
virtual bool parse () override
 
virtual void clear () override
 
scopetroot_scope ()
 
const scopetroot_scope () const
 
void pop_scope ()
 
scopetcurrent_scope ()
 
void add_declarator (exprt &declaration, irept &declarator)
 
void add_tag_with_body (irept &tag)
 
void copy_item (const ansi_c_declarationt &declaration)
 
void new_scope (const std::string &prefix)
 
ansi_c_id_classt lookup (const irep_idt &base_name, irep_idt &identifier, bool tag, bool label)
 
irep_idt lookup_label (const irep_idt base_name)
 
bool pragma_cprover_empty ()
 True iff the CPROVER pragma stack is empty.
 
void pragma_cprover_push ()
 Pushes an empty level in the CPROVER pragma stack.
 
void pragma_cprover_pop ()
 Pops a level in the CPROVER pragma stack.
 
void pragma_cprover_add_check (const irep_idt &name, bool enabled)
 Adds a check to the CPROVER pragma stack.
 
bool pragma_cprover_clash (const irep_idt &name, bool enabled)
 Returns true iff the same check with polarity is already present at top of the stack.
 
void set_pragma_cprover ()
 Tags source_location with the current CPROVER pragma stack.
 
- Public Member Functions inherited from parsert
 parsert ()
 
virtual ~parsert ()
 
bool read (char &ch)
 
bool eof ()
 
void parse_error (const std::string &message, const std::string &before)
 
void inc_line_no ()
 
void set_line_no (unsigned _line_no)
 
void set_file (const irep_idt &file)
 
irep_idt get_file () const
 
unsigned get_line_no () const
 
unsigned get_column () const
 
void set_column (unsigned _column)
 
void set_source_location (exprt &e)
 
void set_function (const irep_idt &function)
 
void advance_column (unsigned token_width)
 

Static Public Member Functions

static ansi_c_id_classt get_class (const typet &type)
 

Public Attributes

ansi_c_parse_treet parse_tree
 
bool tag_following
 
bool asm_block_following
 
unsigned parenthesis_counter
 
std::string string_literal
 
std::list< exprtpragma_pack
 
modet mode
 
bool cpp98
 
bool cpp11
 
bool for_has_scope
 
bool ts_18661_3_Floatn_types
 
bool float16_type
 
bool bf16_type
 
scopest scopes
 
- Public Attributes inherited from parsert
std::istream * in
 
std::string this_line
 
std::string last_line
 
std::vector< exprtstack
 
messaget log
 

Private Attributes

std::list< std::map< const irep_idt, bool > > pragma_cprover_stack
 

Additional Inherited Members

- Protected Attributes inherited from parsert
source_locationt source_location
 
unsigned line_no
 
unsigned previous_line_no
 
unsigned column
 

Detailed Description

Definition at line 23 of file ansi_c_parser.h.

Member Typedef Documentation

◆ identifiert

◆ modet

◆ scopest

Definition at line 89 of file ansi_c_parser.h.

◆ scopet

Member Enumeration Documentation

◆ decl_typet

Enumerator
TAG 
MEMBER 
PARAMETER 
OTHER 

Definition at line 113 of file ansi_c_parser.h.

Constructor & Destructor Documentation

◆ ansi_c_parsert()

ansi_c_parsert::ansi_c_parsert ( )
inline

Definition at line 28 of file ansi_c_parser.h.

Member Function Documentation

◆ add_declarator()

void ansi_c_parsert::add_declarator ( exprt & declaration,
irept & declarator )

Definition at line 84 of file ansi_c_parser.cpp.

◆ add_tag_with_body()

void ansi_c_parsert::add_tag_with_body ( irept & tag)

Definition at line 58 of file ansi_c_parser.cpp.

◆ clear()

virtual void ansi_c_parsert::clear ( )
inlineoverridevirtual

Reimplemented from parsert.

Definition at line 47 of file ansi_c_parser.h.

◆ copy_item()

void ansi_c_parsert::copy_item ( const ansi_c_declarationt & declaration)
inline

Definition at line 121 of file ansi_c_parser.h.

◆ current_scope()

scopet & ansi_c_parsert::current_scope ( )
inline

Definition at line 107 of file ansi_c_parser.h.

◆ get_class()

ansi_c_id_classt ansi_c_parsert::get_class ( const typet & type)
static

Definition at line 157 of file ansi_c_parser.cpp.

◆ lookup()

ansi_c_id_classt ansi_c_parsert::lookup ( const irep_idt & base_name,
irep_idt & identifier,
bool tag,
bool label )

Definition at line 15 of file ansi_c_parser.cpp.

◆ lookup_label()

irep_idt ansi_c_parsert::lookup_label ( const irep_idt base_name)
inline

Definition at line 142 of file ansi_c_parser.h.

◆ new_scope()

void ansi_c_parsert::new_scope ( const std::string & prefix)
inline

Definition at line 127 of file ansi_c_parser.h.

◆ parse()

virtual bool ansi_c_parsert::parse ( )
inlineoverridevirtual

Implements parsert.

Definition at line 42 of file ansi_c_parser.h.

◆ pop_scope()

void ansi_c_parsert::pop_scope ( )
inline

Definition at line 102 of file ansi_c_parser.h.

◆ pragma_cprover_add_check()

void ansi_c_parsert::pragma_cprover_add_check ( const irep_idt & name,
bool enabled )

Adds a check to the CPROVER pragma stack.

Definition at line 194 of file ansi_c_parser.cpp.

◆ pragma_cprover_clash()

bool ansi_c_parsert::pragma_cprover_clash ( const irep_idt & name,
bool enabled )

Returns true iff the same check with polarity is already present at top of the stack.

Definition at line 204 of file ansi_c_parser.cpp.

◆ pragma_cprover_empty()

bool ansi_c_parsert::pragma_cprover_empty ( )

True iff the CPROVER pragma stack is empty.

Definition at line 179 of file ansi_c_parser.cpp.

◆ pragma_cprover_pop()

void ansi_c_parsert::pragma_cprover_pop ( )

Pops a level in the CPROVER pragma stack.

Definition at line 189 of file ansi_c_parser.cpp.

◆ pragma_cprover_push()

void ansi_c_parsert::pragma_cprover_push ( )

Pushes an empty level in the CPROVER pragma stack.

Definition at line 184 of file ansi_c_parser.cpp.

◆ root_scope() [1/2]

scopet & ansi_c_parsert::root_scope ( )
inline

Definition at line 92 of file ansi_c_parser.h.

◆ root_scope() [2/2]

const scopet & ansi_c_parsert::root_scope ( ) const
inline

Definition at line 97 of file ansi_c_parser.h.

◆ set_pragma_cprover()

void ansi_c_parsert::set_pragma_cprover ( )

Tags source_location with the current CPROVER pragma stack.

Definition at line 211 of file ansi_c_parser.cpp.

Member Data Documentation

◆ asm_block_following

bool ansi_c_parsert::asm_block_following

Definition at line 67 of file ansi_c_parser.h.

◆ bf16_type

bool ansi_c_parsert::bf16_type

Definition at line 84 of file ansi_c_parser.h.

◆ cpp11

bool ansi_c_parsert::cpp11

Definition at line 76 of file ansi_c_parser.h.

◆ cpp98

bool ansi_c_parsert::cpp98

Definition at line 76 of file ansi_c_parser.h.

◆ float16_type

bool ansi_c_parsert::float16_type

Definition at line 83 of file ansi_c_parser.h.

◆ for_has_scope

bool ansi_c_parsert::for_has_scope

Definition at line 79 of file ansi_c_parser.h.

◆ mode

modet ansi_c_parsert::mode

Definition at line 73 of file ansi_c_parser.h.

◆ parenthesis_counter

unsigned ansi_c_parsert::parenthesis_counter

Definition at line 68 of file ansi_c_parser.h.

◆ parse_tree

ansi_c_parse_treet ansi_c_parsert::parse_tree

Definition at line 26 of file ansi_c_parser.h.

◆ pragma_cprover_stack

std::list<std::map<const irep_idt, bool> > ansi_c_parsert::pragma_cprover_stack
private

Definition at line 170 of file ansi_c_parser.h.

◆ pragma_pack

std::list<exprt> ansi_c_parsert::pragma_pack

Definition at line 70 of file ansi_c_parser.h.

◆ scopes

scopest ansi_c_parsert::scopes

Definition at line 90 of file ansi_c_parser.h.

◆ string_literal

std::string ansi_c_parsert::string_literal

Definition at line 69 of file ansi_c_parser.h.

◆ tag_following

bool ansi_c_parsert::tag_following

Definition at line 66 of file ansi_c_parser.h.

◆ ts_18661_3_Floatn_types

bool ansi_c_parsert::ts_18661_3_Floatn_types

Definition at line 82 of file ansi_c_parser.h.


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