--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] preprocessor problems with jessie



Hi,

I'm trying to use Frama-C with Jessie on a 64-bit Ubuntu 13.10 machine 
with these packages installed from source:

frama-c-Fluorine-20130601
why-2.33
why3-0.81

I'm simply trying to verify an example code (below, I believe it is 
straight from the web) but Frama-C is dying with a large amount of 
preprocessor problems as shown in the attached file.  A web search on 
the actual error line didn't return anything useful so I wanted to check 
here if this is a known problem that I might be able to correct?

Thanks,

John Regehr





#pragma JessieIntegerModel(strict)

/*@ predicate Sorted{L}(int *a, integer l, integer h) =
   @   \forall integer i,j; l <= i <= j < h ==> a[i] <= a[j] ;
   @*/

/*@ requires \valid_range(t,0,n-1);
   @ ensures Sorted(t,0,n-1);
   @*/
void insert_sort(int t[], int n) {
   int i,j;
   int mv;
   if (n <= 1) return;
   /*@ loop invariant 0 <= i <= n;
     @ loop invariant Sorted(t,0,i);
     @ loop variant n-i;
     @*/
   for (i=1; i<n; i++) {
     // assuming t[0..i-1] is sorted, insert t[i] at the right place
     mv = t[i];
     /*@ loop invariant 0 <= j <= i;
       @ loop invariant j == i ==> Sorted(t,0,i);
       @ loop invariant j < i ==> Sorted(t,0,i+1);
       @ loop invariant \forall integer k; j <= k < i ==> t[k] > mv;
       @ loop variant j;#pragma JessieIntegerModel(strict)

/*@ predicate Sorted{L}(int *a, integer l, integer h) =
   @   \forall integer i,j; l <= i <= j < h ==> a[i] <= a[j] ;
   @*/

/*@ requires \valid_range(t,0,n-1);
   @ ensures Sorted(t,0,n-1);
   @*/
void insert_sort(int t[], int n) {
   int i,j;
   int mv;
   if (n <= 1) return;
   /*@ loop invariant 0 <= i <= n;
     @ loop invariant Sorted(t,0,i);
     @ loop variant n-i;
     @*/
   for (i=1; i<n; i++) {
     // assuming t[0..i-1] is sorted, insert t[i] at the right place
     mv = t[i];
     /*@ loop invariant 0 <= j <= i;
       @ loop invariant j == i ==> Sorted(t,0,i);
       @ loop invariant j < i ==> Sorted(t,0,i+1);
       @ loop invariant \forall integer k; j <= k < i ==> t[k] > mv;
       @ loop variant j;
       @*/
     // look for the right index j to put t[i]
     for (j=i; j > 0; j--) {
       if (t[j-1] <= mv) break;
       t[j] = t[j-1];
     }
     t[j] = mv;
   }
}


/*
Local Variables:
compile-command: "frama-c -jessie insertion_sort.c"
End:
*/

       @*/
     // look for the right index j to put t[i]
     for (j=i; j > 0; j--) {
       if (t[j-1] <= mv) break;
       t[j] = t[j-1];
     }
     t[j] = mv;
   }
}


/*
Local Variables:
compile-command: "frama-c -jessie insertion_sort.c"
End:
*/
-------------- next part --------------
[kernel] preprocessing with "gcc -C -E -I.  -dD insertion_sort.c"
/tmp/ppannot45f6d8.c:235:0: warning: "__STDC_IEC_559__" redefined [enabled by default]
 #define __STDC_IEC_559__ 1
 ^
In file included from /usr/include/stdc-predef.h:30:0,
                 from <command-line>:0:
/usr/include/x86_64-linux-gnu/bits/predefs.h:27:0: note: this is the location of the previous definition
 #define __STDC_IEC_559__  1
 ^
/tmp/ppannot45f6d8.c:236:0: warning: "__STDC_IEC_559_COMPLEX__" redefined [enabled by default]
 #define __STDC_IEC_559_COMPLEX__ 1
 ^
In file included from /usr/include/stdc-predef.h:30:0,
                 from <command-line>:0:
/usr/include/x86_64-linux-gnu/bits/predefs.h:28:0: note: this is the location of the previous definition
 #define __STDC_IEC_559_COMPLEX__ 1
 ^
/tmp/ppannot45f6d8.c:237:0: warning: "__STDC_ISO_10646__" redefined [enabled by default]
 #define __STDC_ISO_10646__ 201103L
 ^
In file included from <command-line>:0:0:
/usr/include/stdc-predef.h:34:0: note: this is the location of the previous definition
 #define __STDC_ISO_10646__  201103L
 ^
/tmp/ppannot45f6d8.c:238:0: warning: "__STDC_NO_THREADS__" redefined [enabled by default]
 #define __STDC_NO_THREADS__ 1
 ^
In file included from <command-line>:0:0:
/usr/include/stdc-predef.h:37:0: note: this is the location of the previous definition
 #define __STDC_NO_THREADS__  1
 ^
