--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on June 2020 ---
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>