Lithum- Z3 shell aborts with error message
ID0000030: This issue was created automatically from Mantis Issue 30. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0000030 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2014-02-12 |
Reporter | virgile | Assigned To | cmarche | Resolution | unable to reproduce |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Lithium-20081201 | Target Version | - | Fixed in Version | Frama-C Beryllium-20090902 |
Description :
[bug #7241 from old bts, reported by Christoph Weber] Hello,
while I was trying to proof a function I got an error message.
Unfortunatly, I dont have time to figure out a smaller example
But the error occured when I altered the clause:
====== ensures ( (\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) && a[k1] < b[k1]) || (\forall integer k2; (0 <= k2 < length_a) ==> length_a < length_b && a[k2] == b[k2]) ) ==> \result == 1 ;
into: ensures ( (\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) && a[k1] < b[k1]) || (\forall integer k2; (0 <= k2 < length_a) ==> length_a < length_b && a[k2] == b[k2]) ) ^^ \result == 0 ;
========== Here the source-code:
/*@ requires 0 <= length_a; requires 0 <= length_b;
requires \valid_range (a, 0, length_a-1); requires \valid_range (b, 0, length_b-1);
assigns \nothing;
ensures \result == 1 || \result == 0;
ensures ( (\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) && a[k1] < b[k1]) || (\forall integer k2; (0 <= k2 < length_a) ==> length_a < length_b && a[k2] == b[k2]) ) ^^ \result ==0 ;
/
int lexicographical_compare_array (int a, int length_a, int* b, int length_b)
{
int i = 0;
/*@
loop invariant 0 <= i <= length_a;
loop invariant 0 <= i <= length_b;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];
*/
for ( ; i != length_a && i != length_b; ++i)
{
if (a[i] < b[i])
{
/*@
assert \exists integer k1; 0 <= k1 <= i && a[k1] < b[k1];
*/
return 1;
}
if (b[i] < a[i])
{
return 0;
}
}
//return i == length_a && i != length_b ? 1 : 0;
if (i == length_a && i != length_b)
{
/*@
assert
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) && a[k1] < b[k1]) || (\forall integer k2; (0 <= k2 < length_a) ==> length_a < length_b && a[k2] == b[k2]) ); */ return 1; } else { return 0; } }
Sorry for the complex function,
Cheers Christoph