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.

---