NuSMV/code/nusmv/core/trace/Trace_private.h File Reference

#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/utils/array.h"
#include "nusmv/core/utils/error.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/utils/EnvObject_private.h"

Go to the source code of this file.

Data Structures
struct	Trace
	Trace Class. More...
struct	TraceDefineFrame
struct	TraceFrozenFrame
struct	TraceVarFrame
Defines
#define	CHECK(cond)
#define	TRACE_DEFINE_FRAME(x)   ((TraceDefineFrame_ptr) x)
#define	TRACE_DEFINE_FRAME_CHECK_INSTANCE(x)   (nusmv_assert(TRACE_DEFINE_FRAME(x) != TRACE_DEFINE_FRAME(NULL)))
#define	TRACE_FROZEN_FRAME(x)   ((TraceFrozenFrame_ptr) x)
#define	TRACE_FROZEN_FRAME_CHECK_INSTANCE(x)   (nusmv_assert(TRACE_FROZEN_FRAME(x) != TRACE_FROZEN_FRAME(NULL)))
#define	TRACE_VAR_FRAME(x)   ((TraceVarFrame_ptr) x)
#define	TRACE_VAR_FRAME_CHECK_INSTANCE(x)   (nusmv_assert(TRACE_VAR_FRAME(x) != TRACE_VAR_FRAME(NULL)))
Typedefs
typedef struct TraceDefineFrame_TAG *	TraceDefineFrame_ptr
typedef struct TraceFrozenFrame_TAG *	TraceFrozenFrame_ptr
typedef struct TraceVarFrame_TAG *	TraceVarFrame_ptr
Enumerations
enum	TraceSection {   TRACE_SECTION_INVALID = 0, TRACE_SECTION_FROZEN_VAR, TRACE_SECTION_STATE_VAR, TRACE_SECTION_INPUT_VAR,   TRACE_SECTION_STATE_DEFINE, TRACE_SECTION_INPUT_DEFINE, TRACE_SECTION_STATE_INPUT_DEFINE, TRACE_SECTION_NEXT_DEFINE,   TRACE_SECTION_STATE_NEXT_DEFINE, TRACE_SECTION_INPUT_NEXT_DEFINE, TRACE_SECTION_STATE_INPUT_NEXT_DEFINE, TRACE_SECTION_END }
	The private header file for the Trace class. More...
Functions
TraceSection	trace_category_to_section (const SymbCategory category)
Trace_ptr	trace_create (SymbTable_ptr st, const char *desc, const TraceType type, NodeList_ptr symbols, boolean is_volatile, boolean allow_bits)
TraceIter	trace_iter_get_next (const TraceIter iter)
TraceIter	trace_iter_get_prev (const TraceIter iter)
SymbCategory	trace_section_to_category (const TraceSection section)
boolean	trace_step_iter_fetch (TraceStepIter *step_iter, node_ptr *symb, node_ptr *value)
const char *	trace_symb_category_to_string (const SymbCategory category)
boolean	trace_symbols_iter_fetch (TraceSymbolsIter *symbols_iter, node_ptr *symb)

---

Define Documentation

#define CHECK

(

cond

)

#define TRACE_DEFINE_FRAME

(

x

)

((TraceDefineFrame_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define TRACE_DEFINE_FRAME_CHECK_INSTANCE

(

x

)

(nusmv_assert(TRACE_DEFINE_FRAME(x) != TRACE_DEFINE_FRAME(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

#define TRACE_FROZEN_FRAME

(

x

)

((TraceFrozenFrame_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define TRACE_FROZEN_FRAME_CHECK_INSTANCE

(

x

)

(nusmv_assert(TRACE_FROZEN_FRAME(x) != TRACE_FROZEN_FRAME(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

#define TRACE_VAR_FRAME

(

x

)

((TraceVarFrame_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define TRACE_VAR_FRAME_CHECK_INSTANCE

(

x

)

(nusmv_assert(TRACE_VAR_FRAME(x) != TRACE_VAR_FRAME(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef struct TraceDefineFrame_TAG* TraceDefineFrame_ptr

typedef struct TraceFrozenFrame_TAG* TraceFrozenFrame_ptr

typedef struct TraceVarFrame_TAG* TraceVarFrame_ptr

---

Enumeration Type Documentation

enum TraceSection

The private header file for the Trace class.

Author:

Marco Pensallorto optional

Enumerator:

TRACE_SECTION_INVALID
TRACE_SECTION_FROZEN_VAR
TRACE_SECTION_STATE_VAR
TRACE_SECTION_INPUT_VAR
TRACE_SECTION_STATE_DEFINE
TRACE_SECTION_INPUT_DEFINE
TRACE_SECTION_STATE_INPUT_DEFINE
TRACE_SECTION_NEXT_DEFINE
TRACE_SECTION_STATE_NEXT_DEFINE
TRACE_SECTION_INPUT_NEXT_DEFINE
TRACE_SECTION_STATE_INPUT_NEXT_DEFINE
TRACE_SECTION_END

---

Function Documentation

TraceSection trace_category_to_section

(

const SymbCategory

category

)

Todo:

Missing synopsis

Todo:

Missing description

Trace_ptr trace_create	(	SymbTable_ptr	st,
		const char *	desc,
		const TraceType	type,
		NodeList_ptr	symbols,
		boolean	is_volatile,
		boolean	allow_bits
	)

AutomaticStart

Todo:

Missing synopsis

Todo:

Missing description

TraceIter trace_iter_get_next

(

const TraceIter

iter

)

Todo:

Missing synopsis

Todo:

Missing description

TraceIter trace_iter_get_prev

(

const TraceIter

iter

)

Todo:

Missing synopsis

Todo:

Missing description

SymbCategory trace_section_to_category

(

const TraceSection

section

)

Todo:

Missing synopsis

Todo:

Missing description

boolean trace_step_iter_fetch	(	TraceStepIter *	step_iter,
		node_ptr *	symb,
		node_ptr *	value
	)

Todo:

Missing synopsis

Todo:

Missing description

const char* trace_symb_category_to_string

(

const SymbCategory

category

)

Todo:

Missing synopsis

Todo:

Missing description

boolean trace_symbols_iter_fetch	(	TraceSymbolsIter *	symbols_iter,
		node_ptr *	symb
	)

Todo:

Missing synopsis

Todo:

Missing description