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] Inductive definition of reachability in an array-implemented list.

Dear Nicolas,

thanks for answering the questions about the integer models.
I must admit that I usually have a hard time to explain to people
from industry about the different models.
They usually ask:

	"What is the purpose of a proof of my code when I use normal C  
integer arithmtic
	but the prover uses mathematical integers?"

What would you say?

Regards

Jens

Am 04.06.2009 um 23:11 schrieb Nicolas Stouls:

> Dear,
>
> The jessie-int-model option allow to manage used integer type
> Three options :
>  exact : abstract integer are used (no limits)
>  modulo : such as int type, integer used in specification are  
> defined on 32 bits.
>  bounded : such as bounded, but in case of overflow, the value is  
> bounded to maxint or minint.
>
> The "exact" option is more efficient because there is no Integer  
> conversion introduced in the PO. However, the behavior is not  
> correct if an overflow can occur.
>
>
> Regards,
> Nicolas Stouls
>



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090605/2be506f6/attachment.htm