-
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.
-
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.
-
UsageHrcWriteModel()
- Prints the usage of the command UsageHrcWriteModel
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/04/06 21h:13