--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on December 2013 ---
Hi, Thanks for the hints! The version I am using is Fluorine-20130401, WP 0.7. The wp help manual shows: -wp-model <model+...> Memory model selection. Available selectors: * 'Hoare' logic variables only * 'Typed' typed pointers only * '+nocast' no pointer cast * '+cast' unsafe pointer casts * '+raw' no logic variable * '+ref' by-reference-style pointers detection * '+nat/+cint' natural or machine integers arithmetics * '+real/+float' real or IEEE floatting point arithmetics If I understood it correctly, those are the options. But I am not clear about the difference between +cast and +nocast? Moreover, is the model to be configured in command line this way : $ frama-c -wp wp-model Typed+nocast file.c thanks xiao-lei From: loic.correnson at cea.fr To: frama-c-discuss at lists.gforge.inria.fr Date: Mon, 9 Dec 2013 14:33:53 +0000 Subject: [Frama-c-discuss] RE : [wp] type conversion check is less strict than Jessie? Hi, This is because you are casting a constant int into a pointer, which makes a valid physical address. However, you can not do pointer arithmetics on such values, say, you **can not prove** that (int *) 0x100 shifted by one (on 64-bit machine) leads to (int *) 0x108. By the way, I'm surprise by the output of WP you report here. Which version are you using ? I suggest you to move to Fluorine, where the memory model of wp offers more options on pointers and casts. Regards. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131210/4a838ce9/attachment.html>