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: mail at allan-blanchard.fr (mail at allan-blanchard.fr)
  • Date: Fri, 19 Jun 2020 09:10:54 +0200 (CEST)
  • In-reply-to: <CAOyGZc5W9=JF9FO8E-Bm+W6Z40pEcNYVzvEmh5gJQA+c0bierA@mail.gmail.com>
  • References: <CAOyGZc5W9=JF9FO8E-Bm+W6Z40pEcNYVzvEmh5gJQA+c0bierA@mail.gmail.com>
Dear Cyril, 

It seems that either an hypothesis or a lemma is missing to verify the property automatically, we should have a closer look to this, thank you for the report. 
WP strategies can help to finish the proof but it is not that easy to apply directly on the goal, so here is a workaround. 

Add a lemma : 

/*@ lemma u16_and_is_u16: 
\forall unsigned short s, m ; 0 <= (s & m) <= USHRT_MAX ; 
*/ 

which is enough to verify all assertions in your example. 
However, the lemma will not be directly proved automatically, you can either terminate the proof via the TIP or via automatic strategies. 

To use TIP, just double click on the lemma in the "WP Goals" view of the GUI, then select the goal to prove and apply the tactic "Split & Bit Range(s)" on the right. 
To use automatic strategies, add "-wp-auto wp:split,wp:bitrange" to the command line, however, it can require some time to be applied. 

In order to maximize automation without increasing (too much) the verification time, you should probably exclude the proof of the lemmas in most of the verification process (using "-wp-prop=- at lemma") and then finish the remaining goals using more expensive features. 
For example: 

frama-c files.c... -eva ... -then -wp -wp-prop="- at lemma" ... -then -wp-prop="@lemma" -wp-auto="wp:split,wp:bitrange" 

Best regards, 
Allan B 


De: "Cyril" <cyril.deberge at gmail.com> 
À: "Frama-c-discuss" <frama-c-discuss at lists.gforge.inria.fr> 
Envoyé: Jeudi 18 Juin 2020 20:17:30 
Objet: [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é 

_______________________________________________ 
Frama-c-discuss mailing list 
Frama-c-discuss at lists.gforge.inria.fr 
https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200619/2e7c2210/attachment.html>