CBMC
dfcc_libraryt Class Reference

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

#include <dfcc_library.h>

+ Collaboration diagram for dfcc_libraryt:

Public Member Functions

 dfcc_libraryt (goto_modelt &goto_model, message_handlert &lmessage_handler)
 Class constructor. More...
 
void load (std::set< irep_idt > &to_instrument)
 After calling this function, all library types and functions are present in the the goto_model. More...
 
std::optional< dfcc_funtget_dfcc_fun (const irep_idt &id) const
 Returns the dfcc_funt that corresponds to the given id if any. More...
 
const irep_idtget_dfcc_fun_name (dfcc_funt fun) const
 Returns the name of the given dfcc_funt. More...
 
bool is_dfcc_library_symbol (const irep_idt &id) const
 True iff the given id is one of the library symbols. More...
 
void specialize (const std::size_t contract_assigns_size_hint)
 Specializes the library by unwinding loops in library functions to the given assigns clause size. More...
 
void 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. More...
 
void disable_checks ()
 Adds "checked" pragmas to instructions of all library functions instructions. More...
 
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 More...
 
dfcc_funt get_hook (const irep_idt &function_id) const
 Returns the library instrumentation hook for the given front-end function. More...
 
std::optional< dfcc_funtget_havoc_hook (const irep_idt &function_id) const
 Returns the library instrumentation hook for the given built-in. More...
 
const symboltget_instrumented_functions_map_symbol ()
 Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
const code_function_callt link_is_fresh_call (const exprt &write_set_ptr, const exprt &is_fresh_obj_set_ptr, const source_locationt &source_location)
 Builds call to __CPROVER_contracts_link_is_fresh. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 

Public Attributes

std::map< dfcc_typet, typetdfcc_type
 Maps enum values to the actual types (dynamically loaded) More...
 
std::map< dfcc_funt, symboltdfcc_fun_symbol
 Maps enum values to the actual function symbols (dynamically loaded) More...
 

Protected Member Functions

std::set< irep_idtget_missing_funs ()
 Collects the names of all library functions currently missing from the goto_model into missing. More...
 
void inline_functions ()
 Inlines library functions that need to be inlined before use. More...
 
void fix_malloc_free_calls ()
 Fixes function calls to malloc and free in library functions. More...
 

Protected Attributes

goto_modeltgoto_model
 
message_handlertmessage_handler
 
messaget log
 

Static Protected Attributes

static bool loaded = false
 True iff the contracts library symbols are loaded. More...
 
static bool inlined = false
 True iff the library functions are inlined. More...
 
static bool specialized = false
 True iff the library functions are specialized to a particular contract. More...
 
static bool malloc_free_fixed = false
 True iff the library functions uses of malloc and free are fixed. More...
 

Private Attributes

const std::map< dfcc_typet, irep_idtdfcc_type_to_name
 Enum to type name mapping. More...
 
const std::map< irep_idt, dfcc_typetdfcc_name_to_type
 Swapped dfcc_type_to_name. More...
 
const std::map< dfcc_funt, irep_idtdfcc_fun_to_name
 enum to function name mapping More...
 
const std::map< irep_idt, dfcc_funtdfcc_name_to_fun
 
const std::map< irep_idt, dfcc_funtdfcc_hook
 Maps built-in function names to enums to use for instrumentation. More...
 
const std::map< irep_idt, dfcc_funthavoc_hook
 Maps front-end functions to library functions giving their havoc semantics. More...
 
const std::set< irep_idtassignable_builtin_names
 All built-in function names (front-end and instrumentation hooks) More...
 

Detailed Description

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

Definition at line 153 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 174 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 538 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 
)

◆ 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 227 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 464 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 366 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 380 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 207 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 199 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 516 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 239 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 495 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 407 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 375 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 193 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 824 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 836 of file dfcc_library.cpp.

◆ link_is_fresh_call()

const code_function_callt dfcc_libraryt::link_is_fresh_call ( const exprt write_set_ptr,
const exprt is_fresh_obj_set_ptr,
const source_locationt source_location 
)

Builds call to __CPROVER_contracts_link_is_fresh.

Definition at line 812 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 278 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 
)

◆ 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 875 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_hintsize of the assigns clause being checked

Definition at line 430 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 619 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 631 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 
)

◆ 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 711 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 725 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 697 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 682 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 
)

◆ 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 754 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 
)

◆ 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 740 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 558 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 590 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 800 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 643 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 655 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 608 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 210 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 217 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 198 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 204 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 201 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 195 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 214 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 192 of file dfcc_library.h.

◆ goto_model

goto_modelt& dfcc_libraryt::goto_model
protected

Definition at line 174 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 207 of file dfcc_library.h.

◆ inlined

bool dfcc_libraryt::inlined = false
staticprotected

True iff the library functions are inlined.

Definition at line 165 of file dfcc_library.h.

◆ loaded

bool dfcc_libraryt::loaded = false
staticprotected

True iff the contracts library symbols are loaded.

Definition at line 162 of file dfcc_library.h.

◆ log

messaget dfcc_libraryt::log
protected

Definition at line 176 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 172 of file dfcc_library.h.

◆ message_handler

message_handlert& dfcc_libraryt::message_handler
protected

Definition at line 175 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 169 of file dfcc_library.h.


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