View Issue Details [ Jump to Notes ] [ Related Changesets ]  [ Issue History ] [ Print ] 
ID  Project  Category  View Status  Date Submitted  Last Update 
0001443  FramaC  Plugin > wp  public  20130611 20:44  20140313 15:57 

Reporter  virgile  
Assigned To  signoles  
Priority  normal  Severity  minor  Reproducibility  always 
Status  closed  Resolution  fixed  
Platform   OS   OS Version  
Product Version  FramaC Fluorine20130501  
Target Version   Fixed in Version  FramaC Neon20140301  

Summary  0001443: Property reported as inconditionnally valid when its dependency graph shows some orange box 
Description  Using wp on the attached files, the rtegenerated asserts (and some loop invariants) are reported as valid (green bullet), while they are dependent of some unproved loop invariant.
I flag it as WP bug, as it occurs only when specifying two provers with wpproof, so that I suspect some issue in reporting dependencies in this setting. 
Steps To Reproduce  command line used:
framacgui wp wpmodel Typed+ref wpsplit binary_search_proved.c wprte wpproof altergo,why3:Z3 
Tags  No tags attached. 

Attached Files  binary_search_proved.c [^] (1,137 bytes) 20130611 20:44 [Show Content] [Hide Content]/*@ requires \valid(a+(0..length1));
requires \forall integer i,j; 0<=i<=j<length ==> a[i]<=a[j];
requires length >=0;
assigns \nothing;
behavior exists:
assumes \exists integer i; 0<=i<length && a[i] == key;
ensures 0<=\result<length && a[\result] == key;
behavior not_exists:
assumes \forall integer i; 0<=i<length ==> a[i] != key;
ensures \result == 1;
complete behaviors;
disjoint behaviors;
*/
int binary_search(int* a, int length, int key) {
int low = 0, high = length  1;
/*@ loop invariant 0<=low<=high+1;
loop invariant high<length;
loop assigns low,high;
loop invariant \forall integer k; 0<=k<low ==> a[k] < key;
loop invariant \forall integer k; high<k<length ==> a[k] > key;
loop variant highlow;
*/
while (low<=high) {
int mid = low+(highlow)/2;
if (a[mid] == key) return mid;
if (a[mid] < key) { low = mid+1; }
else {
high = mid  1;
}
}
return 1;
}
/*
Local Variables:
compilecommand: "framacgui wp wprte wpmodel Typed+ref wpsplit wptimeout 30 binary_search_proved.c"
End:
*/

