CommandBuildBooleanModel()
Compiles the flattened hierarchy into boolean SEXP
CommandBuildFlatModel()
Compiles the flattened hierarchy into SEXP
CommandBuildModel()
Compiles the flattened hierarchy into BDD
CommandCPPrintClusterInfo()
Prints out information about the clustering. ** DEPRECATED in 2.4 **
CommandEncodeVariables()
Builds the BDD variables necessary to compile the model into BDD.
CommandFlattenHierarchy()
Flattens the hierarchy of modules
CommandGetInternalStatus()
Implements the get_internal_status command
CommandGoBmc()
Implements the go_bmc command
CommandGo()
Implements the go command
CommandIwls95PrintOption()
Prints the Iwls95 Options.
CommandPrintFsmStats()
Prints out information about the fsm and clustering.
CommandProcessModel()
Performs the batch steps and then returns control to the interactive shell.
CommandShowDependencies()
Show expression dependencies
CommandShowVars()
Shows model's symbolic variables and their values
CommandWriteCoiModel()
Writes a flat model of a given SMV file, restricted to the COI of the model properties
CommandWriteModelFlatBool()
Writes a flat and boolean model of a given SMV file
CommandWriteModelFlat()
Writes the currently loaded SMV model in the specified file, after having flattened it
CommandWriteOrder()
Writes variable order to file.
CompileFlatten_expand_range()
Returns a range going from a to b
CompileFlatten_hash_module()
Add the tableau module to the list of known modules
CompileFlatten_init_flattener()
Inits the flattener module
CompileFlatten_normalise_value_list()
Takes a list of values and returns the same list being normalised
CompileFlatten_quit_flattener()
Quits the flattener module
CompileFlatten_resolve_define_chains()
Takes an expression, and if it is a define or parameter resolves it to the actual expression.
CompileFlatten_resolve_name()
Takes an expression representing an identifier and recursively normalizes it.
CompileFlatten_resolve_number()
Resolves the given symbol to be a number
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()
ComputeCOIFixpoint()
Computes the COI of a given expression
ComputeCOI()
Computes the COI of a given set of variables, defined within the given symb_table
Flatten_GetDefinition()
Gets the flattened version of an atom.
Flatten_remove_symbol_info()
Resets the hashed information about the given symbol
Formula_GetConstants()
Calculates the set of constants occurring into the given formula
Formula_GetDependenciesByType()
Computes the dependencies of an SMV expression by type
Formula_GetDependencies()
Computes dependencies of a given SMV expression
Formulae_GetDependencies()
Compute the dependencies of two set of formulae
UsageWriteCoiModel()
Prints the usage for the write_coi_command
__create_define_name()
Creates a meaningful name for defines needed for dag printing
_coi_get_var_coi0()
Given a variable it returns the cone at depth 0.
check_assign_both()
Given a variable, it checks if there are multiple assignments to it.
check_assign()
Checks for multiple or circular assignments.
check_circular_assign()
Performs circular assignment checking
check_circ()
Checks for circular definitions.
cmp_struct_init()
Initializes the cmp structure
cmp_struct_quit()
Free the cmp structure
coiInit()
Pre-compute the COI of the variables
compileCheckAssignForInputVars()
Checks flattened assign statement for input variables
compileCheckForInputVars()
Checks expressions for illegal occurrences of input vars
compileCheckInitForInputVars()
Checks flattened init statement for input variables
compileCheckInvarForInputVars()
Checks flattened invar statement for input variables
compileCheckNoNextInputs()
Checks expression for input variables in next statements
compileCheckTransForInputVars()
Checks flattened trans statement for input variables
compileFlattenProcessRecur()
Recursive definition of compileFlattenProcess
compileFlattenProcess()
Flatten a hierarchy of SMV processes.
compileFlattenSexpRecur()
Recursive function for flattenig a sexp.
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
computeCoiVar()
Computes the complete cone for a given variable.
construct_matrix_multiplexer()
Create matrix multiplexer in order to get rid of dynamic indexes.
create_process_symbolic_variables()
Creates the internal process selector variable, within the given layer
error_bit_selection_assignment_not_supported()
Error message for unsupported feature
expr2bexpr_get_shift_def_value()
Private service for shifting operations
expr2bexpr_ite()
Creates an encoding for CASE node. If CASE evaluates to a word, a WORD encoding is created.
expr2bexpr_recur_binary()
This function booleanize a binary expression in a standard way.
expr2bexpr_recur_unary()
This function booleanize an unary expression in a standard way: at first process the argument. Then for words apply a corresponding unary word function, for all other type just create exp of the same kind with find_node.
expr2bexpr_recur()
Converts a generic expression into a boolean expression.
expr2bexpr_rotate()
High-level function for rotating words
expr2bexpr_shift_left()
Creates the encoding of the left-shifting circuit for words
expr2bexpr_shift_right()
Creates the encoding of the unsigned right-shifting circuit for words
expr2bexpr_shift()
High-level function for shifting operations
expr2bexpr_word_ite_aux()
Service of expr2bexpr_word_ite, that creates the word encoding
flatten_declare_constants_within_list()
Traverses the list of values, and declare all constants (leaves) it finds
formulaGetDefinitionDependencies()
Compute the dependencies of an atom
formulaGetDependenciesRecur()
Recursive call to Formula_GetDependenciesByType
get_bits()
Computes the total bit number of symbols in the given list
get_hrc_root_node()
Get the HRC root node from a child
init_check_program()
Initializes the data structure to perform semantic checks.
insert_assoc_w()
Virtual menthod that prints the given node (core nodes are handled here)
instantiate_matrix_define()
Instantiates the elements of a matrix define
is_array_define_element()
Returns true iff this name is sub-element of an array define.
is_array_var_element()
Returns true iff this name is sub-element of a variable array.
is_matrix_define_cell_udg()
Print to the given file the matrix define represerntation
make_params_hrc()
Builds the parameters of a module from the list of formal and actual parameters of the module itself.
make_params()
Builds the parameters of a module from the list of formal parameters of the module itself.
push_matrix_index_down()
Pushes the index-access operator down to if-then-else expressions leaves.
put_in_context()
Put a variable in the current "context"
resolve_range()
This function takes a TWODOTS node, and tries to resolve the bounds to integer numbers which are returned.
scalar_atom2bexpr()
Converts an atomic expression into the corresponding (boolean) expression.
sym_intern()
Builds an internal representation for a given string.
up_log2()
Computes the log2 of the given argument rounding the result to the closest upper integer
()
Body of define in evaluation
()
Cleans and frees the hash
()
Clears and frees (with entries) given hash
()
Indicates that no dependency has been yet computed.
()
Indicates that the COI computation should be verbose.
()
Indicates that the dependency computation is ongoing.
()
Indicates that the dependency is empty
()
Private macros for the sake of readability of the function Compile_pop_global
()
Short way of calling printer_base_throw_print_node
()
Short way of print a node
()
Short way of print a node with sharing
()
Short way of print a node without sharing
()
The name of the standard layer dedicated to model symbols

Last updated on 2010/05/19 22h:26