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