Difference between revisions of "C Integer Programs"

From Termination-Portal.org
Jump to navigationJump to search
(fix format and grammar)
Line 43: Line 43:
  
 
The grammar is then (EBNF-like):
 
The grammar is then (EBNF-like):
  P = PRE D* W? I* POST
+
  P = PRE D* W? INS* POST
 
  PRE = W?
 
  PRE = W?
 
       "extern"
 
       "extern"
Line 72: Line 72:
 
  D = "int" W V W? ";"
 
  D = "int" W V W? ";"
 
  V = [a-z,A-Z] [a-z,A-Z,0-9]*
 
  V = [a-z,A-Z] [a-z,A-Z,0-9]*
  I = (A | L | C) W? ";"
+
  INS = (A | L | C) W? ";"
 
  A = V W? "=" W? NE
 
  A = V W? "=" W? NE
  L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
+
  L = "while" W? "(" W? BE W? ")" W? "{" W? INS* W? "}"
  C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* 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
 
  NE = N | V | NE W? NO W? NE | "(" W? NE W? ")" | "-" W? NE
 
  N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"
 
  N = 0 | [1-9] [0-9]* | "__VERIFIER_nondet_int" W? "(" W? ")"

Revision as of 13:10, 22 June 2015


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