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.

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