Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Inductive definition of reachability in an array-implemented list.

  • Subject: [Frama-c-discuss] Inductive definition of reachability in an array-implemented list.
  • From: eric.jenn at fr.thalesgroup.com (JENN Eric)
  • Date: Thu, 04 Jun 2009 15:52:50 +0200
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