--- layout: fc_discuss_archives title: Message 77 from Frama-C-discuss on November 2013 ---
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