--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on November 2013 ---
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.