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