CommandAddProperty()
Adds a property to the list of properties
CommandCheckProperty()
Checks properties
CommandShowProperty()
Shows the currently stored properties
PropDb_add()
Inserts a property in the DB of properties
PropDb_create()
Initializes the DB of properties
PropDb_destroy()
Disposes the DB of properties
PropDb_fill()
Fills the DB of properties
PropDb_get_last()
Returns the last entered property in the DB
PropDb_get_prop_at_index()
Returns the property indexed by index
PropDb_get_prop_index_from_string()
Get a valid property index from a string
PropDb_get_prop_index_from_trace_index()
Returns the index of the property associated to a trace.
PropDb_get_prop_index()
Returns the index of a property in the database
PropDb_get_props_of_type()
Given a property type returns the list of properties of that type currently located into the property database
PropDb_get_size()
Returns the size of the DB
PropDb_print_all_status_type()
Prints all the properties stored in the DB
PropDb_print_all_status()
Prints all the properties stored in the DB
PropDb_print_all_type()
Prints all the properties stored in the DB
PropDb_print_all()
Prints all the properties stored in the DB
PropDb_print_list_header()
Prints the header of the property list
PropDb_print_prop_at_index()
Prints the specified property from the DB
PropDb_prop_create_and_add()
Inserts a property in the DB of properties
PropDb_prop_parse_and_add()
Add a property to the database from a string and a type
PropDb_verify_all_type()
Verifies all properties of a given type
PropDb_verify_all()
Verifies all the properties in the DB
PropDb_verify_prop_at_index()
Verifies a given property
PropPkg_init_cmd()
Initiliaze the prop package for commands
PropPkg_init()
Initializes the package: master property and property database are allocated
PropPkg_quit_cmd()
Quit the prop package for commands
PropPkg_quit()
Quits the package
PropType_to_string()
Returns the a string associated to a property type
Prop_apply_coi_for_bdd()
Applies cone of influence to the given property
Prop_apply_coi_for_bmc()
Applies cone of influence to the given property
Prop_check_type()
Check if a property in the database is of a given type
Prop_create_partial()
Creates a property, but does not insert it within the database, so the property can be used on the fly.
Prop_create()
Allocate a property
Prop_destroy()
Free a property
Prop_get_bdd_fsm()
Returns the boolean FSM in BDD of a property
Prop_get_be_fsm()
Returns the boolean FSM in BE of a property
Prop_get_bool_sexp_fsm()
Returns the boolean FSM in sexp of a property
Prop_get_cone()
Returns the cone of a property
Prop_get_context_text()
Returns the context name of a property
Prop_get_expr()
Returns the property
Prop_get_index()
Returns the index of a property
Prop_get_number_as_string()
Returns the number value as a string (only for compute types)
Prop_get_number()
Returns the number of the property
Prop_get_scalar_sexp_fsm()
Returns the scalar FSM in sexp of a property
Prop_get_status_as_string()
Returns the a string associated to a property status
Prop_get_status()
Returns the status of the property
Prop_get_text()
Returns the property text, with no explicit context
Prop_get_trace()
Returns the trace number associated to a property
Prop_get_type_as_string()
Returns the a string associated to a property type
Prop_get_type()
Returns the property type
Prop_is_psl_ltl()
Returns true if the property is PSL property and it is LTL compatible, that means that can be converted to LTL
Prop_is_psl_obe()
Returns true if the property is PSL property and it is CTL compatible
Prop_master_get_bdd_fsm()
Returns the boolean FSM in BDD
Prop_master_get_be_fsm()
Returns the boolean FSM in BE
Prop_master_get_bool_sexp_fsm()
Returns the boolean FSM in sexp
Prop_master_get_scalar_sexp_fsm()
Returns the scalar FSM
Prop_master_set_bdd_fsm()
Set the boolean FSM in BDD
Prop_master_set_be_fsm()
Set the boolean FSM in BE
Prop_master_set_bool_sexp_fsm()
Set the boolean FSM in sexp
Prop_master_set_scalar_sexp_fsm()
Set the scalar FSM
Prop_print_db()
Prints a property with info or its position and status within the database
Prop_print()
Prints a property
Prop_set_bdd_fsm()
Sets the boolean FSM in BDD of a property
Prop_set_be_fsm()
Sets the boolean FSM in BE of a property
Prop_set_bool_sexp_fsm()
Sets the boolean FSM in sexp of a property
Prop_set_cone()
Sets the cone of a property
Prop_set_fsm_to_master()
Copies master prop FSM data into prop
Prop_set_index()
Sets the index of a property
Prop_set_number_infinite()
Sets the number of the property to INFINITE
Prop_set_number()
Sets the number of the property
Prop_set_scalar_sexp_fsm()
Sets the scalar FSM in sexp of a property
Prop_set_status()
Sets the status of the property
Prop_set_trace()
Sets the trace number
Prop_verify()
Verifies a given property
prop_db_get_prop_type_as_parsing_string()
Returns the parsing type given the property type
prop_db_prop_parse_from_arg_and_add()
Add a property to the database from an arg structure and a type
prop_deinit()
Destroy the elements of a property
prop_init()
Initializes the property
prop_print()
Prints a property
prop_set_bdd_fsm()
prop_set_be_fsm()
prop_set_bool_sexp_fsm()
prop_set_scalar_sexp_fsm()

Last updated on 2005/11/21 16h:42