HrcDumper Struct Reference

Private and protected interface of class 'HrcDumper'. More...

#include <HrcDumper_private.h>

Public Member Functions
	INHERITS_FROM (EnvObject)
Data Fields
unsigned int	columns
void(*	dump_comment )(HrcDumper_ptr self, const char *msg)
void(*	dump_header )(HrcDumper_ptr self, const char *msg)
void(*	dump_node )(HrcDumper_ptr self, node_ptr node)
void(*	dump_snippet )(HrcDumper_ptr self, HrcDumperSnippet snippet, const HrcDumperInfo *info)
FILE *	fout
int	indent
boolean	indent_pending
size_t	indent_size
MasterPrinter_ptr	printer
boolean	use_indentation
boolean	use_mod_suffix
Related Functions
(Note that these are not member functions.)
void	hrc_dumper_anonymizer_dump_node (HrcDumper_ptr self, node_ptr node)
	Dumps a node.
void	hrc_dumper_anonymizer_dump_snippet (HrcDumper_ptr self, HrcDumperSnippet snippet, const HrcDumperInfo *info)
	Dumps a snippet.
void	hrc_dumper_debug_dump_snippet (HrcDumper_ptr self, HrcDumperSnippet snippet, const HrcDumperInfo *info)
void	hrc_dumper_deinit (HrcDumper_ptr self)
	The HrcDumper class private deinitializer.
void	hrc_dumper_dump_comment (HrcDumper_ptr self, const char *msg)
	Dumps a comment.
void	hrc_dumper_dump_header (HrcDumper_ptr self, const char *msg)
void	hrc_dumper_dump_indent (HrcDumper_ptr self)
void	hrc_dumper_dump_node (HrcDumper_ptr self, node_ptr node)
	Dumps a node.
void	hrc_dumper_dump_snippet (HrcDumper_ptr self, HrcDumperSnippet snippet, const HrcDumperInfo *info)
void	hrc_dumper_dump_var_type (HrcDumper_ptr self, node_ptr node)
	Prints the type of a variable.
void	hrc_dumper_init (HrcDumper_ptr self, const NuSMVEnv_ptr env, FILE *fout)
	The HrcDumper class private initializer.
void	hrc_dumper_nl (HrcDumper_ptr self)
	Implements indentation of a newline.
void	hrc_dumper_smv_dump_comment (HrcDumper_ptr self, const char *msg)
	Dumps a comment.
void	hrc_dumper_smv_dump_header (HrcDumper_ptr self, const char *msg)
void	hrc_dumper_smv_dump_snippet (HrcDumper_ptr self, HrcDumperSnippet snippet, const HrcDumperInfo *info)
void	hrc_dumper_xml_dump_comment (HrcDumper_ptr self, const char *msg)
	Dumps a comment.
void	hrc_dumper_xml_dump_snippet (HrcDumper_ptr self, HrcDumperSnippet snippet, const HrcDumperInfo *info)
HrcDumper_ptr	HrcDumper_create (const NuSMVEnv_ptr env, FILE *fout)
	The HrcDumper class constructor.
void	HrcDumper_dec_indent (HrcDumper_ptr self)
	Decrements the indent level.
void	HrcDumper_destroy (HrcDumper_ptr self)
	The HrcDumper class destructor.
VIRTUAL void	HrcDumper_dump_snippet (HrcDumper_ptr self, HrcDumperSnippet snippet, const HrcDumperInfo *info)
	Makes the dumper dump the given snippet.
void	HrcDumper_enable_indentation (HrcDumper_ptr self, boolean flag)
	Enables/disables the indentation.
void	HrcDumper_enable_mod_suffix (HrcDumper_ptr self, boolean flag)
	Controls if module names must be dumped with a (default) suffix or not.
void	HrcDumper_inc_indent (HrcDumper_ptr self)
	Increments the indent level.

Detailed Description

Private and protected interface of class 'HrcDumper'.

Public interface of class 'HrcDumper'.

Author:: Roberto Cavada This file can be included only by derived and friend classes

HrcDumper class definition derived from class Object

See also:: Base class Object

Author:: Roberto Cavada

Todo:: : Missing description

Definition of the public accessor for class HrcDumper

Member Function Documentation

HrcDumper::INHERITS_FROM ( EnvObject )

Friends And Related Function Documentation

void hrc_dumper_anonymizer_dump_node	(	HrcDumper_ptr	self,
		node_ptr	node
	)			`[related]`

Dumps a node.

void hrc_dumper_anonymizer_dump_snippet	(	HrcDumper_ptr	self,
		HrcDumperSnippet	snippet,
		const HrcDumperInfo *	info
	)			`[related]`

Dumps a snippet.

Here we handle only the few needed case (e.g. we need to not anonymize "main", for the others we call the super method)

void hrc_dumper_debug_dump_snippet	(	HrcDumper_ptr	self,
		HrcDumperSnippet	snippet,
		const HrcDumperInfo *	info
	)			`[related]`

void hrc_dumper_deinit ( HrcDumper_ptr self ) [related]

The HrcDumper class private deinitializer.

The HrcDumper class private deinitializer

See also:: HrcDumper_destroy

void hrc_dumper_dump_comment	(	HrcDumper_ptr	self,
		const char *	msg
	)			`[related]`

