Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Frama-C: Detecting unreachable code?
- Subject: [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- Date: Fri, 24 Jan 2014 14:05:14 -0500
- In-reply-to: <0B8A5A42-5BB3-4C9C-99A6-A07AC39A84AB@cea.fr>
- References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449A7@Mail1.FCMD.local> <52E0C26F.2000605@linux-france.org> <20140123082550.GA7256@opentech.at> <CAOH62JhyfqOmKmw5iKjx1CSifK2X6ajxZBxd--h4_nK-3OxmrA@mail.gmail.com> <52E0D85C.3060504@cea.fr>, <CAOH62Jj=TOozP8yxRV7-ECSUknpVhe6_eeMwPuQGOJTYJD+5fg@mail.gmail.com> <B517F47C2F6D914AA8121201F9EBEE6701C7660449A8@Mail1.FCMD.local>, <0B8A5A42-5BB3-4C9C-99A6-A07AC39A84AB@cea.fr>
Hi, I'm not sure how unsigned types are handled by Frama-c. Bit confused why the following code worked for the "neg" behavior, I was hoping that the tool will report an invalid comparison between unsigned int with < 0, or something like that, but the "neg" contract worked. Am I using it in an incorrect way? frama-c -wp -wp-rte sign.c -lib-entry typedef unsigned short int uint16; /*@ behavior neg: assumes i < 0; ensures \result == -1; behavior pos: assumes i > 0; ensures \result == 1; behavior zero: assumes i == 0; ensures \result == 0; */ int sign(uint16 i) { if(i < 0) { /* should never reach here - unsigned i */ return -1; } if (i == 0) { return 0; } return 1; } ________________________________________ From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Lo?c Correnson [loic.correnson at cea.fr] Sent: Friday, January 24, 2014 10:33 AM To: Frama-C public discussion Subject: Re: [Frama-c-discuss] Frama-C: Detecting unreachable code? Your spec is wrong. Result is always (-1) even when i == 5 (which actually only occurs in lib-entry mode, otherwise i == 0). And there is no RTE to check, as it can be confirmed by value. L. Le 24 janv. 2014 ? 03:36, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit : > Hi, > > Thanks for all responses. I'm not sure why the following code cannot considered invalid; I always get "unknown". > > Any comments? > > frama-c -wp -wp-rte non_sense.c -lib-entry > > > > int i = 0; > > /*@ > @ behavior BUG: > @ assumes i == 5; > @ ensures \result == -2; > */ > > int main() > { > if (0 <= i && i <= 10) > { > return -1; > } > > if (i == 5) > { > return -2; > } > > return 0; > } > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://cp.mcafee.com/d/5fHCN8e410edEICzCXUUsU-CrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCSnhPOvFLZvC4kQm3hPRXBQQXIYU-UCCeVqWdAklkrFYG7DR8OJMddECQPt-hojuv78I9CzATsS03fBite8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JZBxUS2_id41Fr5UWHFuNt2lbdQEqnjh0bNRniUAAq80XV_qsE4jh0T2fXoDF0_Ph1qG7AztPvrzzByW5 _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://cp.mcafee.com/d/1jWVIpdEICzCXUUsU-CrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCSnhPOvFLZvC4kQm3hPRXBQQXIYU-UCCeVqWdAklkrFYG7DR8OJMddFCQPt-hojuv78I9CzATsS03fBite8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JZBxUS2_id41Fr5UWHFuNt2lbdQEqnjh0bNRniUAAq80XV_qsE4jh0T2fXoDF0_Ph1qG7AztPsoz7-Nir
- Follow-Ups:
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- References:
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: der.herr at hofr.at (Nicholas Mc Guire)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: nicky.williams at cea.fr (Nicky Williams)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- From: loic.correnson at cea.fr (Loïc Correnson)
- [Frama-c-discuss] Frama-C: Detecting unreachable code?
- Prev by Date: [Frama-c-discuss] Frama-C: Detecting unreachable code?
- Next by Date: [Frama-c-discuss] Frama-C: Detecting unreachable code?
- Previous by thread: [Frama-c-discuss] Frama-C: Detecting unreachable code?
- Next by thread: [Frama-c-discuss] Frama-C: Detecting unreachable code?
- Index(es):