Semantics and application to program verification

Static analysis project

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.

Author: Antoine Miné