Dumps a comment.

void hrc_dumper_dump_header	(	HrcDumper_ptr	self,
		const char *	msg
	)			`[related]`

void hrc_dumper_dump_indent ( HrcDumper_ptr self ) [related]

void hrc_dumper_dump_node	(	HrcDumper_ptr	self,
		node_ptr	node
	)			`[related]`

Dumps a node.

Virtual unimplemented method

void hrc_dumper_dump_snippet	(	HrcDumper_ptr	self,
		HrcDumperSnippet	snippet,
		const HrcDumperInfo *	info
	)			`[related]`

void hrc_dumper_dump_var_type	(	HrcDumper_ptr	self,
		node_ptr	node
	)			`[related]`

Prints the type of a variable.

Prints the type of a variable. The printers used in compileWrite.c in compile package cannot be used in hrc, unless symbol table is used.

The printer manages the following types: BOOLEAN, INTEGER, REAL, UNSIGNED_WORD, SIGNED_WORD, SCALAR, WORD_ARRAY and ARRAY_TYPE.

void hrc_dumper_init	(	HrcDumper_ptr	self,
		const NuSMVEnv_ptr	env,
		FILE *	fout
	)			`[related]`

The HrcDumper class private initializer.

The HrcDumper class private initializer

See also:: HrcDumper_create

void hrc_dumper_nl ( HrcDumper_ptr self ) [related]

Implements indentation of a newline.

void hrc_dumper_smv_dump_comment	(	HrcDumper_ptr	self,
		const char *	msg
	)			`[related]`

Dumps a comment.

void hrc_dumper_smv_dump_header	(	HrcDumper_ptr	self,
		const char *	msg
	)			`[related]`

void hrc_dumper_smv_dump_snippet	(	HrcDumper_ptr	self,
		HrcDumperSnippet	snippet,
		const HrcDumperInfo *	info
	)			`[related]`

void hrc_dumper_xml_dump_comment	(	HrcDumper_ptr	self,
		const char *	msg
	)			`[related]`

Dumps a comment.

void hrc_dumper_xml_dump_snippet	(	HrcDumper_ptr	self,
		HrcDumperSnippet	snippet,
		const HrcDumperInfo *	info
	)			`[related]`

HrcDumper_ptr HrcDumper_create	(	const NuSMVEnv_ptr	env,
		FILE *	fout
	)			`[related]`

The HrcDumper class constructor.

AutomaticStart

The HrcDumper class constructor. Parameter fout belongs to self.

See also:: HrcDumper_destroy

void HrcDumper_dec_indent ( HrcDumper_ptr self ) [related]

Decrements the indent level.

Decrements the indent level. Each call must correspond to a call to inc_indent. An assertion fails if called when the indent level is zero.

See also:: HrcDumper_inc_indent

void HrcDumper_destroy ( HrcDumper_ptr self ) [related]

The HrcDumper class destructor.

The HrcDumper class destructor. This can be used also by all derivated classes.

See also:: HrcDumper_create

VIRTUAL void HrcDumper_dump_snippet	(	HrcDumper_ptr	self,
		HrcDumperSnippet	snippet,
		const HrcDumperInfo *	info
	)			`[related]`

Makes the dumper dump the given snippet.

This is a virtual method

See also:: HrcDumper_destroy

void HrcDumper_enable_indentation	(	HrcDumper_ptr	self,
		boolean	flag
	)			`[related]`

Enables/disables the indentation.

void HrcDumper_enable_mod_suffix	(	HrcDumper_ptr	self,
		boolean	flag
	)			`[related]`

Controls if module names must be dumped with a (default) suffix or not.

void HrcDumper_inc_indent ( HrcDumper_ptr self ) [related]

Increments the indent level.

Increments the indent level

See also:: HrcDumper_dec_indent

Field Documentation

unsigned int HrcDumper::columns

void(* HrcDumper::dump_comment)(HrcDumper_ptr self, const char *msg)

void(* HrcDumper::dump_header)(HrcDumper_ptr self, const char *msg)

void(* HrcDumper::dump_node)(HrcDumper_ptr self, node_ptr node)

void(* HrcDumper::dump_snippet)(HrcDumper_ptr self, HrcDumperSnippet snippet, const HrcDumperInfo *info)

FILE* HrcDumper::fout

int HrcDumper::indent

boolean HrcDumper::indent_pending

size_t HrcDumper::indent_size

MasterPrinter_ptr HrcDumper::printer

boolean HrcDumper::use_indentation

boolean HrcDumper::use_mod_suffix

The documentation for this struct was generated from the following files:

NuSMV/code/nusmv/core/hrc/dumpers/HrcDumper_private.h
NuSMV/code/nusmv/core/hrc/dumpers/HrcDumper.h
NuSMV/code/nusmv/core/hrc/dumpers/HrcDumperAnonymizer_private.h
NuSMV/code/nusmv/core/hrc/dumpers/HrcDumperDebug_private.h
NuSMV/code/nusmv/core/hrc/dumpers/HrcDumperSmv_private.h
NuSMV/code/nusmv/core/hrc/dumpers/HrcDumperXml_private.h

HrcDumper Struct Reference

Public Member Functions

Data Fields

Related Functions

Detailed Description

Member Function Documentation

Friends And Related Function Documentation

Field Documentation