Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001007Frama-CKernel > ACSL implementationpublic2011-11-03 13:162011-11-10 14:18
Assigned Tovirgile 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in Version 
Summary0001007: wrong proof obligation generated for loop initialization [under why-2.30]
DescriptionUsing 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.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (186 bytes) 2011-11-03 13:16 [Show Content]

- Relationships

-  Notes
monate (reporter)
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.
virgile (developer)
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).
Jochen (reporter)
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]" - ?
virgile (developer)
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)

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker