error VC8007: the value of 'result' changed (in reads check of 'memcmp')

Apr 4, 2011 at 12:48 AM
Edited Apr 4, 2011 at 12:49 AM

What does the error message "error VC8007: the value of 'result' changed (in reads check of 'memcmp')" mean with respect to the following:

#include <vcc.h>

_(pure) int memcmp(const unsigned char *bv1, const unsigned char *bv2, size_t n)
	_(requires \thread_local_array(bv1, n))
	_(requires \thread_local_array(bv2, n))
	_(reads \array_range(bv1, n), \array_range(bv2, n))
	_(ensures \result > 0 <==> (\exists size_t j; j < n && (\forall size_t k; k < j ==> bv1[k] == bv2[k]) && (((int) bv1[j]) - bv2[j]) > 0))
	_(ensures \result < 0 <==> (\exists size_t j; j < n && (\forall size_t k; k < j ==> bv1[k] == bv2[k]) && (((int) bv1[j]) - bv2[j]) < 0))
	_(ensures \result == 0 <==> (\forall size_t j; j < n ==> bv1[j] == bv2[j]))
	;

int main()
{
}

(I am using VCC 2.1.40403.0.)

Daniel

Coordinator
Apr 4, 2011 at 8:41 PM

Hi Daniel,

  _(reads ...) clauses are meant to specify the heap memory that a function accesses. For pure functions with reads clauses, VCC can optionally generate a frame axiom stating that the function returns the same result given that the memory that is read is the same. The "reads check" checks the validity of the reads clause, which is what fails above (this might be a triggering problem, again). If you don't need the frame axiom (probably you don't at this point), than you can effectively disable the reads check by stating "_(reads \universe())" (the universal reads clause) instead of the reads clause you give above.

  You can find some more info here: http://vcc.codeplex.com/wikipage?title=Pure%20functions&referringTitle=Documentation Beware though, that some of the details have changed, and this page would need an update...

  Hope this helps, Mark