--- layout: fc_discuss_archives title: Message 80 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?



I looked at the code generated by RTE. I wonder why it casts unsigned int into int types? Is it a bug in RTE?


[formal_verification]$ frama-c -rte sign.c -lib-entry -print
[kernel] preprocessing with "gcc -C -E -I.  sign.c"
[rte] annotating function sign
/* Generated by Frama-C */
typedef unsigned short uint16;
/*@ behavior neg:
      assumes i < 0;
      ensures \false;
    
    behavior pos:
      assumes i > 0;
      ensures \result ? 1;
    
    behavior zero:
      assumes i ? 0;
      ensures \result ? 0;
 */
int sign(uint16 i)
{
  int __retres;
  if ((int)i < 0) {
    __retres = -1;
    goto return_label;
  }
  if ((int)i == 0) {
    __retres = 0;
    goto return_label;
  }
  __retres = 1;
  return_label: /* internal */ return __retres;
}


________________________________________
From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Virgile Prevosto [virgile.prevosto at m4x.org]
Sent: Saturday, January 25, 2014 1:00 PM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] Frama-C: Detecting unreachable code?

Hello,

Le ven. 24 janv. 2014 14:05:14 CET,
Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit :

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

> typedef unsigned short int uint16;
>
> /*@
>  behavior neg:
>    assumes i < 0;
>    ensures \result == -1;
...
> */
> int sign(uint16 i)

WP indeed will happily prove the behavior valid. In fact, it is meant
to prove that if the function is called in a state that satisfies the
assumes then the state at the end of execution will be satisfy the
ensures. Thus, if the assumes clause is always false, the proof is
trivial: ex falso, quod libet...
In order to detect such erroneous assumes, you might replace the
ensures clause by ensures \false: if WP is still able to prove it,
something fishy is going on, either in the spec or in the code.

Best regards,
--
E tutto per oggi, a la prossima volta.
Virgile


_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/2DRPoOd38srhpd7dT1OrOq9KVJeXObP33WapJeXObP33Xz9JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSrp847mvjvW_8T76zB4seWZOW9EVpsV5MQszAn4-mKzp5dl557BgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYGjFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdLEL9CMnWhEwdboL7ltbSbEiFpKB3iWq81ueGWn4Azh07vfXjB0yq86Uh_r4Z87-q8blgYArKrk4k4