Difference between revisions of "C Integer Programs"
Cryingshadow (talk | contribs) (Add new page for integer C category) |
Cryingshadow (talk | contribs) |
||
| Line 1: | Line 1: | ||
[[Category:Categories]] | [[Category:Categories]] | ||
| − | + | == 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 | P = PRE D* W? I* POST | ||
PRE = W? | PRE = W? | ||
| Line 61: | Line 68: | ||
BC = "&&" | "||" | "==" | "!=" | BC = "&&" | "||" | "==" | "!=" | ||
W = (" " | "\n") (" " | "\n")* | 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. | + | 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. | Integers are treated as mathematical integers (so no overflows can occur) and apart from that, the C-sematics are used. | ||
Revision as of 13:05, 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):
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.
