--- layout: fc_discuss_archives title: Message 88 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? (Dharmalingam Ganesan)



You are absolutely right.
It is clear that Frama-C lacks from smoke detectors. I?ve read and heard many interesting works on this subject, and it would be surely a good idea to implement some of them. Just need to find some manpower around? ;-)
L.

Le 25 janv. 2014 ? 16:27, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit :

> Hi,
> 
> Yes, it does satisfy the contract. However, if there is a conditional statement which is always true then it is good to get feedback on that. It is a programming error most likely...
> 
> Best regards,
> Dharma
> 
> -----Original Message-----
> From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Gerlach, Jens
> Sent: Saturday, January 25, 2014 6:31 AM
> To: Discussion Discussion
> Subject: Re: [Frama-c-discuss] Frama-C: Detecting unreachable code? (Dharmalingam Ganesan)
> 
> Hello Dharma,
> 
> I think your function satisfies its contract.
> So, what shall Frama-C do?
> 
> Maybe, your issue is that the function also satisfies the following simpler contract?
> 
> Jens
> 
> int MAX_VALUE = 100;
> 
> float x = 0.0;
> 
> int status = 0;
> 
> /*@
>  requires MAX_VALUE == 100;
>  assigns status;
>  ensures status == -1;
> */
> int main()
> {
> 
>  if((x > MAX_VALUE) ||
>     (x <= MAX_VALUE))
>  {
>     status = -1;
>  }
> }
> 
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://cp.mcafee.com/d/FZsS920s96QmjhPtNwQsIfc6XCQXL8LccfEFCQXL8LccfKcCQXL8LccfEI6QXL9KnojujdE4txZdw2Dr5RkerlgXQ6PrJyWG7dGEtW3pIwZvmvjvW_ce3C3hOzRXBQQQQu73C3hOeLORQr8EGTssVkffGhBrwqrhdECXYyMCY-ehojd79KVI06vaAWsht00_QEhBLeNM12V2kc4RtxxYGjB1SKeNRniZyW4GmrFgSX7ltbSbEiFpKB2V2Hsbvg57OFeD4ng0fZa4prPIjr1EVhsdwLQzh0qmNueGWnIngBiPta6BQQg2YtlQK996y0e-vSDa14QgdMz-S9WgfYQgmGxV8Qg6ywe9X5njVg8WGq80BIfFI3hirKrr2ev
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140127/7b1bdbc1/attachment-0001.html>