Project

General

Profile

Actions

Feature #10933

closed

Add configuration for CPAchecker SMG to disable uncertain environment behavior

Added by Evgeny Novikov over 2 years ago. Updated over 2 years ago.

Status:
Closed
Priority:
Urgent
Category:
Preset jobs, marks and tags
Target version:
Start date:
09/09/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

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.

Actions #1

Updated by Anton Vasilyev over 2 years ago

Added support of pattern search for safe functions to CPAchecker on branch klever_fixes:38277 as an option:
cpa.smg.safeUnknownFunctionsPatterns = "ldv_.*"

Actions #2

Updated by Evgeny Novikov over 2 years ago

  • Status changed from New to Resolved

I did the rest in branch disable-undef-behavior. The new verifier profile is "memory checking without uncertainty". The corresponding requirements specification is "test:memory checking without uncertainty". It is just for Linux and just for testing since it has a specific application domain. Let's wait for test results.

Actions #3

Updated by Evgeny Novikov over 2 years ago

  • Status changed from Resolved to Closed

Tests passed, so, I merged the branch to master in b539922e7.

Actions

Also available in: Atom PDF