--- layout: fc_discuss_archives title: Message 90 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)



Hi,

I can help with testing, if needed. In fact, I have used other static analysis tools and some of them detected such types of issues. If WP will have such features, I will be able to test it on the same code base for known issues, at least.

Best regards,
Dharma



From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Lo?c Correnson
Sent: Monday, January 27, 2014 5:30 AM
To: Frama-C public discussion
Subject: Re: [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<mailto: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> [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<mailto: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<mailto:Frama-c-discuss at lists.gforge.inria.fr>
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss<http://cp.mcafee.com/d/k-Kr3x0g3x0SyOqerL8L6zAQsLCXCQXL8LccfEFCQXL8LccfKcCQXL8LccfEI6QXL9KnojujdE4txZdw2Dr5RkerlgXQ6PrJyWG7dGEtW3pJdxZBPQT-LObzOqabDnKnjjjsVdNd-Wb7bnhIyyHt5zBgY-F6lK1FJ4SCrLOtXTLuZXTdTdw0PVkDjybE07-B2cJVSe08n8ixwCHIcfBisEeRNSeGWnIngBiPta6ToWHFuNt2lbdQEn8lrxrW0E-l9QUyW01_Fgzbutyrhhov76MnWhEwdboL7ltbSbEiFpKB3iWq81ueGWn4Azh07vfXjB0yq86Uh_r4Z87-q8blgYAq83hg74ZyHFYE4tld40iS7QS1EFdTdUr1hdrZx6Sj>

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