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):

P = PRE D* W? INS* POST
PRE = W?
      "extern"
      W
      "int"
      W
      "__VERIFIER_nondet_int"
      W?
      "("
      W?
      "void"
      W?
      ")"
      W?
      ";"
      W?
      "int"
      W
      "main"
      W?
      "("
      W?
      ")"
      W?
      "{"
      W?
POST = W? "return" W "0" W? ";" W? "}" W?
D = "int" W V W? ";"
V = [a-z,A-Z] [a-z,A-Z,0-9]*
INS = (A | L | C) W? ";"
A = V W? "=" W? NE
L = "while" W? "(" W? BE W? ")" W? "{" W? INS* W? "}"
C = "if" W? "(" W? BE W? ")" W? "{" W? INS* W? "}" (W? "else" W? "{" W? INS* W? "}")?
NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")"
NO = "+" | "-" | "*"
BO = "<" | ">" | "<=" | ">=" | "==" | "!="
BC = "&&" | "||" | "==" | "!="
W = (" " | "\n") (" " | "\n")*

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 is used.