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


  • Subject: [Frama-c-discuss] Named behavior, proof obligations and ACSL annotations: the string comparison example
  • From: Thomas.PAREAUD at astrium.eads.net (PAREAUD, Thomas)
  • Date: Thu, 26 Mar 2009 15:56:30 +0100

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