int CommandBuildBooleanModel( int argc, char ** argv )
compileCmd.c
int CommandBuildFlatModel( int argc, char ** argv )
compileCmd.c
int CommandBuildModel( int argc, char ** argv )
compileCmd.c
int CommandCPPrintClusterInfo( int argc, char ** argv )
compileCmd.c
int CommandEncodeVariables( int argc, char ** argv )
compileCmd.c
int CommandFlattenHierarchy( int argc, char ** argv )
compileCmd.c
int CommandGetInternalStatus( int argc, char ** argv )
compileCmd.c
int CommandGoBmc( int argc, char ** argv )
compileCmd.c
int CommandGo( int argc, char ** argv )
compileCmd.c
int CommandIwls95PrintOption( int argc, char ** argv )
compileCmd.c
int CommandPrintFsmStats( int argc, char ** argv )
compileCmd.c
int CommandProcessModel( int argc, char ** argv )
compileCmd.c
int CommandShowDependencies( int argc, char ** argv )
compileCmd.c
int CommandShowVars( int argc, char ** argv )
compileCmd.c
int CommandWriteCoiModel( int argc, char ** argv )
compileCmd.c
int CommandWriteModelFlatBool( int argc, char ** argv )
compileCmd.c
int CommandWriteModelFlat( int argc, char ** argv )
compileCmd.c
int CommandWriteOrder( int argc, char ** argv )
compileCmd.c
node_ptr CompileFlatten_expand_range( int a, int b )
compileFlatten.c
void CompileFlatten_hash_module( node_ptr parsed_module )
compileFlatten.c
void CompileFlatten_init_flattener( )
compileFlatten.c
node_ptr CompileFlatten_normalise_value_list( node_ptr old_values )
compileFlatten.c
void CompileFlatten_quit_flattener( )
compileFlatten.c
node_ptr CompileFlatten_resolve_define_chains( const SymbTable_ptr symb_table, node_ptr expr, node_ptr context )
compileFlatten.c
node_ptr CompileFlatten_resolve_name( const SymbTable_ptr symb_table, node_ptr name, node_ptr context )
compile_flatten_resolve_name_recur
compileFlatten.c
node_ptr CompileFlatten_resolve_number( SymbTable_ptr symb_table, node_ptr n, node_ptr context )
compileFlatten.c
void Compile_CheckAssigns( const SymbTable_ptr symb_table, node_ptr procs )
compileCheck.c
void
Compile_ConstructHierarchy(
SymbTable_ptr st,
SymbLayer_ptr layer,
node_ptr module_name, the ATOM
representing the name of the
module being instantiated
node_ptr instance_name, the name of the module instance to be instantiated
node_ptr actual, the actual module arguments
FlatHierarchy_ptr result,
HrcNode_ptr hrc_result,
hash_ptr instances
)
compileFlatten.c
boolean Compile_DeclareVariable( SymbTable_ptr st, SymbLayer_ptr layer, node_ptr name, SymbType_ptr type, node_ptr context, Instantiation_Variables_Mode_Type mode )
compile_instantiate_var
compileFlatten.c
FlatHierarchy_ptr Compile_FlattenHierarchy( const SymbTable_ptr symb_table, SymbLayer_ptr layer, node_ptr module_name, node_ptr inst_name, node_ptr actual, boolean create_process_variables, enables creation of process variables boolean calc_vars_constr, triggers calc of vars constr, or delays it HrcNode_ptr hrc_result hrc node to be populated )
compileFlatten.c
node_ptr Compile_FlattenSexpExpandDefine( const SymbTable_ptr symb_table, node_ptr sexp, node_ptr context )
Flatten_GetDefinition
Compile_FlattenSexp
compileFlatten.c
node_ptr Compile_FlattenSexp( const SymbTable_ptr symb_table, node_ptr sexp, node_ptr context )
Flatten_GetDefinition
Compile_FlattenSexpExpandDefine
compileFlatten.c
SymbType_ptr Compile_InstantiateType( SymbTable_ptr st, SymbLayer_ptr layer, node_ptr name, node_ptr type, node_ptr context )
compileFlatten.c
void Compile_ProcessHierarchy( SymbTable_ptr symb_table, SymbLayer_ptr layer, FlatHierarchy_ptr hierarchy, node_ptr name, boolean create_process_variables, boolean calc_vars_constr )
compileFlatten.c
void Compile_WriteBoolFsm_udg( FILE* out, const SymbTable_ptr st, NodeList_ptr layers, const char* fsm_name, BoolSexpFsm_ptr bool_sexp_fsm )
compileWriteUdg.c
void Compile_WriteBoolFsm( FILE* out, const SymbTable_ptr st, NodeList_ptr layers, const char* fsm_name, BoolSexpFsm_ptr bool_sexp_fsm, boolean force_flattening )
compileWrite.c
void Compile_WriteBoolModel_udg( FILE* out, BddEnc_ptr enc, NodeList_ptr layers, const char* fsm_name, BoolSexpFsm_ptr bool_sexp_fsm )
compileWriteUdg.c
void Compile_WriteBoolModel( FILE* out, BddEnc_ptr enc, NodeList_ptr layers, const char* fsm_name, BoolSexpFsm_ptr bool_sexp_fsm, boolean force_flattening )
compileWrite.c
void Compile_WriteBoolSpecs_udg( FILE* out, BddEnc_ptr enc, FlatHierarchy_ptr hierarchy )
compileWriteUdg.c
void Compile_WriteBoolSpecs( FILE* out, BddEnc_ptr enc, FlatHierarchy_ptr hierarchy )
compileWrite.c
void Compile_WriteFlattenFsm_udg( FILE* out, const SymbTable_ptr st, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy )
compileWriteUdg.c
void Compile_WriteFlattenFsm( FILE* out, const SymbTable_ptr st, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy, boolean force_flattening )
compileWrite.c
void Compile_WriteFlattenModel_udg( FILE* out, const SymbTable_ptr st, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy )
compileWriteUdg.c
void Compile_WriteFlattenModel( FILE* out, const SymbTable_ptr st, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy, boolean force_flattening )
compileWrite.c
void Compile_WriteFlattenSpecs_udg( FILE* out, const SymbTable_ptr st, FlatHierarchy_ptr hierarchy )
compileWriteUdg.c
void Compile_WriteFlattenSpecs( FILE* out, const SymbTable_ptr st, FlatHierarchy_ptr hierarchy, boolean force_flattening )
compileWrite.c
void Compile_WriteObfuscatedFlattenModel( FILE* out, const SymbTable_ptr st, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy, boolean print_map, boolean force_flattening )
compileWrite.c
void Compile_WriteRestrictedFlattenModel( FILE* out, const SymbTable_ptr st, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy, boolean force_flattening )
compileWrite.c
int Compile_check_if_bool_model_was_built( FILE* err, boolean forced )
compileUtil.c
int Compile_check_if_encoding_was_built( FILE* err )
compileUtil.c
int Compile_check_if_flat_model_was_built( FILE* err, boolean forced )
compileUtil.c
int Compile_check_if_flattening_was_built( FILE* err )
compileUtil.c
int Compile_check_if_model_was_built( FILE* err, boolean forced )
compileUtil.c
void Compile_check_input_next( const SymbTable_ptr st, node_ptr expr, node_ptr context )
compileCheck.c
void Compile_check_next( const SymbTable_ptr st, node_ptr expr, node_ptr context, boolean is_one_next_allowed )
compileCheck.c
void Compile_cleanup_booleanizer_cache_about( SymbTable_ptr st, NodeList_ptr symbs )
compileBEval.c
node_ptr Compile_convert_to_dag_udg( SymbTable_ptr symb_table, node_ptr expr, hash_ptr dag_hash, hash_ptr defines )
compileWriteUdg.c
node_ptr Compile_convert_to_dag( SymbTable_ptr symb_table, node_ptr expr, hash_ptr dag_hash, hash_ptr defines )
compileWrite.c
void Compile_destroy_dag_info_udg( hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
void Compile_destroy_dag_info( hash_ptr dag_info, hash_ptr defines )
compileWrite.c
Expr_ptr Compile_detexpr2bexpr_list( BddEnc_ptr enc, Expr_ptr expr )
Compile_detexpr2bexpr
Compile_expr2bexpr
expr2bexpr_recur
compileBEval.c
Expr_ptr Compile_detexpr2bexpr( BddEnc_ptr enc, Expr_ptr expr )
Compile_expr2bexpr
expr2bexpr_recur
Compile_detexpr2bexpr_list
compileBEval.c
Expr_ptr Compile_expr2bexpr( BddEnc_ptr enc, SymbLayer_ptr det_layer, Expr_ptr expr )
Compile_detexpr2bexpr
expr2bexpr_recur
compileBEval.c
FsmBuilder_ptr Compile_get_global_fsm_builder( )
compileStruct.c
PredicateNormaliser_ptr Compile_get_global_predicate_normaliser( )
compileStruct.c
hash_ptr Compile_get_obfuscation_map( const SymbTable_ptr symb_table )
compileWrite.c
void Compile_init_cmd( )
compileCmd.c
void Compile_init( )
compileCmd.c
boolean Compile_is_symbol_constant( node_ptr node )
compileWrite.c
node_ptr Compile_make_dag_info_udg( node_ptr expr, hash_ptr hash )
compileWriteUdg.c
node_ptr Compile_make_dag_info( node_ptr expr, hash_ptr hash )
compileWrite.c
Set_t Compile_make_sorted_vars_list_from_order( const SymbTable_ptr st, const NodeList_ptr vars, const NodeList_ptr vars_order )
compileUtil.c
node_ptr Compile_obfuscate_expression( const SymbTable_ptr symb_table, const node_ptr expr, const hash_ptr obfuscation_map )
compileWrite.c
node_ptr Compile_pop_distrib_ops( node_ptr prop )
compileUtil.c
void Compile_print_matrix_define_udg( FILE* out, const node_ptr n )
compileWriteUdg.c
void Compile_print_matrix_define( FILE* out, const node_ptr n )
compileWrite.c
void Compile_quit( )
compileCmd.c
void Compile_write_dag_defines_udg( FILE* out, hash_ptr defines )
compileWriteUdg.c
void Compile_write_dag_defines( FILE* out, hash_ptr defines )
compileWrite.c
Set_t ComputeCOIFixpoint( const SymbTable_ptr symb_table, const FlatHierarchy_ptr hierarchy, const Expr_ptr expression, const int steps, boolean* reached_fixpoint )
compileCone.c
Set_t ComputeCOI( const SymbTable_ptr symb_table, Set_t base )
compileCone.c
node_ptr Flatten_GetDefinition( const SymbTable_ptr symb_table, node_ptr atom )
compileFlatten.c
void Flatten_remove_symbol_info( node_ptr name )
compileFlatten.c
Set_t Formula_GetConstants( const SymbTable_ptr symb_table, node_ptr formula, node_ptr context )
compileCone.c
Set_t Formula_GetDependenciesByType( const SymbTable_ptr symb_table, node_ptr formula, node_ptr context, SymbFilterType filter, boolean preserve_time )
formulaGetDependenciesByTypeAux
formulaGetDefinitionDependencies
compileCone.c
Set_t Formula_GetDependencies( const SymbTable_ptr symb_table, node_ptr formula, node_ptr context )
formulaGetDefinitionDependencies
compileCone.c
Set_t Formulae_GetDependencies( const SymbTable_ptr symb_table, node_ptr formula, node_ptr justice, node_ptr compassion )
compileCone.c
static int UsageWriteCoiModel( )
compileCmd.c
node_ptr __create_define_name( SymbTable_ptr st, const char * prefix, node_ptr body )
compileWrite.c
static Set_t _coi_get_var_coi0( SymbTable_ptr st, FlatHierarchy_ptr hierarchy, node_ptr var, boolean * nonassign, boolean use_cache )
optional
compileCone.c
static void check_assign_both( node_ptr v, int node_type, int lineno )
compileCheck.c
static void check_assign( const SymbTable_ptr symb_table, node_ptr n, node_ptr context, int mode )
compileCheck.c
static void check_circular_assign( const SymbTable_ptr symb_table, node_ptr n, node_ptr context, boolean is_next, boolean is_lhs, boolean lhs_is_next )
compileCheck.c
static void check_circ( const SymbTable_ptr symb_table, node_ptr n, node_ptr context, boolean is_next, boolean lhs_is_next )
next(x) := alpha(next(x))
next(x) := next(alpha(x))
x := alpha(x)
alpha(x)
(alpha(next(x))
) is a
formula in which the variable x
(next(x)
)
occurs. Notice that next(alpha(x))
can be rewritten in
term of next(x)
, since the next operator distributes
along all kind of operators.
compileCheck.c
cmp_struct_ptr cmp_struct_init( )
compileStruct.c
void cmp_struct_quit( cmp_struct_ptr cmp )
compileStruct.c
static void coiInit( const SymbTable_ptr symb_table, FlatHierarchy_ptr hierarchy )
ComputeCOI
compileCone.c
static void compileCheckAssignForInputVars( SymbTable_ptr symb_table, node_ptr assign, FlatHierarchy_ptr hierarchy )
compileCheck.c
void compileCheckForInputVars( const SymbTable_ptr symb_table, node_ptr trans_expr, node_ptr init_expr, node_ptr invar_expr, node_ptr assign_expr, FlatHierarchy_ptr hierarchy )
compileCheck.c
static void compileCheckInitForInputVars( SymbTable_ptr symb_table, node_ptr init )
compileCheck.c
static void compileCheckInvarForInputVars( SymbTable_ptr symb_table, node_ptr invar )
compileCheck.c
static void compileCheckNoNextInputs( SymbTable_ptr symb_table, node_ptr expr, node_ptr ctx )
compileCheck.c
static void compileCheckTransForInputVars( SymbTable_ptr symb_table, node_ptr trans )
compileCheck.c
static void compileFlattenProcessRecur( const SymbTable_ptr symb_table, node_ptr assign, node_ptr context, node_ptr running, FlatHierarchy_ptr flatHierarchy )
compileFlatten.c
static node_ptr compileFlattenProcess( const SymbTable_ptr symb_table, node_ptr proc_assign_list, FlatHierarchy_ptr flattenHierarchy )
compileFlatten.c
static node_ptr compileFlattenSexpRecur( const SymbTable_ptr symb_table, node_ptr sexp, node_ptr context )
Compile_FlattenSexp
Compile_FlattenSexpExpandDefine
compileFlatten.c
void compile_add_vars_to_hierarhcy( node_ptr name, SymbType_ptr type, FlatHierarchy_ptr fh )
compileFlatten.c
void compile_build_model( boolean force_build )
compileCmd.c
void compile_check_print_io_atom_stack_assign( FILE * fd )
compileCheck.c
Expr_ptr compile_cmd_remove_assignments( Expr_ptr expr )
compileCmd.c
void compile_cmd_write_coi_prop_fsm( FlatHierarchy_ptr fh, Set_t cone, Set_t props, FILE* output_file )
compileCmd.c
void compile_cmd_write_coi_prop( Set_t cone, Set_t props, FILE* output_file )
compileCmd.c
void compile_cmd_write_global_coi_fsm( FlatHierarchy_ptr hierarchy, Prop_Type prop_type, FILE* output_file )
compileCmd.c
int compile_cmd_write_properties_coi( FlatHierarchy_ptr hierarchy, Prop_Type prop_type, boolean only_dump_coi, const char* file_name )
compileCmd.c
node_ptr compile_concat_contexts( node_ptr ctx1, node_ptr ctx2 )
compileFlatten.c
node_ptr compile_convert_to_dag_aux_udg( SymbTable_ptr symb_table, node_ptr expr, hash_ptr hash, unsigned int num_thres, unsigned int dep_thres, hash_ptr defines, const char* defines_prefix )
compileWriteUdg.c
node_ptr compile_convert_to_dag_aux( SymbTable_ptr symb_table, node_ptr expr, hash_ptr hash, unsigned int num_thres, unsigned int dep_thres, hash_ptr defines, const char* defines_prefix )
compileWrite.c
void compile_create_boolean_model( )
compileCmd.c
hash_ptr compile_create_dag_info_from_hierarchy_udg( SymbTable_ptr st, FlatHierarchy_ptr hierarchy, SymbLayer_ptr det_layer, BddEnc_ptr enc )
compileWriteUdg.c
hash_ptr compile_create_dag_info_from_hierarchy( SymbTable_ptr st, FlatHierarchy_ptr hierarchy, SymbLayer_ptr det_layer, BddEnc_ptr enc, boolean force_flattening, hash_ptr cdh )
compileWrite.c
void compile_create_flat_model( )
compileCmd.c
int compile_encode_variables( )
compileCmd.c
node_ptr compile_flatten_eval_number( SymbTable_ptr st, node_ptr n, node_ptr context )
compileFlatten.c
int compile_flatten_get_int( node_ptr value )
compileFlatten.c
node_ptr compile_flatten_normalise_value_list( node_ptr old_value_list )
compileFlatten.c
node_ptr compile_flatten_resolve_name_recur( const SymbTable_ptr symb_table, node_ptr n, node_ptr context )
CompileFlatten_resolve_name
compileFlatten.c
int compile_flatten_smv( boolean calc_vars_constrains )
compileCmd.c
assoc_retval compile_free_define_udg( char * key, char * data, char * arg )
compileWriteUdg.c
assoc_retval compile_free_define( char * key, char * data, char * arg )
compileWrite.c
assoc_retval compile_free_node_udg( char * key, char * data, char * arg )
compileWriteUdg.c
assoc_retval compile_free_node( char * key, char * data, char * arg )
compileWrite.c
node_ptr compile_get_rid_of_define_chain( SymbTable_ptr st, node_ptr expr, hash_ptr cdh )
compileWrite.c
void compile_insert_assign_hrc( HrcNode_ptr hrc_result, node_ptr cur_decl )
compileFlatten.c
void compile_instantiate_by_name( SymbTable_ptr st, SymbLayer_ptr layer, node_ptr module_name, node_ptr instance_name, node_ptr actual, node_ptr * assign, FlatHierarchy_ptr result, HrcNode_ptr hrc_result, hash_ptr instances )
compileFlatten.c
void compile_instantiate_vars( SymbTable_ptr st, SymbLayer_ptr layer, node_ptr var_list, node_ptr mod_name, node_ptr * assign, FlatHierarchy_ptr result, HrcNode_ptr hrc_result, hash_ptr instances )
compile_instantiate_var
compileFlatten.c
void compile_instantiate_var( SymbTable_ptr st, SymbLayer_ptr layer, node_ptr name, node_ptr type, node_ptr context, node_ptr * assign, FlatHierarchy_ptr result, HrcNode_ptr hrc_result, hash_ptr instances )
symbol_hash
saying that the variable values are {0,1}
.M..N
, then
we add an entry in the symbol_hash
saying that the
variable values are {M, M+1, ..., N-1, N}
. If
M
is less or equal to N
, than an error occurs.{a1, a2, ..., aN}
, then we add an entry in the
symbol_hash
saying that the variable values are
{a1, ..., aN}
. VAR
x : array 1..4 of boolean;
". We call this function
for 4 times, asking at each call i
(i
from 1
to 4) to declare the boolean variable x[i]
.instantiate_by_name with the name of the
instantiated module as root name (to extract its definition)
and as variable name as the name of the module (to perform
flattening).
compile_instantiate_vars
compileFlatten.c
void compile_instantiate( SymbTable_ptr st, SymbLayer_ptr layer, node_ptr mod_def, node_ptr mod_name, node_ptr actual, node_ptr * assign, FlatHierarchy_ptr result, HrcNode_ptr hrc_result, hash_ptr instances )
compile_instantiate_var
compile_instantiate_vars
compileFlatten.c
node_ptr compile_make_dag_info_aux_udg( node_ptr expr, hash_ptr hash )
compileWriteUdg.c
node_ptr compile_make_dag_info_aux( node_ptr expr, hash_ptr hash )
compileWrite.c
node_ptr compile_pack_dag_info_udg( unsigned int count, unsigned int depth )
compileWriteUdg.c
node_ptr compile_pack_dag_info( unsigned int count, unsigned int depth, boolean admissible )
compileWrite.c
void compile_print_assign_udg( SymbTable_ptr st, FILE * out, node_ptr lhs, node_ptr rhs, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
void compile_print_assign( SymbTable_ptr st, FILE * out, node_ptr lhs, node_ptr rhs, hash_ptr dag_info, hash_ptr defines )
compileWrite.c
void compile_set_dag_info_udg( node_ptr info, unsigned int count, unsigned int depth )
compileWriteUdg.c
void compile_set_dag_info( node_ptr info, unsigned int count, unsigned int depth, boolean admissible )
compileWrite.c
void compile_symbtype_obfuscated_print( SymbType_ptr type, FILE* out, const SymbTable_ptr symb_table, hash_ptr obfuscation_map )
compileWrite.c
void compile_unpack_dag_info_udg( node_ptr info, unsigned int* count, unsigned int* depth )
compileWriteUdg.c
void compile_unpack_dag_info( node_ptr info, unsigned int* count, unsigned int* depth, boolean* admissible )
compileWrite.c
void compile_write_bool_fsm( FILE* out, const SymbTable_ptr symb_table, NodeList_ptr layers, const char* fsm_name, BoolSexpFsm_ptr bool_sexp_fsm, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
void compile_write_bool_specs( FILE* out, BddEnc_ptr enc, SymbLayer_ptr det_layer, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines, hash_ptr cdh )
compileWrite.c
void compile_write_bool_spec( FILE* out, BddEnc_ptr enc, node_ptr spec, const char* msg, SymbLayer_ptr det_layer, hash_ptr dag_info, hash_ptr defines, hash_ptr cdh )
compileWrite.c
int compile_write_constants( const SymbTable_ptr symb_table, FILE* out )
compileWrite.c
int compile_write_flat_asgn( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr vars, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines, hash_ptr cdh )
compileWrite.c
int compile_write_flat_define_aux( const SymbTable_ptr symb_table, FILE* out, node_ptr name, hash_ptr dag_info, hash_ptr defines, hash_ptr printed_arrays )
compileWrite.c
int compile_write_flat_define( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr names, hash_ptr dag_info, hash_ptr defines )
compileWrite.c
void compile_write_flat_fsm( FILE* out, const SymbTable_ptr symb_table, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_flat_matrix_define_udg( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr names, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
void compile_write_flat_specs( FILE* out, const SymbTable_ptr st, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
void compile_write_flat_spec( FILE* out, const SymbTable_ptr symb_table, node_ptr spec, const char* msg, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_flatten_bfexpr( BddEnc_ptr enc, const SymbTable_ptr symb_table, SymbLayer_ptr det_layer, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, hash_ptr cdh )
compileWrite.c
int compile_write_flatten_bool_vars( const SymbTable_ptr symb_table, const BoolEnc_ptr bool_enc, FILE* out, NodeList_ptr vars )
compileWrite.c
int compile_write_flatten_expr_pair( const SymbTable_ptr symb_table, FILE* out, node_ptr l, const char* s, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_flatten_expr_split( const SymbTable_ptr symb_table, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_flatten_expr( const SymbTable_ptr symb_table, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_flatten_psl( const SymbTable_ptr symb_table, FILE* out, node_ptr n, hash_ptr dag_info, hash_ptr defines, hash_ptr cdh )
compileWrite.c
int compile_write_flatten_spec_split( const SymbTable_ptr symb_table, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_flatten_spec( const SymbTable_ptr symb_table, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_flatten_vars_aux( const SymbTable_ptr symb_table, const node_ptr name, FILE* out, hash_ptr printed )
compileWrite.c
int compile_write_flatten_vars( const SymbTable_ptr symb_table, FILE* out, NodeList_ptr vars )
compileWrite.c
NodeList_ptr compile_write_get_restricted_vars( Set_t keep_vars, NodeList_ptr all_vars )
compileWrite.c
int compile_write_obfuscated_constants( const SymbTable_ptr symb_table, FILE* out, hash_ptr obfuscation_map )
compileWrite.c
void compile_write_obfuscated_dag_defines( FILE* out, const SymbTable_ptr st, hash_ptr defines, hash_ptr obfuscation_map )
compileWrite.c
int compile_write_obfuscated_flat_asgn( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr vars, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, hash_ptr cdh )
compileWrite.c
int compile_write_obfuscated_flat_define_aux( const SymbTable_ptr symb_table, FILE* out, node_ptr name, hash_ptr dag_info, hash_ptr defines, hash_ptr printed_arrays, hash_ptr obfuscation_map )
compile_write_flat_define_aux
compileWrite.c
int compile_write_obfuscated_flat_define( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr names, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map )
compileWrite.c
void compile_write_obfuscated_flat_fsm( FILE* out, const SymbTable_ptr symb_table, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, boolean force_flattening, hash_ptr cdh )
compile_write_flat_fsm
compileWrite.c
void compile_write_obfuscated_flat_specs( FILE* out, const SymbTable_ptr st, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, boolean force_flattening, hash_ptr cdh )
compile_write_flat_specs
compileWrite.c
void compile_write_obfuscated_flat_spec( FILE* out, const SymbTable_ptr symb_table, node_ptr spec, const char* msg, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_obfuscated_flatten_expr_pair( const SymbTable_ptr symb_table, FILE* out, node_ptr l, const char* s, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_obfuscated_flatten_expr_split( const SymbTable_ptr symb_table, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_obfuscated_flatten_expr( const SymbTable_ptr symb_table, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_obfuscated_flatten_spec_split( const SymbTable_ptr symb_table, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, boolean force_flattening, hash_ptr cdh )
compileWrite.c
int compile_write_obfuscated_flatten_spec( const SymbTable_ptr symb_table, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines, hash_ptr obfuscation_map, boolean force_flattening, hash_ptr cdh )
compileWrite.c
boolean compile_write_obfuscated_flatten_vars_aux( const SymbTable_ptr symb_table, const node_ptr name, FILE* out, hash_ptr printed, hash_ptr obfuscation_map )
compile_write_flatten_vars_aux
compileWrite.c
int compile_write_obfuscated_flatten_vars( const SymbTable_ptr symb_table, FILE* out, NodeList_ptr vars, hash_ptr obfuscation_map )
compileWrite.c
void compile_write_restricted_flat_fsm( FILE* out, const SymbTable_ptr symb_table, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines, boolean force_flattening, hash_ptr cdh )
compileWrite.c
void compile_write_udg_bool_fsm( FILE* out, const SymbTable_ptr symb_table, NodeList_ptr layers, const char* fsm_name, BoolSexpFsm_ptr bool_sexp_fsm, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
void compile_write_udg_bool_specs( FILE* out, BddEnc_ptr enc, SymbLayer_ptr det_layer, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
void compile_write_udg_bool_spec( FILE* out, BddEnc_ptr enc, node_ptr spec, const char* msg, SymbLayer_ptr det_layer, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_constants( const SymbTable_ptr symb_table, FILE* out )
compileWriteUdg.c
int compile_write_udg_flat_asgn( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr vars, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_flat_define( const SymbTable_ptr symb_table, FILE* out, const NodeList_ptr names, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
void compile_write_udg_flat_fsm( FILE* out, const SymbTable_ptr symb_table, const array_t* layer_names, const char* fsm_name, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
void compile_write_udg_flat_specs( FILE* out, const SymbTable_ptr st, FlatHierarchy_ptr hierarchy, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_flatten_bfexpr( BddEnc_ptr enc, const SymbTable_ptr symb_table, SymbLayer_ptr det_layer, FILE* out, node_ptr n, const char* s, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_flatten_bool_vars( const SymbTable_ptr symb_table, const BoolEnc_ptr bool_enc, FILE* out, NodeList_ptr vars )
compileWriteUdg.c
int compile_write_udg_flatten_expr_pair( const SymbTable_ptr symb_table, FILE* out, node_ptr l, ModelSectionTag mst, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_flatten_expr_split( const SymbTable_ptr symb_table, FILE* out, node_ptr n, ModelSectionTag mst, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_flatten_expr( const SymbTable_ptr symb_table, FILE* out, node_ptr n, ModelSectionTag mst, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
node_ptr compile_write_udg_flatten_matrix_define( SymbTable_ptr st, node_ptr body, node_ptr context )
compileWriteUdg.c
int compile_write_udg_flatten_psl( const SymbTable_ptr symb_table, FILE* out, node_ptr n, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_flatten_spec_split( const SymbTable_ptr symb_table, FILE* out, node_ptr n, ModelSectionTag mst, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_flatten_spec( const SymbTable_ptr symb_table, FILE* out, node_ptr n, ModelSectionTag mst, hash_ptr dag_info, hash_ptr defines )
compileWriteUdg.c
int compile_write_udg_flatten_vars( const SymbTable_ptr symb_table, FILE* out, NodeList_ptr vars )
compileWriteUdg.c
inline int compile_write_udg_print_1_ary( FILE* buffer, node_ptr code, const char* str, boolean close, boolean shared, const char* color1 )
compileWriteUdg.c
inline int compile_write_udg_print_2_arya( FILE* buffer, node_ptr code, const char* str, boolean close, boolean shared )
compileWriteUdg.c
inline int compile_write_udg_print_2_ary( FILE* buffer, node_ptr code, const char* str, boolean close, boolean shared, const char* color1, const char* color2 )
compileWriteUdg.c
inline int compile_write_udg_print_3_aryc_color( FILE* buffer, node_ptr code, const char* str, node_ptr fst, node_ptr snd, node_ptr trd, boolean close, boolean shared, const char* color1, const char* color2, const char* color3 )
compileWriteUdg.c
inline int compile_write_udg_print_3_aryc( FILE* buffer, node_ptr code, const char* str, node_ptr fst, node_ptr snd, node_ptr trd, boolean close, boolean shared )
compileWriteUdg.c
int compile_write_udg_print_node( FILE* out, node_ptr n, boolean close, boolean shared, const char* style )
compileWriteUdg.c
static Set_t computeCoiVar( SymbTable_ptr st, FlatHierarchy_ptr fh, node_ptr var )
optional
compileCone.c
static node_ptr construct_matrix_multiplexer( node_ptr matrix, node_ptr index, boolean is_matrix_next, SymbTable_ptr symb_table )
compileFlatten.c
static void create_process_symbolic_variables( SymbTable_ptr symb_table, SymbLayer_ptr layer, node_ptr process_name_list )
compileFlatten.c
void error_bit_selection_assignment_not_supported( node_ptr name )
compileFlatten.c
static node_ptr expr2bexpr_get_shift_def_value( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr context, boolean in_next, node_ptr a, node_ptr b, int numWidth, node_ptr defaultBit )
compileBEval.c
static node_ptr expr2bexpr_ite( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
expr2bexpr_word_ite_aux
compileBEval.c
static node_ptr expr2bexpr_recur_binary( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
static node_ptr expr2bexpr_recur_unary( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
static node_ptr expr2bexpr_recur( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
Compile_expr2bexpr
detexpr2bexpr
compileBEval.c
static node_ptr expr2bexpr_rotate( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
static node_ptr expr2bexpr_shift_left( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr context, boolean in_next, node_ptr a, node_ptr b, node_ptr def_case, int numWidth )
compileBEval.c
static node_ptr expr2bexpr_shift_right( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr context, boolean in_next, node_ptr a, node_ptr b, node_ptr def_case, int numWidth )
compileBEval.c
static node_ptr expr2bexpr_shift( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
static node_ptr expr2bexpr_word_ite_aux( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
static void flatten_declare_constants_within_list( SymbTable_ptr symb_table, SymbLayer_ptr layer, node_ptr value_list )
compileFlatten.c
static Set_t formulaGetDefinitionDependencies( const SymbTable_ptr symb_table, node_ptr formula, SymbFilterType filter, boolean preserve_time, int time )
Formula_GetDependencies
compileCone.c
static Set_t formulaGetDependenciesRecur( const SymbTable_ptr symb_table, node_ptr formula, node_ptr context, SymbFilterType filter, boolean preserve_time, int time )
formulaGetDefinitionDependencies
Formula_GetDependenciesByType
compileCone.c
static int get_bits( const SymbTable_ptr st, const NodeList_ptr lst )
compileCmd.c
static HrcNode_ptr get_hrc_root_node( HrcNode_ptr node )
compileFlatten.c
static void init_check_program( node_ptr l )
compileCheck.c
static inline int insert_assoc_w( hash_ptr hash, node_ptr key, node_ptr value )
compileWriteUdg.c
static void instantiate_matrix_define( SymbTable_ptr st, SymbLayer_ptr layer, node_ptr name, node_ptr mod_name, node_ptr definition )
compileFlatten.c
static boolean is_array_define_element( const SymbTable_ptr symb_table, const node_ptr name )
compileWrite.c
static boolean is_array_var_element( const SymbTable_ptr symb_table, const node_ptr name )
compileWrite.c
static boolean is_matrix_define_cell_udg( const SymbTable_ptr st, const node_ptr name )
compileWriteUdg.c
static void make_params_hrc( node_ptr basename, node_ptr actual_list, node_ptr formal_list, HrcNode_ptr hrc_result )
compileFlatten.c
static void make_params( SymbLayer_ptr layer, node_ptr basename, node_ptr actual_list, node_ptr formal_list )
compileFlatten.c
static node_ptr push_matrix_index_down( node_ptr matrix, node_ptr index, boolean is_matrix_next, SymbTable_ptr st )
compileFlatten.c
static node_ptr put_in_context( node_ptr v )
param_context
.
param_context
compileFlatten.c
static void resolve_range( SymbTable_ptr st, node_ptr range, node_ptr context, int* low, int* high )
compileFlatten.c
static node_ptr scalar_atom2bexpr( BddEnc_ptr enc, SymbLayer_ptr det_layer, node_ptr expr, node_ptr context, boolean in_next )
compileBEval.c
node_ptr sym_intern( char * s )
VAR x : {a1, a2, a3}; y : {a3, a4, a5}; ASSIGN next(x) := case x = y : a2; !(x = y) : a1; 1 : a3; esac;i.e. to allow the equality test between x and y. This can be performed because we internally have a unique representation of the atom a3.
find_atom
compileUtil.c
static int up_log2( int a )
compileCmd.c
( )
Flatten_GetDefinition
compileFlatten.c
( )
compileFlatten.c
( )
compileCone.c
( )
compileCone.c
( )
compileCone.c
( )
compileCone.c
( )
compileCone.c
( )
compileUtil.c
( )
compileWriteUdg.c
( )
compileWriteUdg.c
( )
compileWriteUdg.c
( )
compileWriteUdg.c
( )
compile.h