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: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Fri, 10 Jan 2020 09:49:19 +0100
  • In-reply-to: <CAP6v9C5LG1Daxn9dz4H2AiV59z3J8=M1Qe-EQgjeX54-5XAWvA@mail.gmail.com>
  • References: <CAP6v9C5LG1Daxn9dz4H2AiV59z3J8=M1Qe-EQgjeX54-5XAWvA@mail.gmail.com>
Hi,
Actually, there was probably a bug in 19.1 regarding right-shift, which has been fixed in 20.0 ;
Indeed, you shall upgrade to the new version.
Debugging z3 output is not _yet_ available, since we need some extra support from why3 for doing so.
You can however get the prover output with `-wp-msg-key prover` and have the why3 task for each prover logged down with `-wp-out <dir>`.
Regards,
	L.


> Le 9 janv. 2020 à 22:47, Benjamin Nauck <benjamin at nauck.se> a écrit :
> 
> 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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss