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] frama-c outputs errors in jessie tutorial
- Subject: [Frama-c-discuss] frama-c outputs errors in jessie tutorial
- From: kydeza at gmail.com (kydeza)
- Date: Thu, 30 Sep 2010 14:38:02 +0200
Hello, I am trying frama-c using tutorials provided on the web site frama-c.com, especially the jessie tutorial: http://frama-c.com/jessie_tutorial_index.html and I have a problem with the section 3.2 ?Advanced Algebraic Modeling? frama-c outputs errors when it analyses ACSL specifications, here is the output: prompt> frama-c -jessie sorting.c [kernel] preprocessing with "gcc -C -E -I. -dD sorting.c" sorting.c:7:[kernel] user error: Error during annotations analysis: invalid implicit conversion from int * to int [] [kernel] user error: skipping file "sorting.c" that has errors. [kernel] Frama-C aborted because of an invalid user input. The line 7 is ? @ ensures Swap{Old,Here}(t,i,j); ?, but the type ?int *? is never used in this program. So I do not now what is the problem and how to correct it. Anyone has an idea ? I'm using the version Boron-20100401 Thank you I copy the tutotrial example below (to avoid you to go to see the tutorial: http://frama-c.com/jessie_tutorial_index.html#htoc13): --- sorting.h -------------------- /*@ predicate Swap{L1,L2}(int a[], integer i, integer j) = @ \at(a[i],L1) == \at(a[j],L2) && @ \at(a[j],L1) == \at(a[i],L2) && @ \forall integer k; k != i && k != j @ ==> \at(a[k],L1) == \at(a[k],L2); @*/ /*@ inductive Permut{L1,L2}(int a[], integer l, integer h) { @ case Permut_refl{L}: @ \forall int a[], integer l, h; Permut{L,L}(a, l, h) ; @ case Permut_sym{L1,L2}: @ \forall int a[], integer l, h; @ Permut{L1,L2}(a, l, h) ==> Permut{L2,L1}(a, l, h) ; @ case Permut_trans{L1,L2,L3}: @ \forall int a[], integer l, h; @ Permut{L1,L2}(a, l, h) && Permut{L2,L3}(a, l, h) ==> @ Permut{L1,L3}(a, l, h) ; @ case Permut_swap{L1,L2}: @ \forall int a[], integer l, h, i, j; @ l <= i <= h && l <= j <= h && Swap{L1,L2}(a, i, j) ==> @ Permut{L1,L2}(a, l, h) ; @ } @*/ /*@ predicate Sorted{L}(int a[], integer l, integer h) = @ \forall integer i; l <= i < h ==> a[i] <= a[i+1] ; @*/ -- end sorting.h --------------- --- sorting.c -------------------- #pragma JessieIntegerModel(math) #include "sorting.h" /*@ requires \valid(t+i) && \valid(t+j); @ assigns t[i],t[j]; @ ensures Swap{Old,Here}(t,i,j); @*/ void swap(int t[], int i, int j) { int tmp = t[i]; t[i] = t[j]; t[j] = tmp; } /*@ requires \valid_range(t,0,n?1); @ behavior sorted: @ ensures Sorted(t,0,n?1); @ behavior permutation: @ ensures Permut{Old,Here}(t,0,n?1); @*/ void min_sort(int t[], int n) { int i,j; int mi,mv; if (n <= 0) return; /*@ loop invariant 0 <= i < n; @ for sorted: @ loop invariant @ Sorted(t,0,i) && @ (\forall integer k1, k2 ; @ 0 <= k1 < i <= k2 < n ==> t[k1] <= t[k2]) ; @ for permutation: @ loop invariant Permut{Pre,Here}(t,0,n?1); @ loop variant n?i; @*/ for (i=0; i<n-1; i++) { // look for minimum value among t[i..n?1] mv = t[i]; mi = i; /*@ loop invariant i < j && i <= mi < n; @ for sorted: @ loop invariant @ mv == t[mi] && @ (\forall integer k; i <= k < j ==> t[k] >= mv); @ for permutation: @ loop invariant @ Permut{Pre,Here}(t,0,n?1); @ loop variant n?j; @*/ for (j=i+1; j < n; j++) { if (t[j] < mv) { mi = j ; mv = t[j]; } } swap(t,i,mi); } } -- end sorting.c ---------------
- Follow-Ups:
- [Frama-c-discuss] frama-c outputs errors in jessie tutorial
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- [Frama-c-discuss] frama-c outputs errors in jessie tutorial
- Prev by Date: [Frama-c-discuss] Binary search now works with Alt-Ergo 0.92
- Next by Date: [Frama-c-discuss] make error for "Hello Frama-C World" plugin
- Previous by thread: [Frama-c-discuss] problem with VS project
- Next by thread: [Frama-c-discuss] frama-c outputs errors in jessie tutorial
- Index(es):