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] Named behavior, proof obligations and ACSL annotations: the string comparison example

Thank you for these advices.

Using return statement make identity proved.
Nevertheless, my main goal is to prove this code without modifying it.

Just another question.
How is it possible to know what is the problem in proving the VC expressions (in the top right panel of Gwhy)?
For example, the VC below is not resolved, but I do not known why.

Could you explain me?

Thanks again.
--
Thomas Pareaud


*********************************************************************
strncmp_ensures_negative_po_2

pString1: char_P pointer
pString2: char_P pointer
nbBytes_0: int
char_P_pString1_27_alloc_table: char_P alloc_table
char_P_pString2_28_alloc_table: char_P alloc_table
char_P_char_M_pString1_27: (char_P, int) memory
char_P_char_M_pString2_28: (char_P, int) memory
H1: (nbBytes_0 > 0 and
     (exists j_9:int,
      select(char_P_char_M_pString1_27, shift(pString1, j_9)) < select(char_P_char_M_pString2_28,
                                                                shift(pString2,
                                                                j_9)) and
      (forall i_33:int.
       0 <= i_33 and i_33 < j_9 and j_9 < nbBytes_0 ->
       select(char_P_char_M_pString1_27, shift(pString1, i_33)) = select(char_P_char_M_pString2_28,
                                                                  shift(pString2,
                                                                  i_33))))) and
    (nbBytes_0 >= 0 and
     offset_min(char_P_pString1_27_alloc_table, pString1) <= 0 and
     offset_max(char_P_pString1_27_alloc_table, pString1) >= nbBytes_0 - 1 and
     offset_min(char_P_pString2_28_alloc_table, pString2) <= 0 and
     offset_max(char_P_pString2_28_alloc_table, pString2) >= nbBytes_0 - 1 and
     (nbBytes_0 <> 0 ->
      (exists j_13:int,
       0 <= j_13 and
       j_13 < nbBytes_0 and
       select(char_P_char_M_pString1_27, shift(pString1, j_13)) = 0)) and
     (nbBytes_0 <> 0 ->
      (exists j_12:int,
       0 <= j_12 and
       j_12 < nbBytes_0 and
       select(char_P_char_M_pString2_28, shift(pString2, j_12)) = 0)))
diff: int
H6: diff = 0
H11: nbBytes_0 <> 0
mutable_nbBytes_0: int
mutable_pString1: char_P pointer
mutable_pString2: char_P pointer
H12: true
H13: (0 < mutable_nbBytes_0 and
      mutable_nbBytes_0 <= nbBytes_0 and
      0 = diff and
      shift(pString1, nbBytes_0) = shift(mutable_pString1, mutable_nbBytes_0) and
      shift(pString2, nbBytes_0) = shift(mutable_pString2, mutable_nbBytes_0) and
      (mutable_nbBytes_0 <> nbBytes_0 ->
       select(char_P_char_M_pString1_27, shift(mutable_pString1, -1)) = 
       select(char_P_char_M_pString2_28, shift(mutable_pString2, -1))) and
      (forall k_3:int.
       0 <= k_3 and k_3 < nbBytes_0 - mutable_nbBytes_0 ->
       select(char_P_char_M_pString1_27, shift(pString1, k_3)) = select(char_P_char_M_pString2_28,
                                                                 shift(pString2,
                                                                 k_3))) and
      (forall k_4:int.
       0 <= k_4 and k_4 < nbBytes_0 - mutable_nbBytes_0 ->
       select(char_P_char_M_pString1_27, shift(pString1, k_4)) = select(char_P_char_M_pString2_28,
                                                                 shift(pString2,
                                                                 k_4))))
tmp_0_2: int
H14: tmp_0_2 = mutable_nbBytes_0
mutable_nbBytes_0_0: int
H15: mutable_nbBytes_0_0 = mutable_nbBytes_0 - 1
H16: tmp_0_2 <> 0
result: int
H17: result = select(char_P_char_M_pString1_27, mutable_pString1)
result0: int
H18: result0 = select(char_P_char_M_pString2_28, mutable_pString2)
H19: result = result0
H20: mutable_nbBytes_0_0 = 0
result1: int
H21: result1 = select(char_P_char_M_pString1_27, mutable_pString1)
result2: int
H22: result2 = select(char_P_char_M_pString2_28, mutable_pString2)
__retres: int
H23: __retres = result1 - result2
return: int
H24: return = __retres
              

