Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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