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