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] math vs. bits

Hi,

The main reason is that the support of bitwise operators in Jessie in
very shallow, if any.

I'm surprised that the first function could be proved.

To succeed in proving such kind of code with Jessie, you should probably
provide properties on bitwise operators, under the form of lemmas.

I'm not sure Jessie is the right tool for that, The Value plugin or the
WP plugin might do better.

- Claude

On 11/08/2013 04:25 AM, John Regehr wrote:
> The functions below have identical specifications and are functionally
> equivalent.  All provers (Z3, Yices, CVC4) were able to verify all VCs
> for the first one, yet the second had a number of VCs that no prover
> could discharge.
> 
> I'm curious if this might be some sort of bug in Jessie or Frama-C, or
> are our provers just weak at dealing with bits?
> 
> My goal today was to verify some rotate-by-n functions but that turned
> out to be unexpectedly ambitious so I'm trying rotate-by-1 first.
> 
> John
> 
> 
> 
> /*@
>   @ ensures x <= INT32_MAX ==> \result == 2 * x ;
>   @ ensures x > INT32_MAX ==> \result == 2 * x - UINT32_MAX;
>   @ */
> uint32_t rotate_left_1_a (uint32_t x)
> {
>   return (x << 1) + (x >> 31);
> }
> 
> /*@
>   @ ensures x <= INT32_MAX ==> \result == 2 * x ;
>   @ ensures x > INT32_MAX ==> \result == 2 * x - UINT32_MAX;
>   @ */
> uint32_t rotate_left_1_b (uint32_t x)
> {
>   return (x << 1) | (x >> 31);
> }
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss