Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why does value analysis determine this to be invalid?

Hello,

There are two things at work here. First, Value generates an initial
analysis state that depends on many things (section 5.2 of the
manual). Here, a suitable value for the formal parameter ptr must be
generated. Since uintptr_t is actually a scalar integer type, Value
generates the range [--..--], that is all possible numerical values
that fit inside sizeof(uintptr_t). Then, the operation ptr &
(uintptr_t)~1 results in an imprecise range [0..4294967294]. All those
addresses are invalid if you do not use option -absolute-valid-range
(which specifies which numeric range are valid addresses), and your
precondition cannot hold.

Alternatively, if you want ptr to be "a" real address, you should use
void* instead of uintptr_t. In this case, Value will generate a fresh
base for ptr.

On Thu, May 1, 2014 at 9:50 PM, Marko Sch?tz Schmuck
<MarkoSchuetz at web.de> wrote:
> Dear All,
>
> with the following source code
>
> #include <stdint.h>
>
> /*@
>   @ requires \valid((int *)(ptr & (uintptr_t)~1));
>   @ */
>
> void func(uintptr_t ptr) {
>   int i;
>   i = *(int *)(ptr & (uintptr_t)~1);
> }
>
> frama-c -val ~/tmp/test2.c -main func
>
> results in
>
> [..]
> ../../tmp/test2.c:4:[value] Function func: precondition got status invalid.
> [..]
>
> I would expect the precondition to be unknown, not invalid.
>
> Am I misunderstanding something here?
>
> Thanks and best regards,
>
> Marko
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss



-- 
Boris