--- layout: fc_discuss_archives title: Message 32 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 ! ! !



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
>