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