--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Syntax Error although it is from the Mini-Tutorial ! ! !



Hello,

Munir Khleif a ?crit :
> But when I come to the second one I get  a Syntax error from frama-c
> 
> output
> ----------------------------------
> Parsing
> [preprocessing] running gcc -C -E -I.   test.c
> File "test.c", line 4, characters 39-42: syntax error while parsing annotation
> 
> Cleaning unused parts
> Symbolic link
> Starting semantical analysis
> ----------------------------------
> #include <stdio.h>
> 
> 
>  /*@ requires n > 0 && \valid(p+(0..n-1));
>     @ ensures \result == \max(0,n-1, \lambda integer i; p[i]);
>     @*/
>   int max_seq(int* p, int n) {
>   int res = *p;
>   int i;
>   for(i = 0; i < n; i++) {
>          if (res < *p) { res = *p; }
>               p++;
>          }
>          return res;
>    }
> 
>    int main ( void ) {
> 
>          return 0;
>    }
> ----------------------------
> 
> So I don't really know what the problem is or might be ...
> I tryed it on 2 different linux mashines and alwas the same errors!

Your above example works without any error on my Linux machine, both 
with Frama-C Beryllium-beta1 and Frama-C Lithium. What is your Frama-C 
version?

Below is the result of my test from your example:

$ cat a.c
#include <stdio.h>


/*@ requires n > 0 && \valid(p+(0..n-1));
   @ ensures \result == \max(0,n-1, \lambda integer i; p[i]);
   @*/
int max_seq(int* p, int n) {
   int res = *p;
   int i;
   for(i = 0; i < n; i++) {
     if (res < *p) { res = *p; }
     p++;
   }
   return res;
}

int main ( void ) {

   return 0;
}

Here is my output with Frama-C Beryllium-beta1:
$ frama-c -version
Version: Beryllium-20090601-beta1
Compilation date: Thu Jul 23 11:12:28 CEST 2009
Share path: /usr/local/share/frama-c (may be overridden with 
FRAMAC_SHARE variable)
Library path: /usr/local/lib/frama-c
Plug-in paths: /usr/local/lib/frama-c/plugins (may be overriden with 
FRAMAC_PLUGIN variable)
$ frama-c a.c
[kernel...] preprocessing with "gcc -C -E -I.   a.c"

Here is my output with Frama-C Lithium:
$ frama-c -version
./bin/toplevel.opt -version
Version: Lithium-20081201
Compilation date: Mon May 4 18:22:12 CEST 2009
Frama-C library path: /usr/local/share/frama-c (may be overridden with 
FRAMAC_SHARE variable)
Parsing
Cleaning unused parts
Symbolic link
Starting semantical analysis
$ frama-c a.c
Parsing
[preprocessing] running gcc -C -E -I.   a.c
Cleaning unused parts
Symbolic link
Starting semantical analysis

Regards,
Julien Signoles
-- 
Researcher-engineer
CEA LIST, Software Reliability Lab
91191 Gif-Sur-Yvette Cedex
tel:(+33)1.69.08.71.83  fax:(+33)1.69.08.83.95  Julien.Signoles at cea.fr