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