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



Le 04/05/2012 09:50, Anne Pacalet a ?crit :
> 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)
>
>    
hi Anne

Perhaps try to use this option :

-absolute-valid-range 0xABCD-0xB000

with the correct range ;)

-- 
jean-marc Harang