georgefernendis Apr 15, 2011 at 3:16 PM A very basic and simple loop invariant but still I am not be debug why VCC is able to verify the loop invariant of the function given below. 'Loop body invariant doesn't verifies' What could be the possible point i am missing here. ============================================ bool bitmap_contains (const struct bitmap *b, size_t start, size_t cnt, bool value) requires(b!=NULL) requires((start + cnt )<= b->bit_cnt) requires(wrapped(b)) ensures(!result <==> forall(size_t k;k>=0 && k exists(size_t k;k>=0 && k=0 && i<=cnt)       invariant(forall(size_t k; k>=0 && kbits[elem_idx (start+k)] & bit_mask (start+k)) != 0) != value))             // NOT able to verify it ??       invariant(start+i<=b->bit_cnt)       {        idx=start+i;                  if (((b->bits[elem_idx (idx)] & bit_mask (idx)) != 0) == value)         return true;    } assert(forall(size_t k;k>=0 && k0            && is_malloc_root(this)          // if i want to free bitmap            && is_malloc_root(as_array(bits, bit_cnt)) // if i want free bits array             )   }; /* Returns the index of the element that contains the bit    numbered BIT_IDX. */ ispure static inline size_t elem_idx (size_t bit_idx)     returns(bit_idx/ELEM_BITS) {     assert(ELEM_BITS>0);   return bit_idx / ELEM_BITS; } /* Returns the index of the element that contains the bit    numbered BIT_IDX. */ ispure static inline size_t elem_idx (size_t bit_idx)     returns(bit_idx/ELEM_BITS) {     assert(ELEM_BITS>0);   return bit_idx / ELEM_BITS; } /* Returns an elem_type where only the bit corresponding to    BIT_IDX is turned on. */ ispure static inline elem_type     bit_mask (size_t bit_idx)     returns( (elem_type) (1 << (bit_idx % ELEM_BITS))) {   return (elem_type) 1 << (bit_idx % ELEM_BITS); } MarkHillebrand Apr 16, 2011 at 10:54 AM Hi,   this is a "triggering problem", related to VCC's underlying handling of quantifiers. In this case, VCC / the underlying prover Z3 only find a trigger (also called "pattern") for the quantified variable "k" involving arithmetic (start + k), which are not handled too well. The warning below indicates this (it can be seen in the VCC output window in VS): ```Prover warning: using arith. in pattern (quantifier id: d2540611.54:17), the weight was increased to 5 (this value can be modified using PI_ARITH_WEIGHT=). Prover warning: using arith. in pattern (quantifier id: d2540611.54:17), the weight was increased to 5 (this value can be modified using PI_ARITH_WEIGHT=). ```   The problem is quite similar to this one: http://vcc.codeplex.com/discussions/251335. It should possible to fix it using manual triggers or restructuring the quantifiers. In this case, the "/oaf" (operators as functions) also helps, which to some extent improves the triggering on arithmetic situation. Pasted below is the example I've worked with.   HTH, Mark ```//`/oaf #include typedef unsigned long size_t; //__int32 typedef unsigned long elem_type; //__int32 #define NULL ((void*)0) #define CHAR_BIT (8) #define ELEM_BITS (sizeof (elem_type) * CHAR_BIT) //CHAR_BIT:= 8 ELEM_BITS=4*8=32 struct bitmap { size_t bit_cnt; /* Number of bits. */ elem_type *bits; /* Elements that represent bits. */ invariant(keeps(as_array(bits,(bit_cnt+ELEM_BITS-1)/ELEM_BITS))) invariant(bit_cnt>0 && is_malloc_root(this) // if i want to free bitmap && 1 /* TODO: not admissible, wrong size: is_malloc_root(as_array(bits, bit_cnt)) */ // if i want free bits array ) }; /* Returns the index of the element that contains the bit numbered BIT_IDX. */ ispure static inline size_t elem_idx (size_t bit_idx) returns(bit_idx/ELEM_BITS) { assert(ELEM_BITS>0); return bit_idx / ELEM_BITS; } /* Returns an elem_type where only the bit corresponding to BIT_IDX is turned on. */ ispure static inline elem_type bit_mask (size_t bit_idx) returns( (elem_type) (1 << (bit_idx % ELEM_BITS))) { return (elem_type) 1 << (bit_idx % ELEM_BITS); } bool bitmap_contains (const struct bitmap *b, size_t start, size_t cnt, bool value) requires(b!=NULL) requires((start + cnt )<= b->bit_cnt) requires(wrapped(b)) // TODO missing definitions: //ensures(!result <==> forall(size_t k;k>=0 && k exists(size_t k;k>=0 && k=0 && i<=cnt) invariant(forall(size_t k; k>=0 && kbits[elem_idx (start+k)] & bit_mask (start+k)) != 0) != value)) invariant(start+i<=b->bit_cnt) { idx=start+i; if (((b->bits[elem_idx (idx)] & bit_mask (idx)) != 0) == value) return true; } // TODO missing definitions: //assert(forall(size_t k;k>=0 && k