--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on June 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] cast to prove an assertion



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>