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] 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