--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on July 2009 ---
Strange ... well this is my version -------- /usr/local/bin/./frama-c -version Version: Lithium-20081201 Compilation date: Fri Jul 10 09:15:56 MST 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 ---------- So maybe I am using it wrong ? but I don't see how ! mhh .. any tips what I can do to find the reason for my errors? Greets On Mon, Jul 27, 2009 at 12:44 PM, Julien Signoles<Julien.Signoles at cea.fr> wrote: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >