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] Help with proving post-conditions

Hi again,
I've made the recommended changes but I still can't prove the 3 of the
post-conditions although everything else is proven with Z3 including the
asserts.
I guess my loop invariants for the second loop are the problem as I find it
hard to express the null character being copied with the way the loop is
written. 

I'd appreciate your help with this.

		/*@ requires valid_string(s);
		    requires valid_string(append);
		    requires \valid_range(s, 0, strlen(s) + strlen(append));
		    assigns s[..];
		    ensures strlen(s) == strlen{Old}(s) + strlen(append);
		    ensures \forall integer i; 0 <= i < strlen{Old}(s) ==>
s[i] == \old(s[i]);
		    ensures \forall integer j; strlen{Old}(s) <= j <=
strlen(s) ==> s[j] == append[j];
		    ensures  \result == s;
		 */
		char *
		strcat(char *s, const char *append)
		{
			char *save = s;

			/*@ loop assigns s;
				loop invariant 0 <= (s-save) <=
strlen(save);
				loop invariant \valid(s);
				loop invariant \base_addr(s) ==
\base_addr(save);
				loop invariant \forall integer k; 0 <= k <
(s-save) ==> save[k] != 0;
			*/
			for (; *s; ++s);
			//@ assert *s == '\0' && s == save + strlen(save);
			//@ assert \valid_range(s, 0, strlen(append));

			//@ ghost char *s_cat = s;
			//@ ghost char *origAppend = append;

			/*@ loop assigns s, s_cat[..], append;
				loop invariant \base_addr(s) ==
\base_addr(s_cat);
				loop invariant \base_addr(append) ==
\base_addr(origAppend);
				loop invariant \valid_range(origAppend, 0,
strlen{Pre}(append));
				loop invariant \valid_range(s_cat, 0,
strlen{Pre}(append));
				loop invariant (append-origAppend) == (s -
s_cat);
				loop invariant 0 <= (append-origAppend) <=
strlen(origAppend);
				loop invariant \forall integer k; 0 <= k <
(append-origAppend) < strlen(origAppend) ==> origAppend[k] != 0;
				loop invariant \forall integer k; 0 <= k <
(append-origAppend) ==> s_cat[k] == origAppend[k];
			*/
			while ((*s++ = *append++) != '\0');
			//@ assert s_cat[append-origAppend - 1] == 0;
			//@ assert strlen(s_cat) == append-origAppend -1;
			//@ assert strlen(origAppend) == append-origAppend
-1;
			//@ assert strlen(s_cat) == strlen(origAppend);
			return(save);
		} 

Thanks,
Murat.

From: frama-c-discuss-bounces at lists.gforge.inria.fr
[mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pascal
Cuoq
Sent: Wednesday, December 09, 2009 12:26 PM
To: Frama-C public discussion
Subject: [Frama-c-discuss] Help with proving post-conditions

Hello,


    ensures strlen(s) == strlen(\at(s, Old)) + strlen(append);

Which strlen function are you trying to use here?
If you mean the C function, you can't: it is not
allowed to call a C function from inside a predicate such
as a pre/prost-condition.

You can have a logic function (I would recommend
to use a slight variation on the strlen name), defined
by yourself as the function that computes
the length of a string. That is the right way to do it.

Another thing:  \at(s, Old) (that you can write \old(s))
does not do what you think it does. In fact, since
strcat does not (in general, unless the caller created
some strange aliasing conditions) modify its
argument s, \old(s) is the same as s. 

What the logic function logic_strlen really takes in
argument is a pointer s *and* a memory state
in which s points to some bytes, and with this
information, it is able to tell you what the length
of s is *in the memory state that you provided*.

Function logic_strlen only needs one memory state, so
this memory state can remain implicit in the body of
the definition, but you have to be aware that
it is an argument of the function,
and that you need to pass it.

In this case you would pass Old i.e. write
something like logic_strlen{Old}(s) instead of
strlen(\at(s, Old)).

Perhaps the explanations in chapter 8 of
the ACSL mini-tutorial 
http://frama-c.cea.fr/download/acsl-tutorial.pdf
can be of help.

Pascal

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 9198 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091210/c6cfc96f/attachment-0001.bin