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