int 
CommandHrcDumpModel(
  int  argc, 
  char ** argv 
)
Writes the SMV model contained in the root node of the hrc structure.

Defined in hrcCmd.c

int 
CommandHrcWriteModel(
  int  argc, 
  char ** argv 
)
Writes the SMV model contained in the root node of the hrc structure.

Defined in hrcCmd.c

void 
Hrc_DumpModel(
  HrcNode_ptr  hrcNode, 
  HrcDumper_ptr  dumper 
)
Prints the SMV module for the hrcNode. If the flag append_suffix is true then the suffix HRC_WRITE_MODULE_SUFFIX is appended when a module type is printed. So HRC_WRITE_MODULE_SUFFIX is appended to the module name in module declarations and to the module name in a module instantiation. The feature is needed for testing to avoid name clash among modules names when the original model and the model generated from hrc are merged.

Defined in hrcDump.c

void 
Hrc_WriteModel(
  HrcNode_ptr  hrcNode, 
  FILE * ofile, 
  boolean  append_suffix 
)
Prints the SMV module for the hrcNode. If the flag append_suffix is true then the suffix HRC_WRITE_MODULE_SUFFIX is appended when a module type is printed. So HRC_WRITE_MODULE_SUFFIX is appended to the module name in module declarations and to the module name in a module instantiation. The feature is needed for testing to avoid name clash among modules names when the original model and the model generated from hrc are merged.

Defined in hrcWrite.c

void 
Hrc_init_cmd(
    
)
Initializes the commands of the hrc package.

Defined in hrcCmd.c

void 
Hrc_init(
    
)
Initializes the hrc package. The initialization consists of the allocation of the mainHrcNode global variable and the initialization of the hrc package commands.

See Also TracePkg_quit
Defined in hrc.c

void 
Hrc_quit_cmd(
    
)
Removes the commands provided by the hrc package.

Defined in hrcCmd.c

void 
Hrc_quit(
    
)
Quits the hrc package, freeing the global variable mainHrcNode and removing the hrc commands.

See Also TracePkg_init
Defined in hrc.c

static int 
UsageHrcDumpModel(
    
)
Prints the usage of the command UsageHrcDumpModel

Defined in hrcCmd.c

static int 
UsageHrcWriteModel(
    
)
Prints the usage of the command UsageHrcWriteModel

Defined in hrcCmd.c

void 
hrc_dump_compile_info(
  HrcNode_ptr  hrcNode, 
  HrcDumper_ptr  dumper, 
  HrcDumperInfo* info 
)
Dumps the compiler information

Defined in hrcDump.c

void 
hrc_dump_module_instance(
  HrcNode_ptr  hrcNode, 
  HrcDumper_ptr  dumper, 
  HrcDumperInfo* info, 
  hash_ptr  printed_module_map 
)
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.

Defined in hrcDump.c

node_ptr 
hrc_prefix_utils_add_context(
  node_ptr  context, 
  node_ptr  expression 
)
Build the expression prefixed by context. If expression is of DOT or CONTEXT type we cannot build the tree DOT(context, expression). We need to recursively visit expression to build a correct DOT tree.

Defined in hrcPrefixUtils.c

node_ptr 
hrc_prefix_utils_assign_module_name(
  HrcNode_ptr  instance, 
  node_ptr  instance_name 
)
Creates a new name for the module instance. The generated module name is _

Defined in hrcPrefixUtils.c

node_ptr 
hrc_prefix_utils_flatten_instance_name(
  HrcNode_ptr  instance 
)
Given an instance returns its flattened name.

Defined in hrcPrefixUtils.c

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.

Defined in hrcPrefixUtils.c

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.

Defined in hrcPrefixUtils.c

boolean 
hrc_prefix_utils_is_subprefix(
  node_ptr  subprefix, 
  node_ptr  prefix 
)
Returns true if subprefix is contained in prefix.

Defined in hrcPrefixUtils.c

node_ptr 
hrc_prefix_utils_remove_context(
  node_ptr  identifier, 
  node_ptr  context 
)
Removes context from identifier. If context is not

Defined in hrcPrefixUtils.c

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

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

void 
hrc_write_print_array_defines(
  FILE* out, 
  HrcNode_ptr  hrcNode 
)
Writes the ARRAY DEFINE declarations contained in hrcNode.

Defined in hrcWrite.c

void 
hrc_write_print_assign(
  FILE * out, 
  node_ptr  lhs, 
  node_ptr  rhs 
)
Prints an assignement statement

Defined in hrcWrite.c

void 
hrc_write_print_defines(
  FILE* out, 
  HrcNode_ptr  hrcNode 
)
Writes DEFINE declarations in SMV format on a file.

Defined in hrcWrite.c

void 
hrc_write_print_var_list(
  FILE* out, 
  node_ptr  var_list 
)
Prints a list of variables.

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

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.

Defined in hrcWrite.c

void 
hrc_write_specifications(
  FILE* out, 
  HrcNode_ptr  hrcNode 
)
Writes all the specifications of a module instance.

Defined in hrcWrite.c

void 
hrc_write_spec(
  FILE* out, 
  node_ptr  spec, 
  const char* msg 
)
Prints in out file the specification.

Defined in hrcWrite.c

static void 
print_scalar_type(
  FILE* out, 
  node_ptr  node 
)
Prints the scalar type of a variable. The printer takes care of reversing the CONS list that contains the enumeration to preserve the order of the literals in the source model.

See Also print_variable_type
Defined in hrcWrite.c

static void 
print_variable_type(
  FILE* out, 
  node_ptr  node 
)
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.

Defined in hrcWrite.c

 
(
    
)
Suffix used to rename module names and module variables

Defined in hrcWrite.c

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