--- layout: fc_discuss_archives title: Message 76 from Frama-C-discuss on January 2014 ---
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