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

[Frama-c-discuss] void * and uintptr_t?



Dear All,

I would expect to be able to show that the precondition of func is
satisfied:

#include <stdint.h>

//@ requires ptr != \null;
void func(void *ptr) {
  int i;
  i = *(int *)ptr;
}

int main() {
  void *p;
  int a[1000];
  p = (void *)((uintptr_t)a + 3*sizeof(int));
  func(p);
  return 0;
}

but frama-c complains

Goal func_pre_5: Pre-condition (file test.c, line 3) in 'main' at call 'func' (file test.c, line 13):
test.c:12: warning from Typed Model:
 - Warning: Hide sub-term definition
   Reason: Forbidden cast of int to pointer
Assume { (* Heap *) Have: (linked Malloc_2). }
Prove: p_0!=null.
Prover Alt-Ergo returns Unknown

but shouldn't a cast from uintptr_t to void * be legal?

What is the recommended way to deal with code that uses these casts?

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/20140421/5b5bb1d9/attachment.pgp>