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

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



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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140501/aed4dc16/attachment.pgp>