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] preprocessor problems with jessie

  • Subject: [Frama-c-discuss] preprocessor problems with jessie
  • From: regehr at cs.utah.edu (John Regehr)
  • Date: Wed, 06 Nov 2013 21:49:41 -0700
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.