node_ptr
hrc_prefix_utils_flatten_instance_name(
HrcNode_ptr instance
)
Given an instance returns its flattened name.
node_ptr
hrc_prefix_utils_get_first_subcontext(
node_ptr symbol
)
Get the first subcontext of the given symbol.
Search the second CONTEXT or DOT node in symbol and returns it. If it
is not found then Nil is returned.
DOT and CONTEXT nodes are always searched in the car node.
Set_t
hrc_prefix_utils_get_prefix_symbols(
Set_t symbol_set,
node_ptr prefix
)
Given a set of symbol returns a new set that
contains only symbols that have a given prefix.
The returned set must be destroyed by the caller.
boolean
hrc_prefix_utils_is_subprefix(
node_ptr subprefix,
node_ptr prefix
)
Returns true if subprefix is contained in prefix.
node_ptr
hrc_prefix_utils_remove_context(
node_ptr identifier,
node_ptr context
)
Removes context from identifier.
If context is not
boolean
hrc_write_assign_list(
FILE* out,
int assign_node_type,
node_ptr assign_list
)
Writes ASSIGN declarations in SMV format on a
file.
Function returns true if at least an assign was written
boolean
hrc_write_constants(
FILE * out,
node_ptr constants_list
)
Prints in the output file the SMV
representations of constants list.
Function returns true if at least a constant was printed.
void
hrc_write_declare_module_variables(
FILE * ofile,
HrcNode_ptr child,
st_table* printed_module_map,
boolean append_suffix
)
Declare a module variables, setting the module
to use and the actual parameters.
Side Effects printed_module_map is changed in the recursive
calls of the the function.
boolean
hrc_write_expr_split(
FILE* out,
node_ptr n,
const char* s
)
Writes a generic expression prefixed by a given
string in SMV format on a file.
Returns true if at least one expression was printed.
void
hrc_write_expr(
FILE* out,
node_ptr n,
const char* s
)
Writes a generic expression prefixed by a given
string in SMV format on a file.
void
hrc_write_module_instance(
FILE * ofile,
HrcNode_ptr hrcNode,
st_table* printed_module_map,
boolean append_suffix
)
Writes the SMV translation of the instance
module contained in hrcNode on file.
Side Effects printed_module_map is changed to keep track of
printed modules.
void
hrc_write_parameters(
FILE* ofile,
node_ptr parameters_list
)
Prints a list of parameters for module
declaration or instantiation.
The parameter list is printed enclosed by brackets, every parameter
is separated by colon.
void
hrc_write_print_array_defines(
FILE* out,
HrcNode_ptr hrcNode
)
Writes the ARRAY DEFINE declarations contained in hrcNode.
void
hrc_write_print_assign(
FILE * out,
node_ptr lhs,
node_ptr rhs
)
Prints an assignement statement
void
hrc_write_print_defines(
FILE* out,
HrcNode_ptr hrcNode
)
Writes DEFINE declarations in SMV format on a
file.
void
hrc_write_print_var_list(
FILE* out,
node_ptr var_list
)
Prints a list of variables.
void
hrc_write_print_vars(
FILE* out,
HrcNode_ptr hrcNode
)
Prints the variable of the module contained in
hrcNode.
The sections printed are VAR, IVAR and FROZENVAR.
void
hrc_write_spec_pair_list(
FILE* out,
node_ptr pair_list,
char* section_name
)
Writes a list of specification that contains
pairs in SMV format.
boolean
hrc_write_spec_split(
FILE* out,
node_ptr n,
const char* s
)
Writes a specification list prefixed by a given
string in SMV format on a file.
Returns true if at least one specification was printed.
void
hrc_write_specifications(
FILE* out,
HrcNode_ptr hrcNode
)
Writes all the specifications of a module instance.
void
hrc_write_spec(
FILE* out,
node_ptr spec,
const char* msg
)
Prints in out file the specification.