DFCC loop contracts crashes with VS

[qinheping]

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

[remi-delmas-3000]

Hi, this seems to be caused by a missing function definition for _errno, I see that the CPROVER library provides a definition for _errno, seems like loading the CPROVER library does not load this particular function. Do you know why is _errno pulled in the model in the first place ?

[qinheping]

No. I need to setup Visual Studio environment to further debug it.