--- layout: fc_discuss_archives title: Message 83 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?



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.