|Anonymous | Login | Signup for a new account||2019-05-22 17:59 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001007||Frama-C||Kernel > ACSL implementation||public||2011-11-03 13:16||2011-11-10 14:18|
|Product Version||Frama-C Nitrogen-20111001|
|Target Version||Fixed in Version|
|Summary||0001007: wrong proof obligation generated for loop initialization [under why-2.30]|
|Description||Using Frama-C Nitrogen and Why 2.30, I ran the command "frama-c -cpp-command 'gcc -C -E -I.' -jessie -jessie-why-opt='-exp goal' -no-unicode -jessie-atp simplify ftest.c" on the attached program. The very first proof obligation formula, viz. ftest_ensures_default_po_1, has "iii" as a free variable, which is unusual. |
The formula essentially says that a==a[iii], which can neither be justified by the program code, nor by the loop invariant, nor by the function contract. I guess, the formula is intended to cover the loop initialization, but something like "FORALL (iii) (IMPLIES (EQ iii 0) ... )" is missing.
|Tags||No tags attached.|
|Attached Files||ftest.c [^] (186 bytes) 2011-11-03 13:16 [Show Content]|
Your loop invariant is not correct. You probably meant:
loop invariant a[iii] == \at(a[\at(iii,Here)],Pre);
or equivalently but shorter:
loop invariant a[iii] == \at(a,Pre)[iii];
i.e. the index iii in a should be evaluated in the current state and not in the pre-state.
The typechecker could (should?) report an error as iii is not even in the scope of the pre-state Pre.
FYI, my tests were done with Wp and not Jessie.
|I agree that the typechecker should do something here. However, given the fact that a is a pointer, \at(a,Pre)[iii] is NOT equivalent to \at(a,Pre)[iii] (this would be the case if a was a C array).|
"administrator" is right: I tried his short version and everything was fine under Why 2.30 / Jessie, too.
From a user's point of view, I agree a warning would be helpful, in particular as it is easy to get confused about the adequate use of Pre,Old,Here,Post in different syntactic contexts.
Virgile probably meant "\at(a,Pre)[iii] is NOT equivalent to a[iii]" - ?
Sorry for the confusion, but no, I meant that \at(a,Pre)[iii] is NOT equivalent to \at(a[\at(iii,Here)],Pre): in the former, you evaluate only a in Pre-state, in the latter, both a and the content of a + iii are evaluated in the Pre-state (iii itself being evaluated Here).
When a is an array, things are different though: in that case, \at(a,Pre) evaluates to the whole array in Pre state, and both expressions are indeed equivalent.
In the case of a pointer, it might be clearer to use explicit dereference:
\at(a,Pre)[iii] == *(\at(a,Pre)+iii)
\at(a[\at(iii,Here)],Pre) == \at(*(a+\at(iii,Here)),Pre)
|2011-11-03 13:16||Jochen||New Issue|
|2011-11-03 13:16||Jochen||Status||new => assigned|
|2011-11-03 13:16||Jochen||Assigned To||=> cmarche|
|2011-11-03 13:16||Jochen||File Added: ftest.c|
|2011-11-08 07:48||monate||Note Added: 0002457|
|2011-11-08 07:49||monate||Assigned To||cmarche => virgile|
|2011-11-08 07:49||monate||Category||Plug-in > jessie => Kernel > ACSL implementation|
|2011-11-08 09:03||virgile||Note Added: 0002458|
|2011-11-10 12:57||Jochen||Note Added: 0002461|
|2011-11-10 14:18||virgile||Note Added: 0002462|
|Copyright © 2000 - 2019 MantisBT Team|