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 15h:56