C Integer Programs

Proposal

For the Termination Competition 2015, we propose a new category for C programs restricted to a very small subset of C operating only on integers with addition, subtraction, and multiplication. The purpose of this category is twofold: First, it is easier for new participants to first start with a restricted subset of C than directly tackling the whole language. Second, this subset captures all necessary concepts to express integer transition systems as used by many program analysis tools as intermediate representation of programs.

Syntax and Semantics

The syntax of termination problems in this category is defined using the following non-terminals:

P:: Program PRE:: Start of the program, including the declaration of an external function for non-deterministic values POST:: The end of the program D:: Variable declaration V:: Variable name INS:: Instruction A:: Assignment L:: Loop C:: Condition NE:: Numerical expression N:: Number BE:: Boolean expression NO:: Numerical operator BO:: Boolean operator BC:: Boolean connective W:: Whitespace

The grammar is then (EBNF-like):

L 

Calls to {{{__VERIFIER_nondet_int()}}} yield non-deterministic values (possibly different ones each time the function is called) and each function call terminates without side effects.

Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used.