-
Compile_CheckAssigns()
- Semantic checks on assignments of the module.
-
Compile_ConstructHierarchy()
- Traverses the module hierarchy and extracts the
information needed to compile the automaton.
-
Compile_DeclareVariable()
- Instantiates the given variable.
-
Compile_FlattenHierarchy()
- Traverse the module hierarchy, collect all required
the informations and flatten the hierarchy.
-
Compile_FlattenSexpExpandDefine()
- Flattens an expression and expands defined symbols.
-
Compile_FlattenSexp()
- Builds the flattened version of an expression.
-
Compile_InstantiateType()
- convert a type from node_ptr-form constructed by parser
into not-memory-shared SymbType_ptr.
-
Compile_ProcessHierarchy()
- This function processes a hierarchy after
collecting all its subparts.
-
Compile_WriteBoolFsm_udg()
- Prints the boolean FSM of an SMV model.
-
Compile_WriteBoolFsm()
- Prints the boolean FSM of an SMV model.
-
Compile_WriteBoolModel_udg()
- Prints the given boolean model
-
Compile_WriteBoolModel()
- Prints the given boolean model
-
Compile_WriteBoolSpecs_udg()
- Prints the boolean specifications of an SMV model.
-
Compile_WriteBoolSpecs()
- Prints the boolean specifications of an SMV model.
-
Compile_WriteFlattenFsm_udg()
- Prints the flatten version of FSM of an SMV model.
-
Compile_WriteFlattenFsm()
- Prints the flatten version of FSM of an SMV model.
-
Compile_WriteFlattenModel_udg()
- This code is experimental
-
Compile_WriteFlattenModel()
-
-
Compile_WriteFlattenSpecs_udg()
- Prints the given flatten specifications.
-
Compile_WriteFlattenSpecs()
- Prints the given flatten specifications.
-
Compile_WriteObfuscatedFlattenModel()
-
-
Compile_WriteRestrictedFlattenModel()
- Dumps the flatten model on the given FILE
-
Compile_check_if_bool_model_was_built()
- Checks if boolean model has been constructed
-
Compile_check_if_encoding_was_built()
- Checks if the variables enconding has been constructed
-
Compile_check_if_flat_model_was_built()
- Checks if flat model has been constructed
-
Compile_check_if_flattening_was_built()
- Checks if the flattening has been carried out
-
Compile_check_if_model_was_built()
- Checks if bdd model has been constructed
-
Compile_check_input_next()
- Checks that given expression contains either no input
variables in next.
-
Compile_check_next()
- Checks that given expression contains either no nested
next, or no next operator at all.
-
Compile_cleanup_booleanizer_cache_about()
- Cleans those hashed entries that are about a symbol that
is being removed
-
Compile_convert_to_dag_udg()
- Top level function to create dags from expressions
-
Compile_convert_to_dag()
- Top level function to create dags from expressions
-
Compile_destroy_dag_info_udg()
- Frees the content of given structures.
-
Compile_destroy_dag_info()
- Frees the content of given structures.
-
Compile_detexpr2bexpr_list()
- Converts a scalar expression into a boolean expression.
-
Compile_detexpr2bexpr()
- Converts a scalar expression into a boolean expression.
-
Compile_expr2bexpr()
- Converts a scalar expression into a boolean expression.
-
Compile_get_global_fsm_builder()
- Returns the global fsm builder
-
Compile_get_global_predicate_normaliser()
- Returns a global predicate normaliser
-
Compile_get_obfuscation_map()
- Generates the obfuscation map
-
Compile_init_cmd()
- Initializes the commands provided by this package
-
Compile_init()
- Initializes the compile package.
-
Compile_is_symbol_constant()
- Tells if the given node is a numeric/boolean constant
-
Compile_make_dag_info_udg()
-
-
Compile_make_dag_info()
-
-
Compile_make_sorted_vars_list_from_order()
- This function creates a new list of variables that will
contain the same symbols into 'vars', but ordered wrt to
'vars_order' content
-
Compile_obfuscate_expression()
- Apply the obfuscation over an expression
-
Compile_pop_distrib_ops()
- Simplifies the given property by exploiting
the distributivity of G, AG and H over AND, and distributivity of F, AF and O
over OR
-
Compile_print_matrix_define_udg()
- Prints a matrix define node to out file.
-
Compile_print_matrix_define()
- Prints a matrix define node to out file.
-
Compile_quit()
- Shut down the compile package
-
Compile_write_dag_defines_udg()
-
-
Compile_write_dag_defines()
-
-
compile_add_vars_to_hierarhcy()
- Given a fully resolved array name and its type the function
adds all the variables in the array to the hierarchy
-
compile_build_model()
- Builds the BDD fsm.
-
compile_check_print_io_atom_stack_assign()
-
-
compile_cmd_remove_assignments()
- Removes expression in the form "a := b" from the given
expression
-
compile_cmd_write_coi_prop_fsm()
- Dumps the model applied to COI for the given property
-
compile_cmd_write_coi_prop()
- Dumps the COI for the given property
-
compile_cmd_write_global_coi_fsm()
- Dumps on output_file the global coi FSM
-
compile_cmd_write_properties_coi()
- Dumps properties shared COI FSMs or sets
-
compile_concat_contexts()
- Concatenates contexts ctx1 and ctx2
-
compile_convert_to_dag_aux_udg()
-
-
compile_convert_to_dag_aux()
-
-
compile_create_boolean_model()
- Creates the master boolean fsm if needed.
A new layer called DETERM_LAYER_NAME
will be added if the bool fsm is created.
-
compile_create_dag_info_from_hierarchy_udg()
-
-
compile_create_dag_info_from_hierarchy()
-
-
compile_create_flat_model()
- creates the master scalar fsm if needed
-
compile_encode_variables()
- Encodes variables in the model (BDD only).
-
compile_flatten_eval_number()
- Tries to resolve recursively to a number
-
compile_flatten_get_int()
- Given a numeric constant in node_ptr representation
the function returns its value as int
-
compile_flatten_normalise_value_list()
- Aux function for the CompileFlatten_normalise_value_list
-
compile_flatten_resolve_name_recur()
- Performs the name "normalization", i.e.
applies find_node and merges context with the identifier.
-
compile_flatten_smv()
- Traverses the parse tree coming from the smv parser and
flattens the smv file.
-
compile_free_define_udg()
- Internal service of Compile_destroy_dag_info_udg
-
compile_free_define()
- Internal service of Compile_destroy_dag_info
-
compile_free_node_udg()
- Internal service of Compile_destroy_dag_info_udg
-
compile_free_node()
- Internal service of Compile_destroy_dag_info
-
compile_get_rid_of_define_chain()
- Get rids of chain of defines
-
compile_insert_assign_hrc()
- Add an assign declaration in hrc_result.
-
compile_instantiate_by_name()
- Starts the flattening from a given point in the
module hierarchy.
-
compile_instantiate_vars()
- Recursively applies compile_instantiate_var.
-
compile_instantiate_var()
- Instantiates the given variable.
-
compile_instantiate()
- Instantiates all in the body of a module.
-
compile_make_dag_info_aux_udg()
-
-
compile_make_dag_info_aux()
-
-
compile_pack_dag_info_udg()
-
-
compile_pack_dag_info()
-
-
compile_print_assign_udg()
- Prints an assignement statement
-
compile_print_assign()
- Prints an assignement statement
-
compile_set_dag_info_udg()
-
-
compile_set_dag_info()
-
-
compile_symbtype_obfuscated_print()
- Prints the obfuscation of the given type
-
compile_unpack_dag_info_udg()
-
-
compile_unpack_dag_info()
-
-
compile_write_bool_fsm()
- Prints the boolean FSM of an SMV model.
-
compile_write_bool_specs()
- Prints the boolean specifications of an SMV model.
-
compile_write_bool_spec()
- Private service to print a boolean specification
-
compile_write_constants()
- Writes the set of non-numeric constants as CONSTANTS
statement
-
compile_write_flat_asgn()
- Writes flattened ASSIGN declarations in SMV format on a
file.
-
compile_write_flat_define_aux()
- Writes a DEFINE declarations in SMV format on a file.
-
compile_write_flat_define()
- Writes DEFINE declarations in SMV format on a file.
-
compile_write_flat_fsm()
- Prints the flatten version of FSM of an SMV model.
-
compile_write_flat_matrix_define_udg()
- Writes MDEFINE declarations in SMV format on a
file.
-
compile_write_flat_specs()
- Prints the flatten specifications of an SMV model.
-
compile_write_flat_spec()
- Prints the given flatten specifications.
-
compile_write_flatten_bfexpr()
- Writes flattened expression in SMV format on a file.
-
compile_write_flatten_bool_vars()
- Writes boolean VAR, FROZENVAR and IVAR declarations in
SMV format on a file. Non boolean vars are dumped as defines for the sake of
readability of conterexamples.
-
compile_write_flatten_expr_pair()
- Writes flattened expression pairs in SMV format on a
file.
-
compile_write_flatten_expr_split()
- Writes flattened expression in SMV format on a file.
-
compile_write_flatten_expr()
- Writes flattened expression in SMV format on a file.
-
compile_write_flatten_psl()
- Writes PSL properties as they are.
-
compile_write_flatten_spec_split()
- Writes flattened spec in SMV format on a file.
-
compile_write_flatten_spec()
- Writes flattened spec in SMV format on a file.
-
compile_write_flatten_vars_aux()
- Print the variable declaration.
-
compile_write_flatten_vars()
- Writes VAR, FROZENVAR, and IVAR declarations in
SMV format on a file.
-
compile_write_get_restricted_vars()
- Processes the intersection between the given set
and the given list
-
compile_write_obfuscated_constants()
- Writes the set of non-numeric constants as CONSTANTS
statement
-
compile_write_obfuscated_dag_defines()
-
-
compile_write_obfuscated_flat_asgn()
- Writes flattened ASSIGN declarations in SMV format on a
file.
-
compile_write_obfuscated_flat_define_aux()
- Writes a DEFINE declarations in SMV format on a file.
-
compile_write_obfuscated_flat_define()
- Writes DEFINE declarations in SMV format on a file.
-
compile_write_obfuscated_flat_fsm()
- Prints the obfuscated flatten version of FSM of an
SMV model.
-
compile_write_obfuscated_flat_specs()
- Prints the obfuscated flatten specifications of an
SMV model.
-
compile_write_obfuscated_flat_spec()
- Prints the given flatten specifications.
-
compile_write_obfuscated_flatten_expr_pair()
- Writes flattened expression pairs in SMV format on a
file.
-
compile_write_obfuscated_flatten_expr_split()
- Writes flattened expression in SMV format on a file.
-
compile_write_obfuscated_flatten_expr()
- Writes flattened expression in SMV format on a file.
-
compile_write_obfuscated_flatten_spec_split()
- Writes flattened spec in SMV format on a file.
-
compile_write_obfuscated_flatten_spec()
- Writes flattened spec in SMV format on a file.
-
compile_write_obfuscated_flatten_vars_aux()
- Print the variable declaration after obfuscation
-
compile_write_obfuscated_flatten_vars()
- Writes VAR, FROZENVAR, and IVAR declarations in
SMV format on a file.
-
compile_write_restricted_flat_fsm()
- Prints the restricted flatten version of FSM of
an SMV model.
-
compile_write_udg_bool_fsm()
- Prints the boolean FSM of an SMV model.
-
compile_write_udg_bool_specs()
- Prints the boolean specifications of an SMV model.
-
compile_write_udg_bool_spec()
- Private service to print a boolean specification
-
compile_write_udg_constants()
- Writes the set of non-numeric constants as CONSTANTS
statement
-
compile_write_udg_flat_asgn()
- Writes flattened ASSIGN declarations in SMV format on a
file.
-
compile_write_udg_flat_define()
- Writes DEFINE declarations in SMV format on a
file.
-
compile_write_udg_flat_fsm()
- Prints the flatten version of FSM of an SMV model.
-
compile_write_udg_flat_specs()
- Prints the flatten specifications of an SMV model.
-
compile_write_udg_flatten_bfexpr()
- Writes flattened expression in SMV format on a file.
-
compile_write_udg_flatten_bool_vars()
- Writes boolean VAR, FROZENVAR and IVAR declarations in
SMV format on a file. Non boolean vars are dumped as defines for the sake of
readability of conterexamples.
-
compile_write_udg_flatten_expr_pair()
- Writes flattened expression pairs in SMV format on a
file.
-
compile_write_udg_flatten_expr_split()
- Writes flattened expression in SMV format on a file.
-
compile_write_udg_flatten_expr()
- Writes flattened expression in SMV format on a file.
-
compile_write_udg_flatten_matrix_define()
- Writes DEFINE declarations in SMV format on a
file.
-
compile_write_udg_flatten_psl()
- Writes PSL properties as they are.
-
compile_write_udg_flatten_spec_split()
- Writes flattened spec in SMV format on a file.
-
compile_write_udg_flatten_spec()
- Writes flattened spec in SMV format on a file.
-
compile_write_udg_flatten_vars()
- Writes VAR, FROZENVAR, and IVAR declarations in
SMV format on a file.
-
compile_write_udg_print_1_ary()
- Printer in udg format for a node with a child
-
compile_write_udg_print_2_arya()
- Printer in udg format for a node with children arity equal to 2
-
compile_write_udg_print_2_ary()
- Printer in udg format for a node with children arity equal to 2
-
compile_write_udg_print_3_aryc_color()
- Printer in udg format for a node with children arity equal to 3
with different colors
-
compile_write_udg_print_3_aryc()
- Printer in udg format for a node with children arity equal to 3
-
compile_write_udg_print_node()
- Menthod that prints the given node in udg format
Last updated on 2010/05/19 22h:26