return < 0
 

-----Message d'origine-----
De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Claude March?
Envoy? : jeudi 26 mars 2009 17:20
? : Frama-C public discussion
Objet : Re: [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example


I guess there is also a tricky point, because the way your code is 
written. Using directly return statements without using the diff 
variable should make things simpler. With the diff variable, it might be 
necessary to specify that diff is not modified in the loop... (i.e 
remains 0)

sorry I can't help more without running the example and see precisely 
what VC are not proved.

- Claude

PAREAUD, Thomas wrote:
> Thank you for this answer.
> 
> Is the 3) point is equivalent to add the predicate below in the loop invariant declaration?
> 
> loop invariant
>       [...]
>    && \forall integer k ; 0 <= k < (\at(nbBytes, Pre) - nbBytes) ==> (*(\at(pString1, Pre)+k) == *(\at(pString2, Pre)+k));
> 
> This line is equivalent to the following one:
> 
> \forall integer k ; 0 <= k < (\at(nbBytes, Pre) - nbBytes) ==> (*(pString1-k) == *(pString2-k));
> 
> 
> But none of the two solutions makes solver proving anything.
> 
> Have you any other idea?
> --
> Thomas Pareaud
> 
> 
>  
> 
> -----Message d'origine-----
> De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Claude March?
> Envoy? : jeudi 26 mars 2009 16:19
> ? : Frama-C public discussion
> Objet : Re: [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example
> 
> A few hints:
> 
> 1) use integer instead of int in annotations. It will probably not help, 
> but is better practice
> 
> 2) split the identity into two, w.r.t your disjunction.
> 
> 3) add a loop invariant expressing that the chars visited so far are 
> equal, otherwise you will not be able to prove anything.
> 
> - Claude
> 
> PAREAUD, Thomas wrote:
>> Dear all,
>>
>> I am a recent user of Frama-C and its Jessie plug-in.
>> I tried for several days to train to this tool.
>>
>> Below, there is an example of a function that compare two strings.
>> There are four different behaviors:
>> - zero: the number of byte to compare equals 0 (return 0)
>> - identity: the two strings are identical (return 0)
>> - positive: it exists a position such as every char before this position
>> were identical between the two strings, and the char at this position is
>> greater in the first string that in the second one.
>> - negative: it exists a position such as every char before this position
>> were identical between the two strings, and the char at this position is
>> lower in the first string that in the second one.
>>
>> I managed to prove the "Safety" (verified by the Yices solver thanks to
>> the loop invariant I introduced) and "zero" behaviors. 
>> Nevertheless, I did not manage to prove neither identity, nor positive,
>> nor negative behaviors.
>>
>> You can find the detail of the code and ACSL annotations below.
>>
>> Does someone have a proposition?
>>
>> Best regards,
>> --
>> Thomas Pareaud
>>
>>
>>
>> /*@ requires nbBytes >= 0;
>>   @ requires \valid(pString1 + (0..(nbBytes-1))); 
>>   @ requires \valid(pString2 + (0..(nbBytes-1)));
>>   @ requires nbBytes!=0 ==> \exists int j ; 0<=j<nbBytes &&
>> *(pString1+j)==0;
>>   @ requires nbBytes!=0 ==> \exists int j ; 0<=j<nbBytes &&
>> *(pString2+j)==0;
>>   @ assigns \nothing;
>>   @ behavior zero:
>>   @   assumes nbBytes == 0;
>>   @   ensures \result == 0;
>>   @ behavior identity: 
>>   @   assumes 
>>   @     nbBytes > 0 
>>   @     && (
>>   @       (\forall int i; 0<=i<nbBytes ==> *(pString1+i)==*(pString2+i))
>>   @       || (\exists int j; 0<=j<nbBytes && *(pString1+j)==0 &&
>> (\forall int i; 0<=i<=j ==> *(pString1+i)==*(pString2+i)))
>>   @     );
>>   @   ensures \result == 0;
>>   @ behavior postive: 
>>   @   assumes nbBytes > 0 && \exists int j; *(pString1+j)>*(pString2+j)
>> && (\forall int i; 0<=i<j<nbBytes ==> *(pString1+i)==*(pString2+i)); 
>>   @   ensures \result > 0;
>>   @ behavior negative: 
>>   @   assumes nbBytes > 0 && \exists int j; *(pString1+j)<*(pString2+j)
>> && (\forall int i; 0<=i<j<nbBytes ==> *(pString1+i)==*(pString2+i)); 
>>   @   ensures \result < 0;
>>   @ disjoint behaviors zero, identity, non_identity;
>>  */
>> int strncmp(const char *pString1, const char *pString2, unsigned int
>> nbBytes)
>> {
>>   int diff = 0;
>>
>>   if (nbBytes == 0)
>>   {
>>     diff = 0;
>>   }
>>   else
>>   {
>> /*@ loop invariant 
>>   @   0 < nbBytes <= \at(nbBytes, Pre) 
>>   @   && \at(pString1, Pre) + \at(nbBytes, Pre) == pString1 + nbBytes 
>>   @   && \at(pString2, Pre) + \at(nbBytes, Pre) == pString2 + nbBytes ;
>>   @ loop assigns \nothing;
>>   @ loop variant nbBytes;
>>   */
>>     while ((nbBytes-- != 0) && (*pString1 == *pString2))
>>     {
>> 		if ((nbBytes == 0) || (*pString1 == '\0')){
>> 			break;
>> 		}
>> 		pString1++;
>> 		pString2++;
>>     }
>> 	diff = (((int)*pString1) - ((int)*pString2));
>>   }
>>
>>   return diff;
>> }
>>
>>
>> Ce courriel (incluant ses eventuelles pieces jointes) peut contenir des informations confidentielles et/ou protegees ou dont la diffusion est restreinte. Si vous avez recu ce courriel par erreur, vous ne devez ni le copier, ni l'utiliser, ni en divulguer le contenu a quiconque. Merci d'en avertir immediatement l'expediteur et d'effacer ce courriel de votre systeme. Astrium decline toute responsabilite en cas de corruption par virus, d'alteration ou de falsification de ce courriel lors de sa transmission par voie electronique.
>> This email (including any attachments) may contain confidential and/or privileged information or information otherwise protected from disclosure. If you are not the intended recipient, please notify the sender immediately, do not copy this message or any attachments and do not use it for any purpose or disclose its content to any person, but delete this message and any attachments from your system. Astrium disclaims any and all liability if this email transmission was virus corrupted, altered or falsified. 
>> ---------------------------------------------------------------------
>> Astrium SAS (393 341 516 RCS Paris) - Siege social: 6 rue Laurent Pichat, 75016 Paris, France
>>
>> _______________________________________________
>> 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
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |







_______________________________________________
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

Ce courriel (incluant ses eventuelles pieces jointes) peut contenir des informations confidentielles et/ou protegees ou dont la diffusion est restreinte. Si vous avez recu ce courriel par erreur, vous ne devez ni le copier, ni l'utiliser, ni en divulguer le contenu a quiconque. Merci d'en avertir immediatement l'expediteur et d'effacer ce courriel de votre systeme. Astrium decline toute responsabilite en cas de corruption par virus, d'alteration ou de falsification de ce courriel lors de sa transmission par voie electronique.
This email (including any attachments) may contain confidential and/or privileged information or information otherwise protected from disclosure. If you are not the intended recipient, please notify the sender immediately, do not copy this message or any attachments and do not use it for any purpose or disclose its content to any person, but delete this message and any attachments from your system. Astrium disclaims any and all liability if this email transmission was virus corrupted, altered or falsified. 
---------------------------------------------------------------------
Astrium SAS (393 341 516 RCS Paris) - Siege social: 6 rue Laurent Pichat, 75016 Paris, France