--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Valid physical address



Hello,

I am trying to use frama-c value analysis on an application
that reads the memory using some physical addresses.
Something like :

unsigned char * p = 0xABCD;
if (*(p + 10) == 1) {
 ...
}

Of course, the value analysis emit an alarm : assert \valid(p+10);
Status: **NOT** VALID according to value analysis (under hypotheses)

The problem is that the test is then considered to be always false
ie. the if branch is said to be dead code.
I don't really understand why...
Is there a way to tell the value analysis to consider the test
to be either true or false ?

Thanks in advance for your help,
-- 
Anne.