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] z3 failure

On Sun, Oct 6, 2013 at 11:06 PM, Stephen Siegel <siegel at udel.edu> wrote:

> I have a very simple example (below) which I want to verify with frama-c +
> Jessie.  The VCs are discharged easily by Alt-Ergo, CVC3, and CVC4.
>  However they are not discharged by Z3.  This is surprising since Z3 is a
> very powerful prover. [...]
> /*@
>   @ requires n>=0 && \valid(a+(0..n-1)) && \valid(b+(0..n-1)) ;
>   @ ensures \forall integer i ; 0 <= i < n ==> a[i] == b[i] ;
>   @ assigns b[0..n-1] ;
>   @*/
> void copy(int n, double a[], double b[]) {
>   int i = 0;
>
>   /*@
>     @ loop invariant 0<=i<=n;
>     @ loop invariant \forall integer j ; 0<=j<i ==> b[j] == a[j] ;
>     @ loop variant n - i ;
>     @*/
>   while (i < n) {
>     b[i] = a[i];
>     i++;
>   }
> }
>

Do you expect the property to be provable or not? The program below shows
that it does not hold for typical C implementations with IEEE 754
representations for floating-point types:

$ cat d.c
#include <stdio.h>

double a = 0. / 0.;

int main(){
  double b = a;
  printf("%d\n", a == b);
}
$ gcc d.c && ./a.out
0

It would be considered a bug in Jessie if it generates, for the same
program property, a provable obligation for some provers and an unprovable
one for others. I would just like it to be clear whether, with Jessie's
default models regarding aliasing and floating-point, we are looking for an
issue with the Z3 output or with Alt-Ergo, CVC3, and CVC4's.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131007/40a49b8b/attachment.html>