--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on June 2009 ---
[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