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

[Frama-c-discuss] Unable to ensure null



Hello,

Le 30/05/2014 17:56, Ian Blissard a ?crit :
> I have come across a situation where I cannot ensure that a pointer will
> be null, and I am unsure what I am doing incorrectly.

You are using the wrong memory model of WP. Using Typed+cast, everything 
is proved.

I used following command line:
  frama-c -pp-annot -cpp-command="gcc -nostdinc -C -E -I. -I`frama-c 
-print-share-path`/libc" -wp -wp-rte -wp-model Typed+cast null_pointer.c

Two points still unclear to me:
  * Why is this memory model working? I don't know. WP documentation 
should help you.

  * There is still a warning and I don't know if it is dangerous or not:
"""
null_pointer.c:12:[wp] warning: Cast with incompatible pointers types 
(source: sint8*) (target: sint32*)
null_pointer.c:15:[wp] warning: Cast with incompatible pointers types 
(source: sint8*) (target: sint32*)
"""

Best regards,
david