--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on October 2013 ---
[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>