--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on December 2013 ---
Please, find any additional informations in the WP manual, sections 2.3 and 3. Actually, "no cast" is not the option you want, I guess. Usually, you only need the default, Typed memory model. Regards, L. ________________________________ De : frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Xiao-lei Cui [x_cui at hotmail.com] Date d'envoi : mercredi 11 d?cembre 2013 03:13 ? : Frama-C public discussion Objet : Re: [Frama-c-discuss] RE : [wp] type conversion check is less strict than Jessie? 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/20131211/a985c725/attachment.html>