--- layout: fc_discuss_archives title: Message 83 from Frama-C-discuss on January 2014 ---
Yes, I refer "Integer Promotion" for my course at UMD. I was thinking of using Frama-C for my course to demonstrate some examples. For this below function, the value plugin says the [value] Values at end of function myFun: i ? [--..--] In my understanding [--, --] refers to all possible integers. But, the value of i for this function can never be below zero. --- unsigned int i = 0; void myFun() { i++; } -- [formal_verification]$ frama-c -val unint.c -main myFun -lib-entry [kernel] preprocessing with "gcc -C -E -I. unint.c" [value] Analyzing an incomplete application starting at myFun [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization i ? [--..--] unint.c:5:[value] assigning non deterministic value for the first time [value] Recording results for myFun [value] done for function myFun [value] ====== VALUES COMPUTED ====== [value] Values at end of function myFun: i ? [--..--] ________________________________________ From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pascal Cuoq [pascal.cuoq at gmail.com] Sent: Saturday, January 25, 2014 3:00 PM To: Frama-C public discussion Subject: Re: [Frama-c-discuss] Frama-C: Detecting unreachable code? On Sat, Jan 25, 2014 at 8:47 PM, Dharmalingam Ganesan <dganesan at fc-md.umd.edu<mailto:dganesan at fc-md.umd.edu>> wrote: I looked at the code generated by RTE. I wonder why it casts unsigned int into int types? Because this is how the C language works Please see http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf<http://cp.mcafee.com/d/1jWVIe6x8e6jqb9EVKUZuX3VKVJeXObP33WapJeXObP33Xz9JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSr8uehoZd_HYyCOejd7b_nKnjpuvV4QsFzHKfYJt6OaqJXEYG7DR8OJMddECQjt-jpspspspsodTdw0GHv0Liq700s4pShOBAQYc4kmcaoxmRcwy-eLOO3FJSeGWnIngBiPta5O5mUm-wafBite8Kw0vWk8OTDoCT1P3NI5-Aq83iSbNRniZyW4GmrFgQKCy0nzGKBN98Qg1TP-QVg8Cy1K4vSNfi1_Cy2Rkf96XCYL4R> , especially ?integer promotions? in section 6.3. Is it a bug in RTE? No.