dfcc_libraryt Member List

This is the complete list of members for dfcc_libraryt, including all inherited members.

add_instrumented_functions_map_init_instructions(const std::set< irep_idt > &instrumented_functions, const source_locationt &source_location, goto_programt &dest)	dfcc_libraryt
assignable_builtin_names	dfcc_libraryt	private
check_replace_ensures_was_freed_preconditions_call(const exprt &ptr, const exprt &write_set_ptr, const source_locationt &source_location)	dfcc_libraryt
dfcc_fun_symbol	dfcc_libraryt
dfcc_fun_to_name	dfcc_libraryt	private
dfcc_hook	dfcc_libraryt	private
dfcc_libraryt(goto_modelt &goto_model, message_handlert &lmessage_handler)	dfcc_libraryt
dfcc_name_to_fun	dfcc_libraryt	private
dfcc_name_to_type	dfcc_libraryt	private
dfcc_type	dfcc_libraryt
dfcc_type_to_name	dfcc_libraryt	private
disable_checks()	dfcc_libraryt
fix_malloc_free_calls()	dfcc_libraryt	protected
get_dfcc_fun(const irep_idt &id) const	dfcc_libraryt
get_dfcc_fun_name(dfcc_funt fun) const	dfcc_libraryt
get_havoc_hook(const irep_idt &function_id) const	dfcc_libraryt
get_hook(const irep_idt &function_id) const	dfcc_libraryt
get_instrumented_functions_map_symbol()	dfcc_libraryt
get_missing_funs()	dfcc_libraryt	protected
goto_model	dfcc_libraryt	protected
havoc_hook	dfcc_libraryt	private
inhibit_front_end_builtins()	dfcc_libraryt
inline_functions()	dfcc_libraryt	protected
inlined	dfcc_libraryt	protectedstatic
is_dfcc_library_symbol(const irep_idt &id) const	dfcc_libraryt
is_front_end_builtin(const irep_idt &function_id) const	dfcc_libraryt
link_allocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)	dfcc_libraryt
link_deallocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)	dfcc_libraryt
link_is_fresh_call(const exprt &write_set_ptr, const exprt &is_fresh_obj_set_ptr, const source_locationt &source_location)	dfcc_libraryt
load(std::set< irep_idt > &to_instrument)	dfcc_libraryt
loaded	dfcc_libraryt	protectedstatic
log	dfcc_libraryt	protected
malloc_free_fixed	dfcc_libraryt	protectedstatic
message_handler	dfcc_libraryt	protected
obj_set_create_indexed_by_object_id_call(const exprt &obj_set_ptr, const source_locationt &source_location)	dfcc_libraryt
obj_set_release_call(const exprt &obj_set_ptr, const source_locationt &source_location)	dfcc_libraryt
specialize(const std::size_t contract_assigns_size_hint)	dfcc_libraryt
specialized	dfcc_libraryt	protectedstatic
write_set_add_allocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_add_decl_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_check_allocated_deallocated_is_empty_call(const exprt &check_var, const exprt &write_set_ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_check_array_copy_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)	dfcc_libraryt
write_set_check_array_replace_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const exprt &src, const source_locationt &source_location)	dfcc_libraryt
write_set_check_array_set_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)	dfcc_libraryt
write_set_check_assignment_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const exprt &size, const source_locationt &source_location)	dfcc_libraryt
write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_check_deallocate_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_check_frees_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_check_havoc_object_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)	dfcc_libraryt
write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const source_locationt &source_location)	dfcc_libraryt
write_set_deallocate_freeable_call(const exprt &write_set_ptr, const exprt &target_write_set_ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_record_dead_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_record_deallocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)	dfcc_libraryt
write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)	dfcc_libraryt