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:
    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;
    x = x + 1;
    if (x > 10) goto exit;
    goto loop;
    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.



                                eval $(opam config env)

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