AProVE Help: C and LLVM

As in the termination category of the SV-COMP, AProVE analyzes termination of the main() function of a C program. To this end, AProVE uses the Clang compiler to translate the C program into a program in the intermediate representation of LLVM (without compiler optimizations as these are not sound for termination proving, i.e., the compiler may remove non-terminating code if this code does not contribute to the return value of a function). To compile C programs to LLVM programs, we use the following command:

clang program.c -S -emit-llvm -o program.llvm

This LLVM program is then analyzed for memory safety and termination. So in contrast to several other termination tools, AProVE only considers a program as "terminating" if it can also prove its memory safety.

Limitations

• The implementation can handle programs with several functions and recursion, but as soon as a recursive function has side effects, we abort the analysis and return MAYBE as the result.
• We cannot deal with types for floating point numbers at the moment.
• Integers are treated as the infinite set ℤ. More precisely, we disregard integer overflows and assume that variables are only instantiated with signed integers appropriate for their type.
• We cannot handle external functions at the moment. This means that the alloca function (which is also available as an instruction in LLVM) is supported by AProVE, but functions like malloc and free are currently not supported (since they are not available as LLVM instructions). However, we allow to just declare functions and use them to produce non-deterministic values. We assume that functions which are only declared, but not defined, have no side effects (in particular, they do not modify their arguments). Another exception is that we interpret function calls to the special function __VERIFIER_assert with one argument as assertions which need to hold for the program to be correct. So if we cannot prove that whenever an assertion is called, its argument evaluates to 1 (true), we abort the analysis and return MAYBE. Otherwise, our proof of memory safety also implies satisfaction of all assertions at their respective program positions.
• We assume that allocation of memory always succeeds, i.e., the alloca instruction never returns 0.
• We also do not deal with data structures (defined by struct) yet. Moreover, the handling of arrays is restricted to programs where arrays are compiled to pointers in LLVM. This means that statements like int* array = alloca(4*sizeof(int)) are supported, but statements like int array[4] are not, because these statements are compiled to an LLVM-specific array data type.
• Up to now, our parser reliably supports LLVM 2.9. Later versions of LLVM might work, but we cannot guarantee this as LLVM is very actively developed. Moreover, the following LLVM instructions are not yet supported (most of them occur rarely if one uses no compiler optimizations, can be replaced by other ones which we support, or deal with floats or complex data structures):
  • switch
  • indirectbr
  • invoke
  • unwind
  • va_arg
  • all vector and aggregate instructions
  • all instructions on floats