NuSMV/code/nusmv/core/compile/symb_table/SymbTable.h File Reference

#include "nusmv/core/compile/symb_table/SymbLayer.h"
#include "nusmv/core/compile/symb_table/SymbCache.h"
#include "nusmv/core/cinit/NuSMVEnv.h"
#include "nusmv/core/compile/type_checking/TypeChecker.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/array.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/compile/symb_table/NFunction.h"
#include "nusmv/core/set/set.h"
#include "nusmv/core/compile/symb_table/ResolveSymbol.h"
#include "nusmv/core/utils/UStringMgr.h"
#include "nusmv/core/utils/Pair.h"
#include "nusmv/core/node/anonymizers/NodeAnonymizerBase.h"

Go to the source code of this file.

Data Structures
struct	SymbTableIter
Defines
#define	SYMB_TABLE(x)   ((SymbTable_ptr) x)
#define	SYMB_TABLE_CHECK_INSTANCE(x)   (nusmv_assert(SYMB_TABLE(x) != SYMB_TABLE(NULL)))
#define	SYMB_TABLE_FOREACH(self, iter, mask)
#define	SYMB_TABLE_FOREACH_FILTER(self, iter, mask, filter, arg)
Typedefs
typedef struct SymbTable_TAG *	SymbTable_ptr
typedef void(*	SymbTableForeachFun )(const SymbTable_ptr, const node_ptr sym, void *arg)
typedef boolean(*	SymbTableIterFilterFun )(const SymbTable_ptr table, const node_ptr sym, void *arg)
typedef void(*	SymbTableTriggerFun )(const SymbTable_ptr table, const node_ptr sym, SymbTableTriggerAction action, void *arg)
	Trigger called by the symbol table when a symbol change status.
Enumerations
enum	SymbCategory {   SYMBOL_INVALID = 0, SYMBOL_CONSTANT, SYMBOL_FROZEN_VAR, SYMBOL_STATE_VAR,   SYMBOL_INPUT_VAR, SYMBOL_STATE_DEFINE, SYMBOL_INPUT_DEFINE, SYMBOL_STATE_INPUT_DEFINE,   SYMBOL_NEXT_DEFINE, SYMBOL_STATE_NEXT_DEFINE, SYMBOL_INPUT_NEXT_DEFINE, SYMBOL_STATE_INPUT_NEXT_DEFINE,   SYMBOL_DEFINE, SYMBOL_FUNCTION, SYMBOL_PARAMETER, SYMBOL_ARRAY_DEFINE,   SYMBOL_VARIABLE_ARRAY }
	Describes the kind of symbol. More...
enum	SymbFilterType {   VFT_CURRENT = 1, VFT_NEXT = VFT_CURRENT << 1, VFT_INPUT = VFT_CURRENT << 2, VFT_FROZEN = VFT_CURRENT << 3,   VFT_DEFINE = VFT_CURRENT << 4, VFT_FUNCTION = VFT_CURRENT << 5, VFT_CONSTANTS = VFT_CURRENT << 6, VFT_STATE = (VFT_CURRENT | VFT_NEXT),   VFT_CURR_INPUT = (VFT_CURRENT | VFT_INPUT), VFT_CURR_FROZEN = (VFT_CURRENT | VFT_FROZEN), VFT_CNIF, VFT_CNIFD = (VFT_CNIF | VFT_DEFINE),   VFT_ALL = (VFT_CNIFD | VFT_FUNCTION | VFT_CONSTANTS) }
	Controls the filter type in some search dependencies routines. More...
enum	SymbTableTriggerAction { ST_TRIGGER_SYMBOL_ADD, ST_TRIGGER_SYMBOL_REMOVE, ST_TRIGGER_SYMBOL_REDECLARE }
enum	SymbTableType {   STT_NONE = 0, STT_CONSTANT = 1, STT_STATE_VAR = STT_CONSTANT << 1, STT_INPUT_VAR = STT_CONSTANT << 2,   STT_FROZEN_VAR = STT_CONSTANT << 3, STT_VAR, STT_DEFINE = STT_CONSTANT << 4, STT_ARRAY_DEFINE = STT_CONSTANT << 5,   STT_PARAMETER = STT_CONSTANT << 6, STT_FUNCTION = STT_CONSTANT << 7, STT_VARIABLE_ARRAY = STT_CONSTANT << 8, STT_ALL }
Functions
void	SymbTable_clear_handled_remove_action_hash (const SymbTable_ptr st, const node_ptr sym, SymbTableTriggerAction action, void *arg)
	This function can be used with SymbTable_get_handled_hash_ptr for the parameter remove_action.

---

Define Documentation

#define SYMB_TABLE

(

x

)

