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