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?

  • Subject: [Frama-c-discuss] why does value analysis determine this to be invalid?
  • From: MarkoSchuetz at web.de (Marko Schütz Schmuck)
  • Date: Thu, 01 May 2014 15:50:56 -0400
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>