((SymbTable_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define SYMB_TABLE_CHECK_INSTANCE

(

x

)

(nusmv_assert(SYMB_TABLE(x) != SYMB_TABLE(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

#define SYMB_TABLE_FOREACH	(	self,
		iter,
		mask		)

Value:

for (SymbTable_gen_iter(self, &iter, mask);   \
       !SymbTable_iter_is_end(self, &iter);     \
       SymbTable_iter_next(self, &iter))

Todo:

Missing synopsis

Todo:

Missing description

#define SYMB_TABLE_FOREACH_FILTER	(	self,
		iter,
		mask,
		filter,
		arg		)

Value:

for (SymbTable_gen_iter(self, &iter, mask),                           \
           SymbTable_iter_set_filter(self, &iter, filter, arg);         \
       !SymbTable_iter_is_end(self, &iter);                             \
       SymbTable_iter_next(self, &iter))

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef struct SymbTable_TAG* SymbTable_ptr

typedef void(* SymbTableForeachFun)(const SymbTable_ptr, const node_ptr sym, void *arg)

Todo:

Missing synopsis

Todo:

Missing description

typedef boolean(* SymbTableIterFilterFun)(const SymbTable_ptr table, const node_ptr sym, void *arg)

Todo:

Missing synopsis

Todo:

Missing description

typedef void(* SymbTableTriggerFun)(const SymbTable_ptr table, const node_ptr sym, SymbTableTriggerAction action, void *arg)

Trigger called by the symbol table when a symbol change status.

---

Enumeration Type Documentation

enum SymbCategory

Describes the kind of symbol.

Todo:

Missing description

Enumerator:

SYMBOL_INVALID
SYMBOL_CONSTANT
SYMBOL_FROZEN_VAR
SYMBOL_STATE_VAR
SYMBOL_INPUT_VAR
SYMBOL_STATE_DEFINE
SYMBOL_INPUT_DEFINE
SYMBOL_STATE_INPUT_DEFINE
SYMBOL_NEXT_DEFINE
SYMBOL_STATE_NEXT_DEFINE
SYMBOL_INPUT_NEXT_DEFINE
SYMBOL_STATE_INPUT_NEXT_DEFINE
SYMBOL_DEFINE
SYMBOL_FUNCTION
SYMBOL_PARAMETER
SYMBOL_ARRAY_DEFINE
SYMBOL_VARIABLE_ARRAY

enum SymbFilterType

Controls the filter type in some search dependencies routines.

Controls the filter type in some search dependencies routines. The available filters are:

VFT_CURRENT

filters out the current state variables

VFT_NEXT

filters out the next state variables

VFT_INPUT

filters out the input variables

VFT_FROZEN

filters out the frozen variables

VFT_DEFINE

filters out the DEFINE

VFT_FUNCTION

filters out the FUNCTION

VFT_STATE

filters out the current and next state variables

VFT_CURR_INPUT

filters out the current state and input variables

VFT_CURR_FROZEN

filters out the current state and frozen variables

VFT_CNIF

filters out all the variables. Constants NOT included

VFT_CNIFD

filters out all the variables and DEFINE. Constants NOT included

VFT_ALL

filters out all the variables, function, DEFINE and constants

Combined modes can be obtained by bit-or: for example VFT_NEXT | VFT_INPUT is going to search for the variables which are next or input variables

Enumerator:

VFT_CURRENT
VFT_NEXT
VFT_INPUT
VFT_FROZEN
VFT_DEFINE
VFT_FUNCTION
VFT_CONSTANTS
VFT_STATE
VFT_CURR_INPUT
VFT_CURR_FROZEN
VFT_CNIF
VFT_CNIFD
VFT_ALL

enum SymbTableTriggerAction

Enumerator:

ST_TRIGGER_SYMBOL_ADD
ST_TRIGGER_SYMBOL_REMOVE
ST_TRIGGER_SYMBOL_REDECLARE

enum SymbTableType

Enumerator:

STT_NONE
STT_CONSTANT
STT_STATE_VAR
STT_INPUT_VAR
STT_FROZEN_VAR
STT_VAR
STT_DEFINE
STT_ARRAY_DEFINE
STT_PARAMETER
STT_FUNCTION
STT_VARIABLE_ARRAY
STT_ALL

---

Function Documentation

void SymbTable_clear_handled_remove_action_hash	(	const SymbTable_ptr	st,
		const node_ptr	sym,
		SymbTableTriggerAction	action,
		void *	arg
	)

This function can be used with SymbTable_get_handled_hash_ptr for the parameter remove_action.

arg is an AssocAndDestroy_ptr. The type of this function is SymbTableTriggerFun

See also:

SymbTable_get_handled_hash_ptr