--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL by Example: contradiction in Count axiomatic



Hello!

In "ACSL By Example Version 14.1.0"
(https://cdn0.scrvt.com/fokus/c8efcdaac330d718/6cc5d3fc9481/ACSL-by-Example_14_1_0.pdf),
Listing 3.32 p.46 (The logic function Count) there is the definition:

axiomatic Count {
logic integer Count{L}(value_type *a, integer m, integer n, value_type
v) reads a[m..n-1];

axiom CountSectionEmpty:
    \forall value_type *a, v, integer m, n;
        n <= m ==> Count(a, m, n, v) == 0;

axiom CountSectionHit:
    \forall value_type *a, v, integer n, m;
        a[n] == v ==> Count(a, m, n + 1, v) == Count(a, m, n, v) + 1;

...
}

With contradiction in it (tested with WP):

value_type a = 5;

assert Count(&a + 1, 0, -1, (value_type) 5) == 0;
assert Count(&a + 1, 0, 0, (value_type) 5)  == 0;
assert Count(&a + 1, 0, 0, (value_type) 5)  == Count(&a + 1, 0, -1,
(value_type) 5) + 1;
assert 0 == 1;


Suggested fix is to add premise m < n to CountSectionHit and
CountSectionMiss axioms e.g.:

axiom CountSectionHit:
    \forall value_type *a, v, integer n, m;
        (m < n) && a[n] == v ==> Count(a, m, n + 1, v) == Count(a, m,
n, v) + 1;

Complete example attached.

Found by AstraVer project team (http://linuxtesting.org/astraver).
We have already notified "ACSL By Example" authors.

---

typedef int value_type;

// ACSL By Example (14.1.0) Listing 3.32 (p.46)
// Count axiomatic w/o CountSectionRead axiom
/*@
axiomatic Count {
logic integer Count{L}(value_type *a, integer m, integer n, value_type
v) reads a[m..n-1];

axiom CountSectionEmpty:
   \forall value_type *a, v, integer m, n;
      n <= m ==> Count(a, m, n, v) == 0;

axiom CountSectionHit:
   \forall value_type *a, v, integer n, m;
      a[n] == v ==> Count(a, m, n + 1, v) == Count(a, m, n, v) + 1;

axiom CountSectionMiss:
   \forall value_type *a, v, integer n, m;
      a[n] != v ==> Count(a, m, n + 1, v) == Count(a, m, n, v);
}*/


/*@ assigns \nothing;
 */
void test(void)
{
   value_type a = 5;
   //@ assert Count(&a + 1, 0, -1, (value_type) 5) == 0;
   //@ assert Count(&a + 1, 0, 0, (value_type) 5) == 0;
   //@ assert Count(&a + 1, 0, 0, (value_type) 5) == Count(&a + 1, 0,
-1, (value_type) 5) + 1;
   //@ assert 0 == 1;
}