An interface to deal with the types of variables (during compilation and type checking. More...
#include <SymbType.h>
Related Functions | |
(Note that these are not member functions.) | |
| int | SymbType_calculate_type_size (const SymbType_ptr self) |
| The function calculate how many bits is required to store a value of a given type. | |
| SymbType_ptr | SymbType_copy (const SymbType_ptr self) |
| Class SymbType copy-constructor. | |
| SymbType_ptr | SymbType_create (const NuSMVEnv_ptr env, SymbTypeTag tag, node_ptr body) |
| Class SymbType constructor. | |
| SymbType_ptr | SymbType_create_array (SymbType_ptr subtype, int lower_bound, int upper_bound) |
| Class SymbType constructor for array types only. | |
| SymbType_ptr | SymbType_create_memory_sharing_array_type (SymbType_ptr subtype, int lower_bound, int higher_bound) |
| Private class SymbType constructor for memory sharing array type instances. | |
| SymbType_ptr | SymbType_create_memory_sharing_type (const NuSMVEnv_ptr env, SymbTypeTag tag, node_ptr body) |
| Private interface accessed by class SymbTable. | |
| SymbType_ptr | SymbType_create_nfunction (const NuSMVEnv_ptr env, NFunction_ptr nfunction) |
| Class SymbType constructor for uninterpreted functions only. | |
| void | SymbType_destroy (SymbType_ptr self) |
| Class SymbType destructor. | |
| void | SymbType_destroy_memory_sharing_type (SymbType_ptr self) |
| Private Class SymbType destructor for memory sharing instances of types. | |
| boolean | SymbType_equals (SymbType_ptr self, SymbType_ptr oth) |
| True if and only if the given types are equal, the given types can be memory-sharing or not. | |
| node_ptr | SymbType_generate_all_word_values (const SymbType_ptr self) |
| Generates and returns a list of all possible values of a particular Unsigned Word type. | |
| int | SymbType_get_array_lower_bound (const SymbType_ptr self) |
| Get array lower bound. | |
| SymbType_ptr | SymbType_get_array_subtype (const SymbType_ptr self) |
| Get inner type of an array. | |
| int | SymbType_get_array_upper_bound (const SymbType_ptr self) |
| Get array upper bound. | |
| node_ptr | SymbType_get_enum_type_values (const SymbType_ptr self) |
| Returns the list of values of an enum type. | |
| SymbType_ptr | SymbType_get_intarray_subtype (const SymbType_ptr self) |
| Get inner type of an array. | |
| NFunction_ptr | SymbType_get_nfunction_type (const SymbType_ptr self) |
| Returns the type of an NFunction. | |
| SymbTypeTag | SymbType_get_tag (const SymbType_ptr self) |
| Returns the tag (the kind) of the type. | |
| int | SymbType_get_word_line_number (const SymbType_ptr self) |
| Returns the line number where the type was declared. | |
| int | SymbType_get_word_width (const SymbType_ptr self) |
| Returns the width of a Word type. | |
| int | SymbType_get_wordarray_awidth (const SymbType_ptr self) |
| Returns the width of the address in a WordArray type. | |
| SymbType_ptr | SymbType_get_wordarray_subtype (const SymbType_ptr self) |
| Returns the subtype of wordarray. | |
| boolean | SymbType_is_array (const SymbType_ptr self) |
| Returns true if the type is an array-type, or else returns false. | |
| boolean | SymbType_is_boolean (const SymbType_ptr self) |
| Returns true, if the type is boolean. Otherwise - returns false. | |
| boolean | SymbType_is_continuous (const SymbType_ptr self) |
| Returns true if the type is a continuous type, or else returns false. | |
| boolean | SymbType_is_enum (const SymbType_ptr self) |
| Returns true if the type is a enum-type, or else returns false. | |
| boolean | SymbType_is_error (const SymbType_ptr self) |
| Returns true, if the type is a error-type, and false otherwise. | |
| boolean | SymbType_is_function (const SymbType_ptr self) |
| Returns true, if the type is an uninterpreted function type. | |
| boolean | SymbType_is_infinite_precision (const SymbType_ptr self) |
| Returns true, if the type is one of infinite-precision types. | |
| boolean | SymbType_is_int_symbolic_enum (const SymbType_ptr self) |
| Returns true, if the type is a enum-type and its value are symbolic AND integer constants. Otherwise - returns false. | |
| boolean | SymbType_is_intarray (const SymbType_ptr self) |
| Returns true if the type is intarray, or else returns false. | |
| boolean | SymbType_is_integer (const SymbType_ptr self) |
| Returns true if the type is a integer-type, or else returns false. | |
| boolean | SymbType_is_memory_shared (SymbType_ptr self) |
| True if and only if the given type is memory shared. | |
| boolean | SymbType_is_pure_int_enum (const SymbType_ptr self) |
| Returns true, if the type is a enum-type and its value are integers only. Otherwise - returns false. | |
| boolean | SymbType_is_pure_symbolic_enum (const SymbType_ptr self) |
| Returns true, if the type is a enum-type and its value are symbolic constants only. Otherwise - returns false. | |
| boolean | SymbType_is_real (const SymbType_ptr self) |
| Returns true if the type is a real-type, or else returns false. | |
| boolean | SymbType_is_set (const SymbType_ptr self) |
| Returns true, if the type is one of the set-types, i.e. boolean-set, integer-set, symbolic-set, integer-symbolic-set, and false otherwise. | |
| boolean | SymbType_is_signed_word (const SymbType_ptr self) |
| Returns true, if the type is a signed Word type. | |
| boolean | SymbType_is_single_value_enum (const SymbType_ptr self) |
| True if it is enum and with just one value. | |
| boolean | SymbType_is_statement (const SymbType_ptr self) |
| Returns true, if the type is a statement-type, and false otherwise. | |
| boolean | SymbType_is_unsigned_word (const SymbType_ptr self) |
| Returns true, if the type is an unsigned Word type. | |
| boolean | SymbType_is_word (const SymbType_ptr self) |
| Returns true, if the type is a Word type (signed or unsigned). | |
| boolean | SymbType_is_word_1 (const SymbType_ptr self) |
| Returns true, if the type is a Unsigned Word type and the width of the word is 1. Otherwise - returns false. | |
| boolean | SymbType_is_wordarray (const SymbType_ptr self) |
| Returns true if the given type is a wordarray. | |
| SymbType_ptr | SymbType_make_from_set_type (const SymbType_ptr self) |
| This function is opposite to SymbType_make_set_type, i.e. if the given type is one of the set-types, then the type without "set" suffix is returned. Otherwise the type is returned without change. | |
| SymbType_ptr | SymbType_make_memory_shared (const SymbType_ptr self) |
| This function takes a NOT memory shared type and returns a memory shared one. | |
| SymbType_ptr | SymbType_make_set_type (const SymbType_ptr self) |
| Returns a minimal set-type which the given type can be implicitly converted to, or NULL if this is impossible. | |
| void | SymbType_print (const SymbType_ptr self, MasterPrinter_ptr printer, FILE *output_stream) |
| Prints the type structure to the output stream. | |
| char * | SymbType_sprint (const SymbType_ptr self, MasterPrinter_ptr printer) |
| Return a string representation of the given type. | |
| node_ptr | SymbType_to_node (const SymbType_ptr self, NodeMgr_ptr nodemgr) |
| Returns a node representing a type. | |
An interface to deal with the types of variables (during compilation and type checking.
NOTE: In the following description "integer" is used everywhere to refer to the set of natural numbers, EXCEPT for the type specified in c), that has a special meaning.
The types can be: a) boolean (TRUE, FALSE) b) enum (enumeration), that represents a set of particular values, e.g. . a pure symbolic enumeration type: {A, OK, CORRECT, FAIL} . a pure integer enumeration type: {1,2,3,4,5, 10, -1, 0} . an integer and symbolic enumeration type: {0, 2, 4, OK, FAIL} . a range of integer values: 1 .. 10; c) integer, that represents the infinite-precision integer arithmetic. d) real, that represents the infinite-precision rational arithmetic. e) continuous, that represents infinite-precision real variables with continuous behavior (they can be derivated); f) word of width N (N is an integer positive number), that represents bit vectors of N bits. g) WordArray of address word of width M and value word of width N (with M and N integer positive numbers), that represents a memory array of 2^M locations, each of which contains a word of M bits. WARNING: Traces assumes only array defines to have type array h) Array represents array of fixed lower and upper bounds and elements of a particular type. i) Set types created by "union" expressions and used in "in", "case" and ":=" expressions: . a set of boolean values : 0 union 1 . a set of integer values : 0 union -1 union 10 . a set of symbolic values : OK union FAIL . a set of integer and symbolic values: OK union 1 Note that only expressions (not declared variables) can have these types. j) No-type is an artificial type to represent expressions which usually do not have any type (for example, assignments). k) Error type is an artificial type to represent erroneous situations.
A type can be created with the class' constructor. In the case of a enum type, during construction it is necessary to specify explicitly the list of values this type consists of.
The constructor is typically used in a symbol table.
Another possibility is to obtain the types with SymbTablePkg_..._type functions. In this case, the enum types will be "abstract", i.e. they will consist of some artificial (not existing) values. The important feature is that the memory is shared by these functions, i.e. you can compare pointers to types, instead of the types' contents. These functions are mostly used in type checking (since the particular values of enum types are of no importance).
Generic and symbolic encoding
| int SymbType_calculate_type_size | ( | const SymbType_ptr | self | ) | [related] |
The function calculate how many bits is required to store a value of a given type.
This function can be invoked only on finite-precision valid type of variables. This means that such types as no-type or error-type or real or any memory-shared ones should not be given to this function.
| SymbType_ptr SymbType_copy | ( | const SymbType_ptr | self | ) | [related] |
Class SymbType copy-constructor.
This function takes one type and returns its copy.
Note: the body of the type is not copied, i.e. just pointer is remembered. See SymbType_create for more info about body.
Note: the input type should not be a memory-shared type (since there is no meaning in coping a memory sharing type).
allocate memory
| SymbType_ptr SymbType_create | ( | const NuSMVEnv_ptr | env, | |
| SymbTypeTag | tag, | |||
| node_ptr | body | |||
| ) | [related] |
Class SymbType constructor.
The tag must be a correct tag. The 'body' is the additional info corresponding to a particular kind of the type: for a enum type the body is the list of values; for "BOOL", "INT" or "REAL" the body is unused, and set to Nil; for signed and unsigned "WORD" it is the NUMBER node defining the width of the type; for "WORDARRAY", the body is a pair of NUMBER nodes, defining the width of the address, and the width of the value. for everything else body is Nil;
Note that array types have to be created with SymbType_create_array, not with this constructor.
Set-types are used with expressions which represent a set values. "NO-TYPE" is used with expressions which normally do not have any type such as assignments. "ERROR" type indicates an error (not an actual type).
No-type, error-type and all set-types (boolean-set, integer-set, symbolic-set, symbolic-integer-set) should not be created with this constructor, but only with memory-shared function SymbTablePkg_..._type. The reason behind this constrain is that only expressions (not variables) can have these types, therefore only memory-shared versions of these types are required.
The constructor does not create a copy of the body, but just remember the pointer.
NB: system "reset" command destroys all node_ptr objects, including those used in SymbType_ptr. So destroy all symbolic types before the destruction of node_ptr objects, i.e. before or during "reset"
allocate memory
| SymbType_ptr SymbType_create_array | ( | SymbType_ptr | subtype, | |
| int | lower_bound, | |||
| int | upper_bound | |||
| ) | [related] |
Class SymbType constructor for array types only.
WARNING: Traces assumes only array defines to have type ARRAY This is specialized version of SymbType_create which is designed for array types only. It is implemented as a special construtor because array types are quite different from all the others.
Parameter subtype is the subtype of the array type. This type has to be not-memory-shared and its ownership is passed to created type. I.e. subtype will be destroyed when returned type is destroyed.
lower_bound, upper-bound are the lower and upper bounds,resp, of the array.
All the constrains about memory, lifetype, etc are the same as for SymbType_create.
allocate memory
| SymbType_ptr SymbType_create_memory_sharing_array_type | ( | SymbType_ptr | subtype, | |
| int | lower_bound, | |||
| int | higher_bound | |||
| ) | [related] |
Private class SymbType constructor for memory sharing array type instances.
The same as SymbType_create_memory_sharing_type but can be used to create array types. subtype has to be memory shared.
allocate memory
| SymbType_ptr SymbType_create_memory_sharing_type | ( | const NuSMVEnv_ptr | env, | |
| SymbTypeTag | tag, | |||
| node_ptr | body | |||
| ) | [related] |
Private interface accessed by class SymbTable.
Private class SymbType constructor for memory sharing type instances The difference from the public constructor is that this constructor marks the created type as a memory sharing type. As result the public constructor will not be able to destroy memory sharing instance of a type. Use the private constructor SymbType_destroy_memory_sharing_type to destroy such instances.
allocate memory
| SymbType_ptr SymbType_create_nfunction | ( | const NuSMVEnv_ptr | env, | |
| NFunction_ptr | nfunction | |||
| ) | [related] |
Class SymbType constructor for uninterpreted functions only.
This is specialized version of SymbType_create which is designed for uninterpreted functions only. It is implemented as a special construtor because functions types are quite different from all the others.
allocate memory
| void SymbType_destroy | ( | SymbType_ptr | self | ) | [related] |
Class SymbType destructor.
Deallocate the memory. The destructor does not deallocate memory from the type's body (since the constructor did not created the body).
NOTE: If self is a memory sharing type instance, i.e. a type returned by SymbTablePkg_..._type functions then the destructor will not delete the type.
| void SymbType_destroy_memory_sharing_type | ( | SymbType_ptr | self | ) | [related] |
Private Class SymbType destructor for memory sharing instances of types.
The same as the public destructor SymbType_destroy but 'self' has to be created by private constructor SymbType_create_memory_sharing_type only.
| boolean SymbType_equals | ( | SymbType_ptr | self, | |
| SymbType_ptr | oth | |||
| ) | [related] |
True if and only if the given types are equal, the given types can be memory-sharing or not.
| node_ptr SymbType_generate_all_word_values | ( | const SymbType_ptr | self | ) | [related] |
Generates and returns a list of all possible values of a particular Unsigned Word type.
| int SymbType_get_array_lower_bound | ( | const SymbType_ptr | self | ) | [related] |
Get array lower bound.
| SymbType_ptr SymbType_get_array_subtype | ( | const SymbType_ptr | self | ) | [related] |
Get inner type of an array.
The returned pointer belongs to the ginven SymbType_ptr and must not be freed
| int SymbType_get_array_upper_bound | ( | const SymbType_ptr | self | ) | [related] |
Get array upper bound.
| node_ptr SymbType_get_enum_type_values | ( | const SymbType_ptr | self | ) | [related] |
Returns the list of values of an enum type.
The given type has to be a ENUM type. The return list is a list of all possible values of a enum type. This list was provided during construction.
NB: Memory sharing types do not have particular values, since they are "simplified".
| SymbType_ptr SymbType_get_intarray_subtype | ( | const SymbType_ptr | self | ) | [related] |
Get inner type of an array.
The returned pointer belongs to the ginven SymbType_ptr and must not be freed
| NFunction_ptr SymbType_get_nfunction_type | ( | const SymbType_ptr | self | ) | [related] |
| SymbTypeTag SymbType_get_tag | ( | const SymbType_ptr | self | ) | [related] |
Returns the tag (the kind) of the type.
| int SymbType_get_word_line_number | ( | const SymbType_ptr | self | ) | [related] |
Returns the line number where the type was declared.
The body of the type, provided during construction, is a node NUMBER specifying the width of the Word or a node CONS specifying the address-value widths or WordArray. This node was create during parsing and contains the line number of the type declaration. NB: The type should not be memory-sharing. NB: Virtually this function is used only in TypeChecker_is_type_wellformed
| int SymbType_get_word_width | ( | const SymbType_ptr | self | ) | [related] |
Returns the width of a Word type.
The given type should be Word and the body of the type (given to the constructor) should be NUMBER node.
| int SymbType_get_wordarray_awidth | ( | const SymbType_ptr | self | ) | [related] |
Returns the width of the address in a WordArray type.
| SymbType_ptr SymbType_get_wordarray_subtype | ( | const SymbType_ptr | self | ) | [related] |
Returns the subtype of wordarray.
| boolean SymbType_is_array | ( | const SymbType_ptr | self | ) | [related] |
Returns true if the type is an array-type, or else returns false.
WARNING: Traces assumes this function returns true only for array defines
| boolean SymbType_is_boolean | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is boolean. Otherwise - returns false.
The kind of enum-type is analysed in the constructor.
| boolean SymbType_is_continuous | ( | const SymbType_ptr | self | ) | [related] |
Returns true if the type is a continuous type, or else returns false.
| boolean SymbType_is_enum | ( | const SymbType_ptr | self | ) | [related] |
Returns true if the type is a enum-type, or else returns false.
| boolean SymbType_is_error | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is a error-type, and false otherwise.
Error type is used to indicate an error
| boolean SymbType_is_function | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is an uninterpreted function type.
| boolean SymbType_is_infinite_precision | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is one of infinite-precision types.
Infinite-precision types are such as integer and real.
| boolean SymbType_is_int_symbolic_enum | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is a enum-type and its value are symbolic AND integer constants. Otherwise - returns false.
The kind of enum-type is analysed in the constructor.
| boolean SymbType_is_intarray | ( | const SymbType_ptr | self | ) | [related] |
Returns true if the type is intarray, or else returns false.
| boolean SymbType_is_integer | ( | const SymbType_ptr | self | ) | [related] |
Returns true if the type is a integer-type, or else returns false.
| boolean SymbType_is_memory_shared | ( | SymbType_ptr | self | ) | [related] |
True if and only if the given type is memory shared.
| boolean SymbType_is_pure_int_enum | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is a enum-type and its value are integers only. Otherwise - returns false.
The kind of enum-type is analysed in the constructor.
| boolean SymbType_is_pure_symbolic_enum | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is a enum-type and its value are symbolic constants only. Otherwise - returns false.
The kind of enum-type is analysed in the constructor.
| boolean SymbType_is_real | ( | const SymbType_ptr | self | ) | [related] |
Returns true if the type is a real-type, or else returns false.
| boolean SymbType_is_set | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is one of the set-types, i.e. boolean-set, integer-set, symbolic-set, integer-symbolic-set, and false otherwise.
| boolean SymbType_is_signed_word | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is a signed Word type.
| boolean SymbType_is_single_value_enum | ( | const SymbType_ptr | self | ) | [related] |
True if it is enum and with just one value.
| boolean SymbType_is_statement | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is a statement-type, and false otherwise.
| boolean SymbType_is_unsigned_word | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is an unsigned Word type.
| boolean SymbType_is_word | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is a Word type (signed or unsigned).
| boolean SymbType_is_word_1 | ( | const SymbType_ptr | self | ) | [related] |
Returns true, if the type is a Unsigned Word type and the width of the word is 1. Otherwise - returns false.
| boolean SymbType_is_wordarray | ( | const SymbType_ptr | self | ) | [related] |
Returns true if the given type is a wordarray.
| SymbType_ptr SymbType_make_from_set_type | ( | const SymbType_ptr | self | ) | [related] |
This function is opposite to SymbType_make_set_type, i.e. if the given type is one of the set-types, then the type without "set" suffix is returned. Otherwise the type is returned without change.
More precisely the following conversion takes place: boolean-set -> boolean integer-set ->integer symbolic-set -> symbolic-enum integer-symbolic-set -> integer-symbolic-set another type -> the same type
The implicit conversion is performed in accordance to the type order. NOTE: only memory-shared types can be given to this function.
| SymbType_ptr SymbType_make_memory_shared | ( | const SymbType_ptr | self | ) | [related] |
This function takes a NOT memory shared type and returns a memory shared one.
The input type should have a corresponding memory shared type. For example, function type and error type do not have memory shared instances.
| SymbType_ptr SymbType_make_set_type | ( | const SymbType_ptr | self | ) | [related] |
Returns a minimal set-type which the given type can be implicitly converted to, or NULL if this is impossible.
The implicit conversion is performed in accordance to the type order. NOTE: only memory-shared types can be given to this function.
| void SymbType_print | ( | const SymbType_ptr | self, | |
| MasterPrinter_ptr | printer, | |||
| FILE * | output_stream | |||
| ) | [related] |
Prints the type structure to the output stream.
This function is made very similar to print_node. If a Enum type was created with SymbType_create then all its values will be printed, otherwise the type was created with SymbTablePkg_..._type and simplified type name (instead of actual type values) is printed.
| char * SymbType_sprint | ( | const SymbType_ptr | self, | |
| MasterPrinter_ptr | printer | |||
| ) | [related] |
Return a string representation of the given type.
This function is made very similar to sprint_node. If an Enum type was created with SymbType_create then all its values will be printed, otherwise the type was created with SymbTablePkg_..._type and simplified type name (instead of actual type values) is printed.
The returned string must be released by the caller.
The returned string is allocated and has to be released by the caller
| node_ptr SymbType_to_node | ( | const SymbType_ptr | self, | |
| NodeMgr_ptr | nodemgr | |||
| ) | [related] |
1.6.1
