CBMC
Public Member Functions | Public Attributes | Protected Member Functions | Protected Attributes | List of all members
ansi_c_convert_typet Class Reference

#include <ansi_c_convert_type.h>

+ Inheritance diagram for ansi_c_convert_typet:
+ Collaboration diagram for ansi_c_convert_typet:

Public Member Functions

virtual void write (typet &type)
 
 ansi_c_convert_typet (message_handlert &_message_handler, const typet &type)
 

Public Attributes

unsigned unsigned_cnt
 
unsigned signed_cnt
 
unsigned char_cnt
 
unsigned int_cnt
 
unsigned short_cnt
 
unsigned long_cnt
 
unsigned double_cnt
 
unsigned float_cnt
 
unsigned c_bool_cnt
 
unsigned proper_bool_cnt
 
unsigned complex_cnt
 
unsigned int8_cnt
 
unsigned int16_cnt
 
unsigned int32_cnt
 
unsigned int64_cnt
 
unsigned ptr32_cnt
 
unsigned ptr64_cnt
 
unsigned gcc_float16_cnt
 
unsigned gcc_float32_cnt
 
unsigned gcc_float32x_cnt
 
unsigned gcc_float64_cnt
 
unsigned gcc_float64x_cnt
 
unsigned gcc_float128_cnt
 
unsigned gcc_float128x_cnt
 
unsigned gcc_int128_cnt
 
unsigned bv_cnt
 
unsigned floatbv_cnt
 
unsigned fixedbv_cnt
 
typet gcc_attribute_mode
 
bool packed
 
bool aligned
 
exprt vector_size
 
exprt alignment
 
exprt bv_width
 
exprt fraction_width
 
exprt msc_based
 
bool constructor
 
bool destructor
 
exprt::operandst c_assigns
 
exprt::operandst c_frees
 
exprt::operandst c_ensures
 
exprt::operandst c_requires
 
c_storage_spect c_storage_spec
 
c_qualifierst c_qualifiers
 
source_locationt source_location
 
std::list< typet > other
 

Protected Member Functions

 ansi_c_convert_typet (message_handlert &_message_handler)
 
virtual void read_rec (const typet &type)
 
virtual void build_type_with_subtype (typet &type) const
 Build a vector or complex type with type as subtype. More...
 
virtual void set_attributes (typet &type) const
 Add qualifiers and GCC attributes onto type. More...
 

Protected Attributes

message_handlert & message_handler
 

Detailed Description

Definition at line 24 of file ansi_c_convert_type.h.

Constructor & Destructor Documentation

◆ ansi_c_convert_typet() [1/2]

ansi_c_convert_typet::ansi_c_convert_typet ( message_handlert &  _message_handler,
const typet &  type 
)
inline

Definition at line 65 of file ansi_c_convert_type.h.

◆ ansi_c_convert_typet() [2/2]

ansi_c_convert_typet::ansi_c_convert_typet ( message_handlert &  _message_handler)
inlineexplicitprotected

Definition at line 78 of file ansi_c_convert_type.h.

Member Function Documentation

◆ build_type_with_subtype()

void ansi_c_convert_typet::build_type_with_subtype ( typet &  type) const
protectedvirtual

Build a vector or complex type with type as subtype.

Definition at line 643 of file ansi_c_convert_type.cpp.

◆ read_rec()

void ansi_c_convert_typet::read_rec ( const typet &  type)
protectedvirtual

Reimplemented in cpp_convert_typet.

Definition at line 22 of file ansi_c_convert_type.cpp.

◆ set_attributes()

void ansi_c_convert_typet::set_attributes ( typet &  type) const
protectedvirtual

Add qualifiers and GCC attributes onto type.

Definition at line 663 of file ansi_c_convert_type.cpp.

◆ write()

void ansi_c_convert_typet::write ( typet &  type)
virtual

Reimplemented in cpp_convert_typet.

Definition at line 283 of file ansi_c_convert_type.cpp.

Member Data Documentation

◆ aligned

bool ansi_c_convert_typet::aligned

Definition at line 45 of file ansi_c_convert_type.h.

◆ alignment

exprt ansi_c_convert_typet::alignment

Definition at line 46 of file ansi_c_convert_type.h.

◆ bv_cnt

unsigned ansi_c_convert_typet::bv_cnt

Definition at line 40 of file ansi_c_convert_type.h.

◆ bv_width

exprt ansi_c_convert_typet::bv_width

Definition at line 46 of file ansi_c_convert_type.h.

◆ c_assigns

exprt::operandst ansi_c_convert_typet::c_assigns

Definition at line 51 of file ansi_c_convert_type.h.

◆ c_bool_cnt

unsigned ansi_c_convert_typet::c_bool_cnt

Definition at line 29 of file ansi_c_convert_type.h.

◆ c_ensures

exprt::operandst ansi_c_convert_typet::c_ensures

Definition at line 51 of file ansi_c_convert_type.h.

◆ c_frees

exprt::operandst ansi_c_convert_typet::c_frees

Definition at line 51 of file ansi_c_convert_type.h.

◆ c_qualifiers

c_qualifierst ansi_c_convert_typet::c_qualifiers

Definition at line 57 of file ansi_c_convert_type.h.

◆ c_requires

exprt::operandst ansi_c_convert_typet::c_requires

Definition at line 51 of file ansi_c_convert_type.h.

◆ c_storage_spec

