--- layout: fc_discuss_archives title: Message 54 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'm wondering whether Frama-C can report unreachable code without any annotation, for example, see the below code?


int i = 0;

int main()
{
  if (0 <= i  && i <= 10)
  {
     return -1;
  }

  if (i == 5) 
  {
     /* can never reach here? */
     return -2;
  }

  return 0;
}

________________________________________
From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of David MENTRE [dmentre at linux-france.org]
Sent: Friday, January 17, 2014 2:34 AM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] Frama-c: WP issues

Hello Dharmalingam,

Le 16/01/2014 19:09, Dharmalingam Ganesan a ?crit :
> I just got an email that this issue is fixed. I'm very curious to try
> but do not know where to pull the source code of the updated
> version?

You cannot. CEA's code repository is closed. You'll have to wait next
official release (like me).

Best regards,
david

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/5fHCNASyOYqejhOMNtYsrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCTDr8f89LZvC7676kuLsKyYCeUsqem4n4-mKzp55mWr7axVZicHs3jq9J4TvAm4TDNOb2pEVdTdw0PVkDjybE07-B2cJVSe08n8ixwCHIcfBisEeRNSeGWnIngBiPta6ToWHFuNt2lbdQEn8lrxrW0E-l9QUyW01_Fgzbutyrpd7bb1I5-Aq83iSbNRniZyW4GmrFgQKCy0nzGKBX96y01gIq89kETZ3tPsUB8bl8SVXsx