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: Claude.Marche at inria.fr (Claude Marche)
  • Date: Thu, 30 Sep 2010 15:10:04 +0200
  • In-reply-to: <1850266265.159315.1285850299240.JavaMail.root@zmbs1.inria.fr>
  • References: <1850266265.159315.1285850299240.JavaMail.root@zmbs1.inria.fr>
On 09/30/2010 02:38 PM, kydeza wrote:
> 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 ?
>    

It is a mistake in the doc, sorry.

Please replace int a[] by int *a in the parameters of Swap, Permut, 
Sorted declarations

Since ACSL-Boron, there is a difference between int[] and int* in the 
logic annotations.

- Claude

> 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 ---------------
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss


-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |