--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on April 2017 ---
Hello Denis, thanks again for reporting this issue. We are in the process of preparing a new release of âACSL by Exampleâ which will fix this inconsistency. Regards Jens 1. ACSL by Example: contradiction in Count axiomatic (Denis Efremov) ---------------------------------------------------------------------- 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; }