--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on June 2009 ---
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 -------------- 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/a5330f04/attachment.vcf