---
layout: fc_discuss_archives
title: Message 75 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)
- Subject: [Frama-c-discuss] Frama-C: Detecting unreachable code? (Dharmalingam Ganesan)
- From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
- Date: Sat, 25 Jan 2014 11:30:57 +0000
- In-reply-to: <mailman.29.1390647739.11169.frama-c-discuss@lists.gforge.inria.fr>
- References: <mailman.29.1390647739.11169.frama-c-discuss@lists.gforge.inria.fr>
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;
}
}