Search papers, labs, and topics across Lattice.
This paper introduces a symbolic execution framework designed to generate function contracts, specifically focusing on handling array manipulations by carrying invariants and assigns information over contiguous array segments. The approach addresses the challenge of inferring invariants and assigns information over array segments in inter-procedural analysis. The framework is implemented within LLVM and integrated with ACSL and Frama-C, demonstrating its effectiveness on benchmarks and realistic library functions involving complex array operations.
Symbolic execution gets a boost for array-heavy code, now tracking invariants across contiguous array segments to generate more accurate function contracts.
Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in inter-procedural analysis where properties of functions are first obtained via the generation of function contracts and then the generated contracts are used as building blocks to analyze the whole program. Typical objectives in function contract generation include pre-/post-conditions and assigns information (that specifies the modification information over program variables and memory segments during function execution). In programs with array manipulations, a crucial point in function contract generation is the treatment of array segments that imposes challenges in inferring invariants and assigns information over such segments. To address this challenge, we propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays. We implement our framework as a prototype within LLVM, and further integrate our prototype with the ACSL assertion format and the Frama-C software verification platform. Experimental evaluation over a variety of benchmarks from the literature and functions from realistic libraries shows that our framework is capable of handling array manipulating functions that indeed involve the carry of array information and are beyond existing approaches.
