--- layout: fc_discuss_archives title: Message 10 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 (Denis Efremov)



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;
    }