--- layout: fc_discuss_archives title: Message 28 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?



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