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] 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