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



Good morning,

I am a student at Tuebingen University in germany and I am trying to
use frama-C in a project that I am working on. I installed all the
requierments and got the basic program to run "frama-C" works.

I am trying to use the Mini-Tutorial (ACSL Mini-Tutorial) to get into
the matter and to see if I installed the software correctly.
The first example is working with no error msg's.

But when I come to the second one I get  a Syntax error from frama-c
.. it compiles without any error wit the GCC comoiler.


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

after checking the file .. I see that it is the line
" /*@ requires n > 0 && \valid(p+(0..n-1)); "
and to be exact it is the chars " n-1 " in the term "\valid(p+(0..n-1));"
-------------------------
#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!

I hope I made it clear enough ;) .. forgive the mistakes.

Good day to you
Munir