/tmp/ppannot27d69b.c:235:0: warning: "__STDC_IEC_559__" redefined [enabled by default]
 #define __STDC_IEC_559__ 1
 ^
In file included from /usr/include/stdc-predef.h:30:0,
                 from <command-line>:0:
/usr/include/x86_64-linux-gnu/bits/predefs.h:27:0: note: this is the location of the previous definition
 #define __STDC_IEC_559__  1
 ^
/tmp/ppannot27d69b.c:236:0: warning: "__STDC_IEC_559_COMPLEX__" redefined [enabled by default]
 #define __STDC_IEC_559_COMPLEX__ 1
 ^
In file included from /usr/include/stdc-predef.h:30:0,
                 from <command-line>:0:
/usr/include/x86_64-linux-gnu/bits/predefs.h:28:0: note: this is the location of the previous definition
 #define __STDC_IEC_559_COMPLEX__ 1
 ^
/tmp/ppannot27d69b.c:237:0: warning: "__STDC_ISO_10646__" redefined [enabled by default]
 #define __STDC_ISO_10646__ 201103L
 ^
In file included from <command-line>:0:0:
/usr/include/stdc-predef.h:34:0: note: this is the location of the previous definition
 #define __STDC_ISO_10646__  201103L
 ^
/tmp/ppannot27d69b.c:238:0: warning: "__STDC_NO_THREADS__" redefined [enabled by default]
 #define __STDC_NO_THREADS__ 1
 ^
In file included from <command-line>:0:0:
/usr/include/stdc-predef.h:37:0: note: this is the location of the previous definition
 #define __STDC_NO_THREADS__  1
 ^
/tmp/ppannotfa0ad4.c:235:0: warning: "__STDC_IEC_559__" redefined [enabled by default]
 #define __STDC_IEC_559__ 1
 ^
In file included from /usr/include/stdc-predef.h:30:0,
                 from <command-line>:0:
/usr/include/x86_64-linux-gnu/bits/predefs.h:27:0: note: this is the location of the previous definition
 #define __STDC_IEC_559__  1
 ^
/tmp/ppannotfa0ad4.c:236:0: warning: "__STDC_IEC_559_COMPLEX__" redefined [enabled by default]
 #define __STDC_IEC_559_COMPLEX__ 1
 ^
In file included from /usr/include/stdc-predef.h:30:0,
                 from <command-line>:0:
/usr/include/x86_64-linux-gnu/bits/predefs.h:28:0: note: this is the location of the previous definition
 #define __STDC_IEC_559_COMPLEX__ 1
 ^
/tmp/ppannotfa0ad4.c:237:0: warning: "__STDC_ISO_10646__" redefined [enabled by default]
 #define __STDC_ISO_10646__ 201103L
 ^
In file included from <command-line>:0:0:
/usr/include/stdc-predef.h:34:0: note: this is the location of the previous definition
 #define __STDC_ISO_10646__  201103L
 ^
/tmp/ppannotfa0ad4.c:238:0: warning: "__STDC_NO_THREADS__" redefined [enabled by default]
 #define __STDC_NO_THREADS__ 1
 ^
In file included from <command-line>:0:0:
/usr/include/stdc-predef.h:37:0: note: this is the location of the previous definition
 #define __STDC_NO_THREADS__  1
 ^
/tmp/ppannotca0e72.c:235:0: warning: "__STDC_IEC_559__" redefined [enabled by default]
 #define __STDC_IEC_559__ 1
 ^
In file included from /usr/include/stdc-predef.h:30:0,
                 from <command-line>:0:
/usr/include/x86_64-linux-gnu/bits/predefs.h:27:0: note: this is the location of the previous definition
 #define __STDC_IEC_559__  1
 ^
/tmp/ppannotca0e72.c:236:0: warning: "__STDC_IEC_559_COMPLEX__" redefined [enabled by default]
 #define __STDC_IEC_559_COMPLEX__ 1
 ^
In file included from /usr/include/stdc-predef.h:30:0,
                 from <command-line>:0:
/usr/include/x86_64-linux-gnu/bits/predefs.h:28:0: note: this is the location of the previous definition
 #define __STDC_IEC_559_COMPLEX__ 1
 ^
/tmp/ppannotca0e72.c:237:0: warning: "__STDC_ISO_10646__" redefined [enabled by default]
 #define __STDC_ISO_10646__ 201103L
 ^
In file included from <command-line>:0:0:
/usr/include/stdc-predef.h:34:0: note: this is the location of the previous definition
 #define __STDC_ISO_10646__  201103L
 ^
/tmp/ppannotca0e72.c:238:0: warning: "__STDC_NO_THREADS__" redefined [enabled by default]
 #define __STDC_NO_THREADS__ 1
 ^
In file included from <command-line>:0:0:
/usr/include/stdc-predef.h:37:0: note: this is the location of the previous definition
 #define __STDC_NO_THREADS__  1
 ^
/usr/include/stdc-predef.h:1:[kernel] user error: unexpected token '/'
[kernel] user error: skipping file "insertion_sort.c" that has errors.
[kernel] Frama-C aborted: invalid user input.