# ENS — Semantics and applications to verification

## Static analysis project

Comes mainly from here.Thanks Antoine!

### Langage syntax

The language is a very small subset of C, supporting the following constructions. At the top level, we allow only declarations:

• Global variable declarations with integer type (`int`) and an optional initializer:
```                            ```
int x;
int y = 2+2;
int x,y,z
```
```
We assume that variables without an explicit initializer are implicitly initialized to 0.
• Function declarations. Functions can return an integer (`int`) or no value (`void`). Functions also have a list of integer arguments:
```                            ```
int f(int x, int y)
{
...
}

void g()
{
...
}
```
```

Inside functions, we allow the following instructions:

• Blocks of instructions in curly brackets `{ ... }`.
• Assignments of an integer expression into a variable. Expressions can use the classic integer operators `+`, `-`, `*`, `/`, `%`. Expressions can also call functions. For instance:
```                            ```
x = 2 + 5;
x = 2 * f(x, f(2 * x)-1);
```
```
The syntax also supports the shortcuts `x++`, `x--`, `x += ...`, `x *= ...`, etc.
• Calls to functions returning no argument can appear as stand-alone instructions:
g();
Note that supporting function calls (both returning a value and not) is not required as a core feature of your analyzer, but you can offer it as an extension.
• Tests `if then` or `if then else`:
```                            ```
if (x==0) x++;
if (x > 0 && x < 100) { x = 2*x; y--; } else { x = 0; y++; }
```
```
Note that the condition in the `if` must be a boolean expression. Boolean expressions are composed of atoms comparing two integer expressions with `==`, `!=`, `<`, `>`, `<=`, `>=`. Atoms can be combined with the boolean operators `!`, `&&`, `||`. Note that, `if (x)`, where `x` is an integer variable, is supported in C but not in our language. Similarly to Java, you must type `if (x!=0)`.
• Loops can use the `while` or `for` standard C constructions (there is no support for `do ... while`). Here are some examples:
```                            ```
while (a<10) { a = a - 1; }
for (i=0;i<10;i++) x++;
for (;;);
```
```
• The `break` instruction can be used to exit the innermost loop:
```                            ```
for (i=0;i<10;i++) {
while (y<10) {
if (x>10) break;
x++; y++;
}
// the break jumps here
}
```
```
• The `return` instruction exits the current function. For functions returning an integer, it takes an integer expression as parameter, as in `return 2+3;`; otherwise, it is just `return;`.
• Arbitrary jumps inside functions are allowed. A label (destination of a jump) is denoted with a colon, as in `a:`. A jump is denoted as `goto a;`. Both forward and backward jumps are allowed. For instance:
```                            ```
x = 0;
loop:
x = x + 1;
...
if (x > 10) goto exit;
...
goto loop;
exit:
x = 0;
```
```
• Local variable declarations. The syntax is similar to the syntax of global declarations, but the variable is only visible inside the current block.

Protip

Ajoutez

```                            ```
eval \$(opam config env)
```
```

à votre `.bashrc` (ou `.zshrc`, ...) pour ne plus avoir de problème avec OCaml.