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] cast to prove an assertion

  • Subject: [Frama-c-discuss] cast to prove an assertion
  • From: cyril.deberge at gmail.com (Cyril)
  • Date: Thu, 18 Jun 2020 20:17:30 +0200
Dear list,

I'm currently working with FramaC 20.0 (calcium version), and i'm using EVA
and WP plugins. I've got a problem with this code:

if( ( ( (pkt->wIndex) & 0xff ) ) == 0 ){
        /*@ assert ((pkt->wIndex) & 0xff) == 0 ; */
        errcode = MBED_ERROR_INVPARAM ;
        goto err ;
    }

    /*@ assert ((pkt->wIndex) & 0xff) != 0 ; */
    /*@ assert ((pkt->wIndex) & 0xff) > 0 ; */

with pkt->wIndex as a uint16_t

I'm trying to help WP with assertions.

/*@ assert ((pkt->wIndex) & 0xff) == 0 ; */ is ok for EVA.
 /*@ assert ((pkt->wIndex) & 0xff) != 0 ; */ is ok for WP

but /*@ assert ((pkt->wIndex) & 0xff) > 0 ; */ remained unknown (either EVA
or WP), even if EVA knows that (pkt->wIndex) >0 after if statement.
I don't understand why WP cannot prove that ((pkt->wIndex) & 0xff) > 0.

I finally managed to prove this assertion by casting (pkt->wIndex) & 0xff
as an uint8_t :
if(((uint8_t)((pkt->wIndex) & 0xff)) == 0 )
(since & 0xff is a mask)

As options for WP and EVA, i'm using :
 -eva-warn-undefined-pointer-comparison none
   -eva-auto-loop-unroll 20
   -eva-slevel 300
   -eva-symbolic-locations-domain
   -eva-equality-domain
  -wp-dynamic
   -eva-split-return auto
   -eva-partition-history 6
  -wp-model "Typed+ref+int"
  -wp-literals
  -wp-prover alt-ergo,cvc4,z3

And finally for the provers, i'm using : alt-ergo 2.3.0, cvc4 1.7 et z3
4.8.6

So is this a normal behavior for FramaC?

Thank you for your answer,

Cyril Debergé
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200618/33c31c18/attachment.html>