--- layout: fc_discuss_archives title: Message 12 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 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