Klever

Supporting uncertain environment behavior, e.g. assume that functions without definitions can return any value allowed by their return types, may be the only choice when there are many target programs and not so much time to develop appropriate models. For particular programs this just prevents to understand quickly that some functions need models.

Anton already specified a preliminary set of options to disable uncertain environment behavior:

cpa.smg.enableHeapAbstraction = false
cpa.smg.handleIncompleteExternalVariableAsExternalAllocation = false
cpa.smg.handleUnknownDereferenceAsSafe = false
cpa.smg.handleUnknownFunctions = STRICT
cpa.smg.merge = "SEP" 

# List of unknown function which are always considered as safe functions, i.e., free
# of memory-related side-effects
cpa.smg.safeUnknownFunctions = {"abort"}

This is great and it does work, but we need one more extra feature from CPAchecker to assume that all functions starting with "ldv_" are safe even when they do not have bodies. The list of such functions is open while most of them does not require definitions actually. For instance, some functions (e.g. ldv_check_final_state()) are defined just by particular requirement specifications.