Open
Description
inline int memcmp(const char *s1, const char *s2, unsigned n)
{
int res = 0;
const unsigned char *sc1 = s1, *sc2 = s2;
for(; n != 0; n--)
// clang-format off
__CPROVER_loop_invariant(n <= __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))
__CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))
__CPROVER_loop_invariant(sc1 <= s1 + __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(sc2 <= s2 + __CPROVER_loop_entry(n))
__CPROVER_loop_invariant(res == 0)
__CPROVER_loop_invariant(sc1 -(const unsigned char*)s1 == sc2 -(const unsigned char*)s2
&& sc1 -(const unsigned char*)s1== __CPROVER_loop_entry(n) - n)
// clang-format on
{
res = (*sc1++) - (*sc2++);
long d1 = sc1 - (const unsigned char *)s1;
long d2 = sc2 - (const unsigned char *)s2;
if(res != 0)
return res;
}
return res;
}
int main()
{
unsigned SIZE;
__CPROVER_assume(1 < SIZE && SIZE < 65536);
unsigned char *a = malloc(SIZE);
unsigned char *b = malloc(SIZE);
memcpy(b, a, SIZE);
assert(memcmp(a, b, SIZE) == 0);
}CBMC version: 5.86.0
Operating system: check-vs-2019-cmake-build-and-test
Exact command line resulting in the issue: goto-instrument --dfcc main --apply-loop-contracts
What behaviour did you expect: ^VERIFICATION SUCCESSFUL$
What happened instead: This test passes under ubuntu and macos, but failed the CI check check-vs-2019-cmake-build-and-test and check-vs-2022-make-build-and-test with the following errors.
...
156: Instrumenting 'malloc'
156: Instrumenting 'memcpy'
156: Instrumenting '_errno'
156: --- begin invariant violation report ---
156: Invariant check failed
156: File: D:\a\cbmc\cbmc\src\goto-instrument\contracts\dynamic-frames\dfcc_instrument.cpp:330 function: dfcc_instrumentt::instrument_function
156: Condition: Precondition
156: Reason: found != goto_model.goto_functions.function_map.end()
156: Backtrace:
156: 0 0x 0
156: 1 0x 0
156: 2 0x 0
156: 3 0x 0
156: 4 0x 0
156: 5 0x 0
156: 6 0x 0
156: 7 0x 0
156: 8 0x 0
156: 9 0x 0
156: a 0x 0
156: b 0x 0
156: c 0x 0
156: d 0x7ffb490b7ab0 BaseThreadInitThunk
156: e 0x7ffb4ac6a330 RtlUserThreadStart
156:
156: Diagnostics:
156: << EXTRA DIAGNOSTICS >>
156: Function '_errno' must exist in the model.
156: << END EXTRA DIAGNOSTICS >>
156:
156: --- end invariant violation report ---
156:
156: EXIT=127
156: SIGNAL=0