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] RE : RE : [wp] type conversion check is less strict than Jessie?

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>