--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on May 2012 ---
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.