c_storage_spect ansi_c_convert_typet::c_storage_spec

Definition at line 54 of file ansi_c_convert_type.h.

◆ char_cnt

unsigned ansi_c_convert_typet::char_cnt

Definition at line 27 of file ansi_c_convert_type.h.

◆ complex_cnt

unsigned ansi_c_convert_typet::complex_cnt

Definition at line 30 of file ansi_c_convert_type.h.

◆ constructor

bool ansi_c_convert_typet::constructor

Definition at line 48 of file ansi_c_convert_type.h.

◆ destructor

bool ansi_c_convert_typet::destructor

Definition at line 48 of file ansi_c_convert_type.h.

◆ double_cnt

unsigned ansi_c_convert_typet::double_cnt

Definition at line 29 of file ansi_c_convert_type.h.

◆ fixedbv_cnt

unsigned ansi_c_convert_typet::fixedbv_cnt

Definition at line 41 of file ansi_c_convert_type.h.

◆ float_cnt

unsigned ansi_c_convert_typet::float_cnt

Definition at line 29 of file ansi_c_convert_type.h.

◆ floatbv_cnt

unsigned ansi_c_convert_typet::floatbv_cnt

Definition at line 41 of file ansi_c_convert_type.h.

◆ fraction_width

exprt ansi_c_convert_typet::fraction_width

Definition at line 46 of file ansi_c_convert_type.h.

◆ gcc_attribute_mode

typet ansi_c_convert_typet::gcc_attribute_mode

Definition at line 43 of file ansi_c_convert_type.h.

◆ gcc_float128_cnt

unsigned ansi_c_convert_typet::gcc_float128_cnt

Definition at line 38 of file ansi_c_convert_type.h.

◆ gcc_float128x_cnt

unsigned ansi_c_convert_typet::gcc_float128x_cnt

Definition at line 38 of file ansi_c_convert_type.h.

◆ gcc_float16_cnt

unsigned ansi_c_convert_typet::gcc_float16_cnt

Definition at line 35 of file ansi_c_convert_type.h.

◆ gcc_float32_cnt

unsigned ansi_c_convert_typet::gcc_float32_cnt

Definition at line 36 of file ansi_c_convert_type.h.

◆ gcc_float32x_cnt

unsigned ansi_c_convert_typet::gcc_float32x_cnt

Definition at line 36 of file ansi_c_convert_type.h.

◆ gcc_float64_cnt

unsigned ansi_c_convert_typet::gcc_float64_cnt

Definition at line 37 of file ansi_c_convert_type.h.

◆ gcc_float64x_cnt

unsigned ansi_c_convert_typet::gcc_float64x_cnt

Definition at line 37 of file ansi_c_convert_type.h.

◆ gcc_int128_cnt

unsigned ansi_c_convert_typet::gcc_int128_cnt

Definition at line 39 of file ansi_c_convert_type.h.

◆ int16_cnt

unsigned ansi_c_convert_typet::int16_cnt

Definition at line 33 of file ansi_c_convert_type.h.

◆ int32_cnt

unsigned ansi_c_convert_typet::int32_cnt

Definition at line 33 of file ansi_c_convert_type.h.

◆ int64_cnt

unsigned ansi_c_convert_typet::int64_cnt

Definition at line 33 of file ansi_c_convert_type.h.

◆ int8_cnt

unsigned ansi_c_convert_typet::int8_cnt

Definition at line 33 of file ansi_c_convert_type.h.

◆ int_cnt

unsigned ansi_c_convert_typet::int_cnt

Definition at line 28 of file ansi_c_convert_type.h.

◆ long_cnt

unsigned ansi_c_convert_typet::long_cnt

Definition at line 28 of file ansi_c_convert_type.h.

◆ message_handler

message_handlert& ansi_c_convert_typet::message_handler
protected

Definition at line 73 of file ansi_c_convert_type.h.

◆ msc_based

exprt ansi_c_convert_typet::msc_based

Definition at line 47 of file ansi_c_convert_type.h.

◆ other

std::list<typet> ansi_c_convert_typet::other

Definition at line 63 of file ansi_c_convert_type.h.

◆ packed

bool ansi_c_convert_typet::packed

Definition at line 45 of file ansi_c_convert_type.h.

◆ proper_bool_cnt

unsigned ansi_c_convert_typet::proper_bool_cnt

Definition at line 30 of file ansi_c_convert_type.h.

◆ ptr32_cnt

unsigned ansi_c_convert_typet::ptr32_cnt

Definition at line 34 of file ansi_c_convert_type.h.

◆ ptr64_cnt

unsigned ansi_c_convert_typet::ptr64_cnt

Definition at line 34 of file ansi_c_convert_type.h.

◆ short_cnt

unsigned ansi_c_convert_typet::short_cnt

Definition at line 28 of file ansi_c_convert_type.h.

◆ signed_cnt

unsigned ansi_c_convert_typet::signed_cnt

Definition at line 27 of file ansi_c_convert_type.h.

◆ source_location

source_locationt ansi_c_convert_typet::source_location

Definition at line 61 of file ansi_c_convert_type.h.

◆ unsigned_cnt

unsigned ansi_c_convert_typet::unsigned_cnt

Definition at line 27 of file ansi_c_convert_type.h.

◆ vector_size

exprt ansi_c_convert_typet::vector_size

Definition at line 46 of file ansi_c_convert_type.h.

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