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

Thank you Pascal for the explanation.

Strlen I was using was a logic function, I will try to pass the state {Old}
instead as you suggest and see if I can fix it.

That makes sense now to me because I was seeing the VCs generated were like:


    strlen(s, .s_0_25) = strlen(s, .s_0_25) + strlen(append) 

where s_0_25 bits were identical which can't be proven obviously.

 

Thanks again for the help. I will try this.

 

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 --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091209/93000430/attachment.htm