NuSMV/code/nusmv/core/compile/dependency/DependencyBase_private.h File Reference

#include "nusmv/core/compile/dependency/DependencyBase.h"
#include "nusmv/core/node/NodeWalker.h"
#include "nusmv/core/node/NodeWalker_private.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/defs.h"

Go to the source code of this file.

Data Structures
struct	DependencyBase
	Private and protected interface of class 'DependencyBase'. More...
Defines
#define	_INSERT_IN_HASH(dependencies_hash, key, result, is_to_be_inserted)
#define	_THROW(symb_table, formula, context, filter, preserve_time, time, dependency_hash)
	Short way of calling dependency_base_throw_get_definition.

---

Define Documentation

#define _INSERT_IN_HASH	(	dependencies_hash,
		key,
		result,
		is_to_be_inserted		)

Value:

if (is_to_be_inserted) {                                                    \
    /* this assures absence of leaks */                                       \
    nusmv_assert((Set_t) NULL ==                                              \
                 formula_dependency_lookup_hash(dependencies_hash,            \
                                                NODE_PTR(&key)));             \
    if (Set_IsEmpty(result)) {                                                \
      formula_dependency_insert_hash(dependencies_hash, NODE_PTR(&key),       \
                                     EMPTY_DEP_SET);                          \
    }                                                                         \
    else formula_dependency_insert_hash(dependencies_hash, NODE_PTR(&key),    \
                                        result);                              \
  }                                                                           \

Macro used to insert a result in the hash avoiding leaks.

#define _THROW	(	symb_table,
		formula,
		context,
		filter,
		preserve_time,
		time,
		dependency_hash		)

Value:

dependency_base_throw_get_dependencies(DEPENDENCY_BASE(self),                \
                                         symb_table,                           \
                                         formula, context, filter,             \
                                         preserve_time,                        \
                                         time, dependency_hash)

Short way of calling dependency_base_throw_get_definition.

Use this macro to recursively recall the get_definition function.