Difference between revisions of "C Integer Programs"
From Termination-Portal.org
Jump to navigationJump to searchCryingshadow (talk | contribs) |
Cryingshadow (talk | contribs) |
||
| Line 9: | Line 9: | ||
The syntax of termination problems in this category is defined using the following non-terminals: | The syntax of termination problems in this category is defined using the following non-terminals: | ||
| − | P | + | ;P |
| − | PRE | + | : Program |
| − | POST | + | ;PRE |
| − | D | + | : Start of the program, including the declaration of an external function for non-deterministic values |
| − | V | + | ;POST |
| − | INS | + | : The end of the program |
| − | A | + | ;D |
| − | L | + | : Variable declaration |
| − | C | + | ;V |
| − | NE | + | : Variable name |
| − | N | + | ;INS |
| − | BE | + | : Instruction |
| − | NO | + | ;A |
| − | BO | + | : Assignment |
| − | BC | + | ;L |
| − | W | + | : 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): | The grammar is then (EBNF-like): | ||
| − | + | P = PRE D* W? I* POST | |
| − | P = PRE D* W? I* POST | + | PRE = W? |
| − | 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? | |
| − | POST = W? "return" W "0" W? ";" W? "}" W? | + | 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? ";" |
| − | I = (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? I* 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? I* W? "}" (W? "else" W? "{" W? I* 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? ")" | + | BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")" |
| − | BE = "true" | "false" | NE W? BO W? NE | BE W? BC W? BE | "!" W? BE | "(" W? BE W? ")" | + | NO = "+" | "-" | "*" |
| − | NO = "+" | "-" | "*" | + | BO = "<" | ">" | "<=" | ">=" | "==" | "!=" |
| − | BO = "<" | ">" | "<=" | ">=" | "==" | "!=" | + | BC = "&&" | "||" | "==" | "!=" |
| − | BC = "&&" | "||" | "==" | "!=" | + | W = (" " | "\n") (" " | "\n")* |
| − | W = (" " | "\n") (" " | "\n")* | ||
| − | |||
| − | Calls to | + | Calls to <code>__VERIFIER_nondet_int()</code> 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. | Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used. | ||
Revision as of 13:08, 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? I* 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]*
I = (A | L | C) W? ";"
A = V W? "=" W? NE
L = "while" W? "(" W? BE W? ")" W? "{" W? I* W? "}"
C = "if" W? "(" W? BE W? ")" W? "{" W? I* W? "}" (W? "else" W? "{" W? I* 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.
