--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on June 2009 ---
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...). -------------- next part -------------- A non-text attachment was scrubbed... Name: eric.jenn.vcf Type: text/x-vcard Size: 191 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090604/cc484852/attachment.vcf