#include <stdio.h>#include "nusmv/core/node/node.h"#include "nusmv/core/utils/utils.h"#include "nusmv/core/node/printers/MasterPrinter.h"Go to the source code of this file.
Defines | |
| #define | nullType SYMB_TYPE(NULL) |
| Generic and symbolic encoding. | |
| #define | SYMB_TYPE(x) ((SymbType_ptr) x) |
| #define | SYMB_TYPE_CHECK_INSTANCE(x) (nusmv_assert(SYMB_TYPE(x) != SYMB_TYPE(NULL))) |
Typedefs | |
| typedef struct SymbType_TAG * | SymbType_ptr |
Enumerations | |
| enum | Enum_types { ENUM_TYPE_PURE_INT, ENUM_TYPE_PURE_SYMBOLIC, ENUM_TYPE_INT_SYMBOLIC } |
| enum | SymbTypeTag { SYMB_TYPE_NONE, SYMB_TYPE_STATEMENT, SYMB_TYPE_BOOLEAN, SYMB_TYPE_ENUM, SYMB_TYPE_INTEGER, SYMB_TYPE_REAL, SYMB_TYPE_NFUNCTION, SYMB_TYPE_CONTINUOUS, SYMB_TYPE_SIGNED_WORD, SYMB_TYPE_UNSIGNED_WORD, SYMB_TYPE_WORDARRAY, SYMB_TYPE_ARRAY, SYMB_TYPE_SET_BOOL, SYMB_TYPE_SET_INT, SYMB_TYPE_SET_SYMB, SYMB_TYPE_SET_INT_SYMB, SYMB_TYPE_INTARRAY, SYMB_TYPE_ERROR } |
Possible kinds of a type. More... | |
Functions | |
| SymbType_ptr | SymbType_convert_right_to_left (SymbType_ptr leftType, SymbType_ptr rightType) |
| Returns the left type, if the right one can be implicitly converted to the left one. NULL - otherwise. | |
| SymbType_ptr | SymbType_get_greater (const SymbType_ptr type1, const SymbType_ptr type2) |
| Returns one of the given types, if the other one can be implicitly converted to the former one. Otherwise - nullType. | |
| SymbType_ptr | SymbType_get_minimal_common (SymbType_ptr type1, SymbType_ptr type2) |
| Returns the minimal type to which the both given types can be converted, or Nil if there is none. | |
| boolean | SymbType_is_back_comp (const SymbType_ptr type) |
| returns true if the given type is "backward compatible", i.e. a enum or integer type. | |
| #define nullType SYMB_TYPE(NULL) |
| #define SYMB_TYPE | ( | x | ) | ((SymbType_ptr) x) |
| #define SYMB_TYPE_CHECK_INSTANCE | ( | x | ) | (nusmv_assert(SYMB_TYPE(x) != SYMB_TYPE(NULL))) |
| typedef struct SymbType_TAG* SymbType_ptr |
| enum Enum_types |
| enum SymbTypeTag |
Possible kinds of a type.
The tags of types that a variable or an expression can have. Note that a variable cannot have a set type.
| SymbType_ptr SymbType_convert_right_to_left | ( | SymbType_ptr | leftType, | |
| SymbType_ptr | rightType | |||
| ) |
Returns the left type, if the right one can be implicitly converted to the left one. NULL - otherwise.
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_get_greater | ( | const SymbType_ptr | type1, | |
| const SymbType_ptr | type2 | |||
| ) |
Returns one of the given types, if the other one can be implicitly converted to the former one. Otherwise - nullType.
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_get_minimal_common | ( | SymbType_ptr | type1, | |
| SymbType_ptr | type2 | |||
| ) |
Returns the minimal type to which the both given types can be converted, or Nil if there is none.
The implicit conversion is performed in accordance to the type order. NOTE: only memory-shared types can be given to this function except for SYMB_TYPE_ARRAY which can be non-memory shared
| boolean SymbType_is_back_comp | ( | const SymbType_ptr | type | ) |
returns true if the given type is "backward compatible", i.e. a enum or integer type.
We distinguish "old" types because we may want to turn off the type checking on these types for backward compatibility. Integer is also considered as "old", because an enum of integer values is always casted to Integer.
1.6.1