Frama-C Bug Tracking System - Frama-C
View Issue Details
0001007Frama-CKernel > ACSL implementationpublic2011-11-03 13:162011-11-10 14:18
Jochen 
virgile 
normalmajoralways
assignedopen 
Frama-C Nitrogen-20111001 
 
0001007: wrong proof obligation generated for loop initialization [under why-2.30]
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[0]==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.
No tags attached.
c ftest.c (186) 2011-11-03 13:16
https://bts.frama-c.com/file_download.php?file_id=288&type=bug
Issue History
2011-11-03 13:16JochenNew Issue
2011-11-03 13:16JochenStatusnew => assigned
2011-11-03 13:16JochenAssigned To => cmarche
2011-11-03 13:16JochenFile Added: ftest.c
2011-11-08 07:48monateNote Added: 0002457
2011-11-08 07:49monateAssigned Tocmarche => virgile
2011-11-08 07:49monateCategoryPlug-in > jessie => Kernel > ACSL implementation
2011-11-08 09:03virgileNote Added: 0002458
2011-11-10 12:57JochenNote Added: 0002461
2011-11-10 14:18virgileNote Added: 0002462

Notes
(0002457)
monate   
2011-11-08 07:48   
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.
(0002458)
virgile   
2011-11-08 09:03   
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).
(0002461)
Jochen   
2011-11-10 12:57   
"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]" - ?
(0002462)
virgile   
2011-11-10 14:18   
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)