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.

翻译：函数契约生成是程序分析中的一个经典问题，其目标是对包含多个过程的程序中的函数进行自动化分析。该问题在过程间分析中具有基础性地位：首先通过生成函数契约来获取函数的性质，随后将生成的契约作为构建模块来分析整个程序。函数契约生成的典型目标包括前置/后置条件以及赋值信息（用于指定函数执行期间对程序变量和内存段的修改信息）。在涉及数组操作的程序中，函数契约生成的关键在于对数组段的处理，这为推断此类数组段上的不变量和赋值信息带来了挑战。为应对这一挑战，我们提出了一种新颖的符号执行框架，该框架能够携带数组连续段上的不变量与赋值信息。我们在LLVM中实现了该框架的原型系统，并进一步将其与ACSL断言格式及Frama-C软件验证平台集成。通过对文献中多种基准测试用例及实际库函数的实验评估表明，我们的框架能够处理确实涉及数组信息携带且超出已有方法能力范围的数组操作函数。