--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on July 2009 ---
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