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: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Fri, 10 Jan 2020 08:39:28 +0000
  • In-reply-to: <CAP6v9C5LG1Daxn9dz4H2AiV59z3J8=M1Qe-EQgjeX54-5XAWvA@mail.gmail.com>
  • References: <CAP6v9C5LG1Daxn9dz4H2AiV59z3J8=M1Qe-EQgjeX54-5XAWvA@mail.gmail.com>
Hello Benjamin,

with Frama-C 20 under macOS I have the following output.

frama-c -wp -wp-prover=z3 test.c
[kernel] Parsing test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Z3 4.8.6] Goal typed_test_ensures_2 : Timeout (Qed:2ms) (10s) (cached)
[wp] [Z3 4.8.6] Goal typed_test_ensures : Timeout (Qed:2ms) (10s) (cached)
[wp] [Cache] found:2
[wp] Proved goals:    0 / 2
  Z3 4.8.6:        0  (interrupted: 2) (cached: 2)

Does this help you?

Regards

Jens

From: Frama-c-discuss <frama-c-discuss-bounces at lists.gforge.inria.fr> on behalf of Benjamin Nauck <benjamin at nauck.se>
Reply-To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Date: Thursday, 9. January 2020 at 22:47
To: "frama-c-discuss at lists.gforge.inria.fr" <frama-c-discuss at lists.gforge.inria.fr>
Subject: [Frama-c-discuss] Strange results when verifying bitshifts using frama-c v19.1 with z3

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/20200110/5c17d3c7/attachment-0001.html>