hrc.h
External header file
hrcInt.h
Internal header file
hrc.c
Package level routines for hrc package.
hrcCmd.c
Shell interface to the hrc package.
hrcDump.c
Creation of an SMV file of an Hrc structure
hrcPrefixUtils.c
Utility functions used to concatenate/remove prefixes from names.
hrcWrite.c
Creation of an SMV file of an Hrc structure

hrc.h

External header file

By: Marco Roveri

See Alsooptional


hrcInt.h

Internal header file

By: Sergio Mover


hrc.c

Package level routines for hrc package.

By: Sergio Mover

This file contains the package level routines for the hrc package. Among these routines there are the init and quit routines that initializes/deinitializes the package global variable (mainHrcNode) and the package commands.

See AlsohrcCmd.c

Hrc_init()
Initializes the hrc package.
Hrc_quit()
Quits the hrc package.

hrcCmd.c

Shell interface to the hrc package.

By: Sergio Mover

This file contains the interface of the compile package with the interactive shell.

Hrc_init_cmd()
Initializes the commands of the hrc package.
Hrc_quit_cmd()
Removes the commands provided by the hrc package.
CommandHrcWriteModel()
Writes the SMV model contained in the root node of the hrc structure.
CommandHrcDumpModel()
Writes the SMV model contained in the root node of the hrc structure.
UsageHrcWriteModel()
Prints the usage of the command UsageHrcWriteModel
UsageHrcDumpModel()
Prints the usage of the command UsageHrcDumpModel

hrcDump.c

Creation of an SMV file of an Hrc structure

By: Sergio Mover

Creates a SMV file from the hrc structure. The exported function Hrc_WriteModel allows to print a HrcNode_ptr structure on a file. The file contains static functions needed to print an SMV file given the hrc structure.

Hrc_DumpModel()
Prints the SMV module for the hrcNode.
hrc_dump_module_instance()
Writes the SMV translation of the instance module contained in hrcNode on file.
hrc_dump_compile_info()
Dumps the compiler information

hrcPrefixUtils.c

Utility functions used to concatenate/remove prefixes from names.

By: Sergio Mover

Utility functions used to concatenate/remove prefixes from names.

hrc_prefix_utils_get_prefix_symbols()
Given a set of symbol returns a new set that contains only symbols that have a given prefix.
hrc_prefix_utils_is_subprefix()
Returns true if subprefix is contained in prefix.
hrc_prefix_utils_add_context()
Build the expression prefixed by context.
hrc_prefix_utils_get_first_subcontext()
Get the first subcontext of the given symbol.
hrc_prefix_utils_remove_context()
Removes context from identifier.
hrc_prefix_utils_assign_module_name()
Creates a new name for the module instance.
hrc_prefix_utils_flatten_instance_name()
Given an instance returns its flattened name.

hrcWrite.c

Creation of an SMV file of an Hrc structure

By: Sergio Mover

Creates a SMV file from the hrc structure. The exported function Hrc_WriteModel allows to print a HrcNode_ptr structure on a file. The file contains static functions needed to print an SMV file given the hrc structure.

()
Suffix used to rename module names and module variables
Hrc_WriteModel()
Prints the SMV module for the hrcNode.
hrc_write_module_instance()
Writes the SMV translation of the instance module contained in hrcNode on file.
hrc_write_declare_module_variables()
Declare a module variables, setting the module to use and the actual parameters.
hrc_write_parameters()
Prints a list of parameters for module declaration or instantiation.
hrc_write_print_vars()
Prints the variable of the module contained in hrcNode.
hrc_write_print_var_list()
Prints a list of variables.
hrc_write_print_defines()
Writes DEFINE declarations in SMV format on a file.
hrc_write_print_array_defines()
Writes the ARRAY DEFINE declarations contained in hrcNode.
hrc_write_expr_split()
Writes an expression in SMV format on a file.
hrc_write_spec_split()
Writes a specification list in SMV format on a file.
hrc_write_expr()
Writes expression in SMV format on a file.
hrc_write_spec()
Prints the given specification.
hrc_write_specifications()
Writes all the specifications of a module instance.
hrc_write_assign_list()
Writes ASSIGN declarations in SMV format on a file.
hrc_write_print_assign()
Prints an assignement statement
hrc_write_spec_pair_list()
Writes a list of specification that contains pairs in SMV format.
hrc_write_constants()
Prints in the output file the SMV representations of constants list.
print_variable_type()
Prints the type of a variable.
print_scalar_type()
Prints the scalar type of a variable.

Last updated on 2011/06/16 12h:15