C Integer Programs

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

Grammar: 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.