--- layout: fc_discuss_archives title: Message 73 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C: Detecting unreachable code?



Hi,

I tried the same below example with the value plugin (frama-c -val sign.c -lib-entry -main sign) it seems to be correct. 

sign.c:6:[value] Function sign, behavior neg: assumes got status invalid; postcondition not evaluated
...

[value] ====== VALUES COMPUTED ======
[value] Values at end of function sign:
          __retres ? {0; 1}

But, not the WP plugin nor the jessie plugin. 

________________________________________
From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Dharmalingam Ganesan [dganesan at fc-md.umd.edu]
Sent: Friday, January 24, 2014 2:05 PM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] Frama-C: Detecting unreachable code?

Hi,

I'm not sure how unsigned types are handled by Frama-c. Bit confused why the following code worked for the "neg" behavior,

I was hoping that the tool will report an invalid comparison between unsigned int with < 0, or something like that, but the "neg" contract worked.


Am I using it in an incorrect way?


frama-c -wp -wp-rte sign.c -lib-entry




typedef unsigned short int uint16;

/*@
 behavior neg:
   assumes i < 0;
   ensures \result == -1;

 behavior pos:
   assumes i > 0;
   ensures \result == 1;

 behavior zero:
   assumes i == 0;
   ensures \result == 0;
*/
int sign(uint16 i)
{
   if(i < 0)
   {
     /* should never reach here - unsigned i */
     return -1;
   }

   if (i == 0)
   {
     return 0;
   }

   return 1;
}

________________________________________
From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Lo?c Correnson [loic.correnson at cea.fr]
Sent: Friday, January 24, 2014 10:33 AM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] Frama-C: Detecting unreachable code?

Your spec is wrong. Result is always (-1) even when i == 5 (which actually only occurs in lib-entry mode, otherwise i == 0).
And there is no RTE to check, as it can be confirmed by value.
        L.

Le 24 janv. 2014 ? 03:36, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit :

> Hi,
>
> Thanks for all responses. I'm not sure why the following code cannot considered invalid; I always get "unknown".
>
> Any comments?
>
> frama-c -wp -wp-rte non_sense.c -lib-entry
>
>
>
> int i = 0;
>
> /*@
>  @ behavior BUG:
>  @  assumes i == 5;
>  @  ensures \result == -2;
> */
>
> int main()
> {
>  if (0 <= i  && i <= 10)
>  {
>     return -1;
>  }
>
>  if (i == 5)
>  {
>     return -2;
>  }
>
>  return 0;
> }
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://cp.mcafee.com/d/5fHCN8e410edEICzCXUUsU-CrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCSnhPOvFLZvC4kQm3hPRXBQQXIYU-UCCeVqWdAklkrFYG7DR8OJMddECQPt-hojuv78I9CzATsS03fBite8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JZBxUS2_id41Fr5UWHFuNt2lbdQEqnjh0bNRniUAAq80XV_qsE4jh0T2fXoDF0_Ph1qG7AztPvrzzByW5


_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/1jWVIpdEICzCXUUsU-CrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCSnhPOvFLZvC4kQm3hPRXBQQXIYU-UCCeVqWdAklkrFYG7DR8OJMddFCQPt-hojuv78I9CzATsS03fBite8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JZBxUS2_id41Fr5UWHFuNt2lbdQEqnjh0bNRniUAAq80XV_qsE4jh0T2fXoDF0_Ph1qG7AztPsoz7-Nir

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/k-Kr3wUpdEICzCXVEVK-yyrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCQ4Z89-C_R-vsd7bbMXHTbFFK9YqemnS3hOPORQr8EGTuhVkffGhBrwqrhdICXYyMCY-ehojd79KVI06vaAWsht00_QEhBLeNM12V2kc4RtxxYGjB1SKeNRniZyW4GmrFgSX7ltbSbEiFpKB2V2Hsbvg57OFeD4ng0fZa4prPIjoVZYQsCMnWhEwdboL7ltbSbEiFpKB3iWq81ueGWn4Azh07vfXjB0yq86Uh_r4Z87-q8blgYArKrZZ8N-eT