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] Strange results when verifying bitshifts using frama-c v19.1 with z3

  • Subject: [Frama-c-discuss] Strange results when verifying bitshifts using frama-c v19.1 with z3
  • From: benjamin at nauck.se (Benjamin Nauck)
  • Date: Thu, 9 Jan 2020 22:47:11 +0100
Hi,
I know v20 is out and I should probably update but I've got some questions
about the behaviour of v19.1 that I would like to have the answer to.

The problem is that I get some strange result when using frama-c v19.1 with
why3 v1.2.1 and z3 v4.8.6 (running on macos 10.14.1).
It seems to starts when I have bit shift in the code I'm trying to verify,
as seen in the following example:

$ cat test.c
//@ ensures \result == 0; ensures \result != 0;
unsigned test(unsigned value) {
    return value >> 1;
}
$ frama-c -wp -wp-prover=z3 test.c
[kernel] Parsing test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] Proved goals:    2 / 2
  Qed:             0  (0.38ms-0.82ms)
  Z3:              2  (140ms)

1. Maybe I'm missing something, but to me, \result should neither be always
0 nor never 0 and it should especially not be both at the same time, right?

2. Any idea what could be causing this?

3. Is there a way to read the output of why3 and z3 to try to debug what is
happening without diving into the source code of frama-c or the
configuration files of why3?

I've put off upgrading to v20 as I need to verify quite a lot of bit
manipulation of integers and I've got the impression that the new version
is a bit buggy when it comes to that (even though workarounds seems to
exist).
4. Should I upgrade to v20 anyway or am I better off with 19.1 for that?

Regards,
Benjamin Nauck
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200109/cb93477b/attachment.html>