--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on June 2009 ---
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 JENN Eric a ?crit : > Dear Nicolas, > > Thanks for your answer... which was extremely useful. > Using "-jessie-int-model exact" makes all three PO to be immediately > discharged whereas /without this option/, all provers ended up with /a > timeout. > /Now, in order to add a new item to my FAQ, could you provide me with a > brief explanation why "int-model exact" is required here? > Thanks in advance! > Regards, > e. > (and sorry for asking such dumb question). > > Nicolas Stouls a ?crit : >> Dear, >> >> If you use : >> >> frama-c <givenProgram.c> -jessie-analysis -jessie-gui >> -jessie-int-model exact >> >> then alt-ergo discharged all two POs. Thus the question is : >> >> What is the real status of PO whitout this option ? (fail or timeout) >> >> Regards >> >> Nicolas. >> >> >> JENN Eric a ?crit : >>> Dear Colleagues, >>> >>> I am puzzled by the following example, which is a slightly adapted >>> version of a bigger piece of code I am working on: >>> >>> typedef int T_ID; >>> >>> typedef struct >>> { >>> T_ID next; >>> } T_ELT; >>> >>> >>> T_ELT LIST[4]; >>> >>> // >>> // Definition of reachability >>> // >>> /*@ >>> inductive is_reachable{L}(T_ID start_id, T_ID end_id) { >>> case is_length_one{L}: >>> \forall T_ID alert_id; >>> (0 <= alert_id < 4) ==> >>> is_reachable(alert_id, alert_id); >>> case is_path_non_one{L}: >>> \forall T_ID start_id, T_ID end_id; >>> ((0 <= start_id < 4) && (0 <= end_id < 4)) ==> >>> is_reachable(LIST[start_id].next, end_id) ==> >>> is_reachable( start_id, end_id); >>> } >>> @*/ >>> >>> /*@ >>> requires >>> \valid(LIST+(0..3)); >>> >>> ensures >>> is_reachable((T_ID)0,(T_ID)1); >>> >>> ensures >>> is_reachable((T_ID)0,(T_ID)0); >>> >>> @*/ >>> >>> void f() >>> { >>> LIST[0].next = 1; >>> LIST[1].next = 2; >>> LIST[2].next = 3; >>> LIST[3].next = -1; >>> >>> } >>> >>> The PO for the second postcondition is verified (hopefully). >>> The PO for the first post-condition can't be discharged neither by >>> Ergo, nor by Simply, nor by Z3. >>> >>> (As usual,) I am certainly missing something obvious, but what? >>> >>> Thanks for your help >>> >>> Regards, >>> >>> e. >>> >>> By the way... >>> A few proposals for "improvements" to gWhy: >>> - It would be nice if one could select provers on a per-PO basis and >>> save this configuration, so as to replay the proof automatically with >>> the appropriate prover. >>> - It would be nice if it were possible to try another prover when a >>> proof fails with a given prover (the one selected using the menu). >>> - It would be nice if we could benefit from multi-cores to start as >>> many provers as there are cores, automatically (that what I do >>> manually...). >>> >>> _______________________________________________ >>> Frama-c-discuss mailing list >>> Frama-c-discuss at lists.gforge.inria.fr >>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: nicolas_stouls.vcf Type: text/x-vcard Taille: 445 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090604/1854de27/attachment.vcf