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 ! ! !

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
>