CBMC
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 (message_handlert &message_handler)
 
bool parse () 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. More...
 
void pragma_cprover_push ()
 Pushes an empty level in the CPROVER pragma stack. More...
 
void pragma_cprover_pop ()
 Pops a level in the CPROVER pragma stack. More...
 
void pragma_cprover_add_check (const irep_idt &name, bool enabled)
 Adds a check to the CPROVER pragma stack. More...
 
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. More...
 
void set_pragma_cprover ()
 Tags source_location with the current CPROVER pragma stack. More...
 
- Public Member Functions inherited from parsert
 parsert (message_handlert &message_handler)
 
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 __float128_is_keyword
 
bool float16_type
 
bool bf16_type
 
bool fp16_type
 
scopest scopes
 
- Public Attributes inherited from parsert
std::istream * in
 
std::string this_line
 
std::string last_line
 
std::vector< exprtstack
 

Private Attributes

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

Additional Inherited Members

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

Detailed Description

Definition at line 24 of file ansi_c_parser.h.

Member Typedef Documentation

◆ identifiert

◆ modet

◆ scopest

typedef std::list<scopet> ansi_c_parsert::scopest

Definition at line 80 of file ansi_c_parser.h.

◆ scopet

Definition at line 78 of file ansi_c_parser.h.

Member Enumeration Documentation

◆ decl_typet

Enumerator
TAG 
MEMBER 
PARAMETER 
OTHER 

Definition at line 104 of file ansi_c_parser.h.

Constructor & Destructor Documentation

◆ ansi_c_parsert()

ansi_c_parsert::ansi_c_parsert ( message_handlert message_handler)
inlineexplicit

Definition at line 29 of file ansi_c_parser.h.

Member Function Documentation

◆ add_declarator()

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

Definition at line 74 of file ansi_c_parser.cpp.

◆ add_tag_with_body()

void ansi_c_parsert::add_tag_with_body ( irept tag)

Definition at line 56 of file ansi_c_parser.cpp.

◆ copy_item()

void ansi_c_parsert::copy_item ( const ansi_c_declarationt declaration)
inline

Definition at line 112 of file ansi_c_parser.h.

◆ current_scope()

scopet& ansi_c_parsert::current_scope ( )
inline

Definition at line 98 of file ansi_c_parser.h.

◆ get_class()

ansi_c_id_classt ansi_c_parsert::get_class ( const typet type)
static

Definition at line 147 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 13 of file ansi_c_parser.cpp.

◆ lookup_label()

irep_idt ansi_c_parsert::lookup_label ( const irep_idt  base_name)
inline

Definition at line 133 of file ansi_c_parser.h.

◆ new_scope()

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

Definition at line 118 of file ansi_c_parser.h.

◆ parse()

bool ansi_c_parsert::parse ( )
inlineoverridevirtual

Implements parsert.

Definition at line 49 of file ansi_c_parser.h.

◆ pop_scope()

void ansi_c_parsert::pop_scope ( )
inline

Definition at line 93 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 184 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 194 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 169 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 179 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 174 of file ansi_c_parser.cpp.

◆ root_scope() [1/2]

scopet& ansi_c_parsert::root_scope ( )
inline

Definition at line 83 of file ansi_c_parser.h.

◆ root_scope() [2/2]

const scopet& ansi_c_parsert::root_scope ( ) const
inline

Definition at line 88 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 201 of file ansi_c_parser.cpp.

Member Data Documentation

◆ __float128_is_keyword

bool ansi_c_parsert::__float128_is_keyword

Definition at line 72 of file ansi_c_parser.h.

◆ asm_block_following

bool ansi_c_parsert::asm_block_following

Definition at line 56 of file ansi_c_parser.h.

◆ bf16_type

bool ansi_c_parsert::bf16_type

Definition at line 74 of file ansi_c_parser.h.

◆ cpp11

bool ansi_c_parsert::cpp11

Definition at line 65 of file ansi_c_parser.h.

◆ cpp98

bool ansi_c_parsert::cpp98

Definition at line 65 of file ansi_c_parser.h.

◆ float16_type

bool ansi_c_parsert::float16_type

Definition at line 73 of file ansi_c_parser.h.

◆ for_has_scope

bool ansi_c_parsert::for_has_scope

Definition at line 68 of file ansi_c_parser.h.

◆ fp16_type

bool ansi_c_parsert::fp16_type

Definition at line 75 of file ansi_c_parser.h.

◆ mode

modet ansi_c_parsert::mode

Definition at line 62 of file ansi_c_parser.h.

◆ parenthesis_counter

unsigned ansi_c_parsert::parenthesis_counter

Definition at line 57 of file ansi_c_parser.h.

◆ parse_tree

ansi_c_parse_treet ansi_c_parsert::parse_tree

Definition at line 27 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 161 of file ansi_c_parser.h.

◆ pragma_pack

std::list<exprt> ansi_c_parsert::pragma_pack

Definition at line 59 of file ansi_c_parser.h.

◆ scopes

scopest ansi_c_parsert::scopes

Definition at line 81 of file ansi_c_parser.h.

◆ string_literal

std::string ansi_c_parsert::string_literal

Definition at line 58 of file ansi_c_parser.h.

◆ tag_following

bool ansi_c_parsert::tag_following

Definition at line 55 of file ansi_c_parser.h.

◆ ts_18661_3_Floatn_types

bool ansi_c_parsert::ts_18661_3_Floatn_types

Definition at line 71 of file ansi_c_parser.h.


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