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] Why wp plugin failed to prove such naive properties?

Hello David,

2013/11/11 David Yang <abiao.yang at gmail.com>:
> In my point of view, the assign means that the locs is assigned in this
> function.

No. Please refer to ACSL manual, p. 29:
"""
1 /*@ r e q u i r e s P1; r e q u i r e s P2; ...
2 @ a s s i g n s L1; a s s i g n s L2; ...
3 @ e n s u r e s E1; e n s u r e s E2; ...
4 @*/

The semantics of such a contract is as follows:
[...]
All memory locations that are allocated in both the pre-state and the
post-state and
do not belong to the set L1 U L2 U ... are left unchanged in the
post-state. The set
L1 U L2 U ... itself is interpreted in the pre-state.
"""

In other words, assigns clause says that all other locations different
from L1, L2, ... are NOT assigned. But it does NOT say that L1, L2,
... locations ARE assigned.

In other words, assigns clause is a superset of effectively assigned locations.

> But  the following property (labeled with "C") was also proved to be valid
> in frama-c(I am using the wp plugin to prove the contract). But the "Arr"
> parameter was only used but not to be defined in the function test. The
> "NoUse" parameter never used in this function at all.
>
> Am I wrongly understand the assign clause?
>
> Thanks.
>
> /*@
> requires \valid(Arr);
> ensures A: Arr == \old(Arr);
> ensures B: *\old(Arr) == \old(*Arr);
> assigns C: *Arr, *NoUse;
>   */
> int test(int *Arr, int index, int *NoUse)
> {
>   return Arr[index];
> }

Proving above assigns clause in your code is consistent with above
reading. You can decrease the assigns clause down to "assigns
\nothing;" and it is still proved.

Best regards,
david