-
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
-
CommandWriteModelFlatUdg()
- Writes the currently loaded SMV model in the
specified uDraw file, after having flattened it
-
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_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()
-
-
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_expr_booleanizable()
- Check if an expr is of a finite range type
-
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_array_define_udg()
- Prints a array define node to out file.
-
Compile_print_array_define()
- Prints an array 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_get_var_type()
- Creates an internal representaion of the symbol type
-
compile_cmd_print_type()
- Prints the given type to the given stream
-
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_build_word_toint_ith_bit_case()
- Aux function for the
compile_flatten_rewrite_word_toint_cast, which
is used for toint cast operator rewriting
-
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_rewrite_word_toint_cast()
- Rewrites the toint operator for word expressions
conversion
-
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_is_booleanizable_aux()
- true if expression is booleanizable
-
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_array_define_udg()
- Writes ARRAY DEFINE declarations in SMV format on a
file.
-
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_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_array_define()
- Writes DEFINE declarations in SMV format on a
file.
-
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_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_array_multiplexer()
- Create array 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_array_define()
- Instantiates the elements of an array define
-
is_array_define_cell_udg()
- Print to the given file the array define represerntation
-
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.
-
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_array_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 2011/04/06 21h:13