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

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