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,

The jessie-int-model option allow to manage used integer type
Three options :
   exact : abstract integer are used (no limits)
   modulo : such as int type, integer used in specification are defined on 32 bits.
   bounded : such as bounded, but in case of overflow, the value is bounded to 
maxint or minint.

The "exact" option is more efficient because there is no Integer conversion 
introduced in the PO. However, the behavior is not correct if an overflow can occur.


Regards,
Nicolas Stouls


JENN Eric a ?crit :
> Dear Nicolas,
> 
> Thanks for your answer... which was extremely useful.
> Using "-jessie-int-model exact" makes all three PO to be immediately 
> discharged whereas /without this option/, all provers ended up with /a 
> timeout.
> /Now, in order to add a new item to my FAQ, could you provide me with a 
> brief explanation why "int-model exact" is required here?
> Thanks in advance!
> Regards,
> e.
> (and sorry for asking such dumb question).
> 
> Nicolas Stouls a ?crit :
>> 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
>> _______________________________________________
>> 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
> _______________________________________________
> 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/1854de27/attachment.vcf