The toy language accepted by the analyzer has a C-inspired syntax.
Note that, before the analysis takes place, the program is simplified to ensure that there is at most one side-effect by statement. Implicit casts in expressions (to model integer promotion and usual arithmetic conversions) are also introduced explicitly. Finally, extra statements are generated to bind formal arguments and return values of functions.
In order to avoid straining the servers, the analysis is limited to small programs with few variables.
The language features boolean and numeric types.
| type | ::= | int-type | real-type | bool |
| int-type | ::= | int-length | unsigned int-length |
| int-length | ::= | char | short | int | long | integer |
| real-type | ::= | float | double | real |
Integer types of different size are available: 8-bit char, 16-bit short, 32-bit int, and 64-bit long, and exist in signed and unsigned versions. However, bound checking is not implemented at the moment; the type only affects the initial range of variables. The type integer corresponds to unbounded integers.
Various types of reals are also available. Floating-point numbers can be 32-bit float or 64-bit double. Bound checking is not implemented at the moment, but rounding is handled. The type real corresponds to mathematical reals, with no bound and no rounding.
The language accepts a subset of C statements.
| stat | ::= | expr; |
| | | ; | |
| | | local-decl | |
| | | assert (expr); | |
| | | return; | |
| | | return expr; | |
| | | break; | |
| | | if (expr) stat | |
| | | if (expr) stat else stat | |
| | | while (expr) stat | |
| | | { stat ... stat } |
Note that the expressions appearing in if, while, and assert constructs must be boolean and cannot be numeric.
As in C, expressions include assignments, incrementations, and function calls.
| expr | ::= | lvalue assign-op expr |
| | | expr bin-op expr | |
| | | un-op expr | |
| | | expr incr-op | |
| | | incr-op expr | |
| | | (type) expr | |
| | | id(expr, ..., expr) | |
| | | (expr) | |
| | | bool-const | |
| | | num-const | |
| | | [num-const;num-const] | |
| assign-op | ::= | = | += | -= | *= | /= | %= |
| bin-op | ::= | + | - | * | / | % | < | > | <= | >= | == | != | && | || |
| un-op | ::= | + | - | ! |
| incr-op | ::= | ++ | -- |
| bool-const | ::= | true | false |
| num-const | ::= | int-const | float-const |
Numeric constants include intervals [a;b], which model a non-deterministic choice. Each time the expression is evaluated, a new value between a and b is chosen.
The only lvalues allowed so-far are simple variable names.
| lvalue | ::= | id |
Declarations include the declaration of local and global variables (with an optional initialization value), of functions (with an optional return type and arbitrary arguments), and of volatiles.
| decl | ::= | local-decl | volatile-decl | fun-decl |
| local-decl | ::= | type var-decl, ..., var-decl; |
| volatile-decl | ::= | volatile type var-decl, ..., var-decl; |
| var-decl | ::= | id | id = expr |
| fun-decl | ::= | type-void id (type id, ..., type id) { stat ... stat } |
| type-void | ::= | type | void |
Variables with no initialization expression specified are considered to have any value in the range of their type.
Volatile variables cannot be assigned. Each time they are evaluated as part of an expression, a non-deterministic value in their initialization range is returned.
A program is a list of declarations. The entry-point of the program is given as a parameter to the analysis; it can be any function with no argument and no return value.