--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on April 2014 ---
Hello, 2014-04-21 20:29 GMT+02:00 Marko Sch?tz Schmuck <MarkoSchuetz at web.de>: > //@ requires ptr != \null; Just as a side note, this pre-condition does not indicate that ptr is a valid pointer to int. You would need requires \valid((int*)ptr); > 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? > Yes, conversion from an integral type to a pointer type is legal in C (albeit implementation-defined). The message from WP merely says "I don't know how to represent that in my memory model" > What is the recommended way to deal with code that uses these casts? > As far as I know, there is currently no WP memory model that can handle such casts. On the other hand, Value Analysis, which has a much more low-level memory model, will conclude that the pre-condition is satisfied at the call site. Best regards, -- E tutto per oggi, a la prossima volta Virgile