Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __CPROVER_object_from __CPROVER_assignable __CPROVER_freeable An error will be triggered in case calls to these functions occur outside of a contrat clause and were hence not mapped to their library implementation.

void disable_checks ()

Adds "checked" pragmas to instructions of all library functions instructions.

bool is_front_end_builtin (const irep_idt &function_id) const

Returns true iff the given function_id is one of __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto, __CPROVER_freeable

dfcc_funt get_hook (const irep_idt &function_id) const

Returns the library instrumentation hook for the given front-end function.

std::optional< dfcc_funt > get_havoc_hook (const irep_idt &function_id) const

Returns the library instrumentation hook for the given built-in.

const symbolt & get_instrumented_functions_map_symbol ()

Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.

void add_instrumented_functions_map_init_instructions (const std::set< irep_idt > &instrumented_functions, const source_locationt &source_location, goto_programt &dest)

Generates instructions to initialize the instrumented function map symbol from the given set of instrumented function.

const code_function_callt 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)

Builds call to __CPROVER_contracts_write_set_create.

const code_function_callt write_set_create_call (const exprt &write_set_ptr, const exprt &contract_assigns_size, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_create.

const code_function_callt write_set_release_call (const exprt &write_set_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_release.

const code_function_callt write_set_add_allocated_call (const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_add_allocated.

const code_function_callt write_set_add_decl_call (const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_add_decl.

const code_function_callt write_set_record_dead_call (const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_record_dead.

const code_function_callt write_set_record_deallocated_call (const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_record_deallocated.

const code_function_callt write_set_check_allocated_deallocated_is_empty_call (const exprt &check_var, const exprt &write_set_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty.

const code_function_callt 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)

Builds call to __CPROVER_contracts_write_set_check_assignment.

const code_function_callt write_set_check_array_set_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_check_array_set.

const code_function_callt write_set_check_array_copy_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_check_array_copy.

const code_function_callt 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)

Builds call to __CPROVER_contracts_write_set_check_array_replace.

const code_function_callt write_set_check_havoc_object_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_check_havoc_object.

const code_function_callt write_set_check_deallocate_call (const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_check_deallocate.

const code_function_callt 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)

Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.

const code_function_callt 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)

Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion.

const code_function_callt write_set_deallocate_freeable_call (const exprt &write_set_ptr, const exprt &target_write_set_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_write_set_deallocate_freeable.

const code_function_callt link_ptr_pred_ctx_call (const exprt &write_set_ptr, const exprt &ptr_pred_ctx_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_link_ptr_pred_ctx.

const code_function_callt link_allocated_call (const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_link_allocated.

const code_function_callt link_deallocated_call (const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_link_deallocated.

const code_function_callt check_replace_ensures_was_freed_preconditions_call (const exprt &ptr, const exprt &write_set_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions.

const code_function_callt obj_set_create_indexed_by_object_id_call (const exprt &obj_set_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id.

const code_function_callt obj_set_release_call (const exprt &obj_set_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_obj_set_release.

const code_function_callt ptr_pred_ctx_init_call (const exprt &ptr_pred_ctx_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_ptr_pred_ctx_init.

const code_function_callt ptr_pred_ctx_reset_call (const exprt &ptr_pred_ctx_ptr, const source_locationt &source_location)

Builds call to __CPROVER_contracts_ptr_pred_ctx_init.

Public Attributes

std::map< dfcc_typet, typet > dfcc_type

Maps enum values to the actual types (dynamically loaded)

std::map< dfcc_funt, symbolt > dfcc_fun_symbol

Maps enum values to the actual function symbols (dynamically loaded)

Protected Member Functions

std::set< irep_idt > get_missing_funs ()

Collects the names of all library functions currently missing from the goto_model into missing.

void inline_functions ()

Inlines library functions that need to be inlined before use.

void fix_malloc_free_calls ()

Fixes function calls to malloc and free in library functions.

Protected Attributes

goto_modelt & goto_model

message_handlert & message_handler

messaget log

Static Protected Attributes

static bool loaded = false

True iff the contracts library symbols are loaded.

static bool inlined = false

True iff the library functions are inlined.

static bool specialized = false

True iff the library functions are specialized to a particular contract.

static bool malloc_free_fixed = false

True iff the library functions uses of malloc and free are fixed.

Private Attributes

const std::map< dfcc_typet, irep_idt > dfcc_type_to_name

Enum to type name mapping.

const std::map< irep_idt, dfcc_typet > dfcc_name_to_type

Swapped dfcc_type_to_name.

const std::map< dfcc_funt, irep_idt > dfcc_fun_to_name

enum to function name mapping

const std::map< irep_idt, dfcc_funt > dfcc_name_to_fun

const std::map< irep_idt, dfcc_funt > dfcc_hook

Maps built-in function names to enums to use for instrumentation.

const std::map< irep_idt, dfcc_funt > havoc_hook

Maps front-end functions to library functions giving their havoc semantics.

const std::set< irep_idt > assignable_builtin_names

All built-in function names (front-end and instrumentation hooks)

Detailed Description

Class interface to library types and functions defined in cprover_contracts.c .

Definition at line 162 of file dfcc_library.h.

Constructor & Destructor Documentation

◆ dfcc_libraryt()

dfcc_libraryt::dfcc_libraryt ( goto_modelt & goto_model,

message_handlert & lmessage_handler

)

Class constructor.

Definition at line 179 of file dfcc_library.cpp.

Member Function Documentation

◆ add_instrumented_functions_map_init_instructions()

void dfcc_libraryt::add_instrumented_functions_map_init_instructions ( const std::set< irep_idt > & instrumented_functions,

const source_locationt & source_location,

goto_programt & dest

)

Generates instructions to initialize the instrumented function map symbol from the given set of instrumented function.

Definition at line 543 of file dfcc_library.cpp.

◆ check_replace_ensures_was_freed_preconditions_call()

const code_function_callt dfcc_libraryt::check_replace_ensures_was_freed_preconditions_call ( const exprt & ptr,

const exprt & write_set_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions.

Definition at line 858 of file dfcc_library.cpp.

◆ disable_checks()

void dfcc_libraryt::disable_checks ( )

Adds "checked" pragmas to instructions of all library functions instructions.

By default checks are not disabled.

Definition at line 232 of file dfcc_library.cpp.

◆ fix_malloc_free_calls()

void dfcc_libraryt::fix_malloc_free_calls ( )

protected

Fixes function calls to malloc and free in library functions.

Change calls to __CPROVER_contracts_malloc into calls to malloc Change calls to __CPROVER_contracts_free into calls to free

Definition at line 469 of file dfcc_library.cpp.

◆ get_dfcc_fun()

std::optional< dfcc_funt > dfcc_libraryt::get_dfcc_fun ( const irep_idt & id ) const

Returns the dfcc_funt that corresponds to the given id if any.

Definition at line 371 of file dfcc_library.cpp.

◆ get_dfcc_fun_name()

const irep_idt & dfcc_libraryt::get_dfcc_fun_name ( dfcc_funt fun ) const

Returns the name of the given dfcc_funt.

Definition at line 385 of file dfcc_library.cpp.

◆ get_havoc_hook()

std::optional< dfcc_funt > dfcc_libraryt::get_havoc_hook ( const irep_idt & function_id ) const

Returns the library instrumentation hook for the given built-in.

function_id must be one of __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto

Definition at line 212 of file dfcc_library.cpp.

◆ get_hook()

dfcc_funt dfcc_libraryt::get_hook ( const irep_idt & function_id ) const

Returns the library instrumentation hook for the given front-end function.

Returns the instrumentation function to use for a given front-end function.

Precondition: function_id is a front end built-in as defined by is_front_end_builtin.

Definition at line 204 of file dfcc_library.cpp.

◆ get_instrumented_functions_map_symbol()

const symbolt & dfcc_libraryt::get_instrumented_functions_map_symbol ( )

Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.

This symbol is an unbounded map of booleans indexed by function pointer ID, meant to have value true for instrumented functions and false for non-instrumented functions. Initialisation instructions for this map are generated by add_instrumented_functions_map_init_instructions

Definition at line 521 of file dfcc_library.cpp.

◆ get_missing_funs()

std::set< irep_idt > dfcc_libraryt::get_missing_funs ( )

protected

Collects the names of all library functions currently missing from the goto_model into missing.

Definition at line 244 of file dfcc_library.cpp.

◆ inhibit_front_end_builtins()

void dfcc_libraryt::inhibit_front_end_builtins ( )

Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __CPROVER_object_from __CPROVER_assignable __CPROVER_freeable An error will be triggered in case calls to these functions occur outside of a contrat clause and were hence not mapped to their library implementation.

Definition at line 500 of file dfcc_library.cpp.

◆ inline_functions()

void dfcc_libraryt::inline_functions ( )

protected

Inlines library functions that need to be inlined before use.

Definition at line 412 of file dfcc_library.cpp.

◆ is_dfcc_library_symbol()

bool dfcc_libraryt::is_dfcc_library_symbol ( const irep_idt & id ) const

True iff the given id is one of the library symbols.

Definition at line 380 of file dfcc_library.cpp.

◆ is_front_end_builtin()

bool dfcc_libraryt::is_front_end_builtin ( const irep_idt & function_id ) const

Returns true iff the given function_id is one of __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto, __CPROVER_freeable

Returns the instrumentation function to use for a given front-end function.

Definition at line 198 of file dfcc_library.cpp.

◆ link_allocated_call()

const code_function_callt dfcc_libraryt::link_allocated_call ( const exprt & write_set_postconditions_ptr,

const exprt & write_set_to_link_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_link_allocated.

Definition at line 833 of file dfcc_library.cpp.

◆ link_deallocated_call()

const code_function_callt dfcc_libraryt::link_deallocated_call ( const exprt & write_set_postconditions_ptr,

const exprt & write_set_to_link_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_link_deallocated.

Definition at line 845 of file dfcc_library.cpp.

◆ link_ptr_pred_ctx_call()

const code_function_callt dfcc_libraryt::link_ptr_pred_ctx_call ( const exprt & write_set_ptr,

const exprt & ptr_pred_ctx_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_link_ptr_pred_ctx.

Definition at line 821 of file dfcc_library.cpp.

◆ load()

void dfcc_libraryt::load ( std::set< irep_idt > & to_instrument )

After calling this function, all library types and functions are present in the the goto_model.

Any other functions that the DFCC functions rely on and need to be instrumented will be added to to_instrument

Definition at line 283 of file dfcc_library.cpp.

◆ obj_set_create_indexed_by_object_id_call()

const code_function_callt dfcc_libraryt::obj_set_create_indexed_by_object_id_call ( const exprt & obj_set_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id.

Definition at line 872 of file dfcc_library.cpp.

◆ obj_set_release_call()

const code_function_callt dfcc_libraryt::obj_set_release_call ( const exprt & obj_set_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_obj_set_release.

Definition at line 884 of file dfcc_library.cpp.

◆ ptr_pred_ctx_init_call()

const code_function_callt dfcc_libraryt::ptr_pred_ctx_init_call ( const exprt & ptr_pred_ctx_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_ptr_pred_ctx_init.

Definition at line 894 of file dfcc_library.cpp.

◆ ptr_pred_ctx_reset_call()

const code_function_callt dfcc_libraryt::ptr_pred_ctx_reset_call ( const exprt & ptr_pred_ctx_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_ptr_pred_ctx_init.

Definition at line 905 of file dfcc_library.cpp.

◆ specialize()

void dfcc_libraryt::specialize ( const std::size_t contract_assigns_size_hint )

Specializes the library by unwinding loops in library functions to the given assigns clause size.

Parameters: contract_assigns_size_hint size of the assigns clause being checked

Definition at line 435 of file dfcc_library.cpp.

◆ write_set_add_allocated_call()

const code_function_callt dfcc_libraryt::write_set_add_allocated_call ( const exprt & write_set_ptr,

const exprt & ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_add_allocated.

Definition at line 628 of file dfcc_library.cpp.

◆ write_set_add_decl_call()

const code_function_callt dfcc_libraryt::write_set_add_decl_call ( const exprt & write_set_ptr,

const exprt & ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_add_decl.

Definition at line 640 of file dfcc_library.cpp.

◆ write_set_check_allocated_deallocated_is_empty_call()

const code_function_callt dfcc_libraryt::write_set_check_allocated_deallocated_is_empty_call ( const exprt & check_var,

const exprt & write_set_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty.

Definition at line 677 of file dfcc_library.cpp.

◆ write_set_check_array_copy_call()

const code_function_callt 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

)

Builds call to __CPROVER_contracts_write_set_check_array_copy.

Definition at line 720 of file dfcc_library.cpp.

◆ write_set_check_array_replace_call()

const code_function_callt 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

)

Builds call to __CPROVER_contracts_write_set_check_array_replace.

Definition at line 734 of file dfcc_library.cpp.

◆ write_set_check_array_set_call()

const code_function_callt 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

)

Builds call to __CPROVER_contracts_write_set_check_array_set.

Definition at line 706 of file dfcc_library.cpp.

◆ write_set_check_assignment_call()

const code_function_callt 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

)

Builds call to __CPROVER_contracts_write_set_check_assignment.

Definition at line 691 of file dfcc_library.cpp.

◆ write_set_check_assigns_clause_inclusion_call()

const code_function_callt 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

)

Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.

Definition at line 778 of file dfcc_library.cpp.

◆ write_set_check_deallocate_call()

const code_function_callt dfcc_libraryt::write_set_check_deallocate_call ( const exprt & check_var,

const exprt & write_set_ptr,

const exprt & ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_check_deallocate.

Definition at line 763 of file dfcc_library.cpp.

◆ write_set_check_frees_clause_inclusion_call()

const code_function_callt 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

)

Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion.

Definition at line 794 of file dfcc_library.cpp.

◆ write_set_check_havoc_object_call()

const code_function_callt 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

)

Builds call to __CPROVER_contracts_write_set_check_havoc_object.

Definition at line 749 of file dfcc_library.cpp.

◆ write_set_create_call() [1/2]

const code_function_callt 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

)

Builds call to __CPROVER_contracts_write_set_create.

Definition at line 567 of file dfcc_library.cpp.

◆ write_set_create_call() [2/2]

const code_function_callt dfcc_libraryt::write_set_create_call ( const exprt & write_set_ptr,

const exprt & contract_assigns_size,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_create.

Definition at line 599 of file dfcc_library.cpp.

◆ write_set_deallocate_freeable_call()

const code_function_callt dfcc_libraryt::write_set_deallocate_freeable_call ( const exprt & write_set_ptr,

const exprt & target_write_set_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_deallocate_freeable.

Definition at line 809 of file dfcc_library.cpp.

◆ write_set_record_dead_call()

const code_function_callt dfcc_libraryt::write_set_record_dead_call ( const exprt & write_set_ptr,

const exprt & ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_record_dead.

Definition at line 652 of file dfcc_library.cpp.

◆ write_set_record_deallocated_call()

const code_function_callt dfcc_libraryt::write_set_record_deallocated_call ( const exprt & write_set_ptr,

const exprt & ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_record_deallocated.

Definition at line 664 of file dfcc_library.cpp.

◆ write_set_release_call()

const code_function_callt dfcc_libraryt::write_set_release_call ( const exprt & write_set_ptr,

const source_locationt & source_location

)

Builds call to __CPROVER_contracts_write_set_release.

Definition at line 617 of file dfcc_library.cpp.

Member Data Documentation

◆ assignable_builtin_names

const std::set<irep_idt> dfcc_libraryt::assignable_builtin_names

private

All built-in function names (front-end and instrumentation hooks)

Definition at line 217 of file dfcc_library.h.

◆ dfcc_fun_symbol

std::map<dfcc_funt, symbolt> dfcc_libraryt::dfcc_fun_symbol

Maps enum values to the actual function symbols (dynamically loaded)

Definition at line 224 of file dfcc_library.h.

◆ dfcc_fun_to_name

const std::map<dfcc_funt, irep_idt> dfcc_libraryt::dfcc_fun_to_name

private

enum to function name mapping

Definition at line 205 of file dfcc_library.h.

◆ dfcc_hook

const std::map<irep_idt, dfcc_funt> dfcc_libraryt::dfcc_hook

private

Maps built-in function names to enums to use for instrumentation.

Definition at line 211 of file dfcc_library.h.

◆ dfcc_name_to_fun

const std::map<irep_idt, dfcc_funt> dfcc_libraryt::dfcc_name_to_fun

private

Definition at line 208 of file dfcc_library.h.

◆ dfcc_name_to_type

const std::map<irep_idt, dfcc_typet> dfcc_libraryt::dfcc_name_to_type

private

Swapped dfcc_type_to_name.

Definition at line 202 of file dfcc_library.h.

◆ dfcc_type

std::map<dfcc_typet, typet> dfcc_libraryt::dfcc_type

Maps enum values to the actual types (dynamically loaded)

Definition at line 221 of file dfcc_library.h.

◆ dfcc_type_to_name

const std::map<dfcc_typet, irep_idt> dfcc_libraryt::dfcc_type_to_name

private

Enum to type name mapping.

Definition at line 199 of file dfcc_library.h.

◆ goto_model

goto_modelt& dfcc_libraryt::goto_model

protected

Definition at line 181 of file dfcc_library.h.

◆ havoc_hook

const std::map<irep_idt, dfcc_funt> dfcc_libraryt::havoc_hook

private

Maps front-end functions to library functions giving their havoc semantics.

Definition at line 214 of file dfcc_library.h.

◆ inlined

bool dfcc_libraryt::inlined = false

staticprotected

True iff the library functions are inlined.

Definition at line 172 of file dfcc_library.h.

◆ loaded

bool dfcc_libraryt::loaded = false

staticprotected

True iff the contracts library symbols are loaded.

Definition at line 169 of file dfcc_library.h.

◆ log

messaget dfcc_libraryt::log

protected

Definition at line 183 of file dfcc_library.h.

◆ malloc_free_fixed

bool dfcc_libraryt::malloc_free_fixed = false

staticprotected

True iff the library functions uses of malloc and free are fixed.

True iff the library functions have already been fixed.

Definition at line 179 of file dfcc_library.h.

◆ message_handler

message_handlert& dfcc_libraryt::message_handler

protected

Definition at line 182 of file dfcc_library.h.

◆ specialized

bool dfcc_libraryt::specialized = false

staticprotected

True iff the library functions are specialized to a particular contract.

Definition at line 176 of file dfcc_library.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp