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?

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