Qinheping Hu

> Is this intended for use with CBMC only, or for inclusion in release versions of the kernel? It is not CBMC-use only. This PR include an array-based implementation of...

DO NOT MERGE. It is a proposal for array-based implementation.

The error message indicates that the synthesizer failed to synthesize a new assign target---the memory location that are going to be written during the loops---, while it found that the...

An attempt fix of this issue: https://github.com/awslabs/aws-c-common/pull/1057. The same failure is also observed in s2n-tls: https://github.com/aws/s2n-tls/pull/4223

@celinval I remove implementation detail as it was too much for RFC; and add more open questions.

This feature will unblock https://github.com/model-checking/verify-rust-std/pull/131, https://github.com/model-checking/verify-rust-std/pull/130, and https://github.com/model-checking/verify-rust-std/pull/129.

> @qinheping since we are using both `--dfcc` and`--apply-loop-contract`and we also want to have `--unwind 50`, is there a way we can resolve this conflict? Could you try to identify...

> @qinheping currently there's no non-built-in loops left, the only one not related to dfcc is `memcpy` but I suppose the CBMC version of it one should be unbounded already?...

> Is the unbounded version of `memcmp` something that's in development or is there any issue with applying loop contract to it? We don't have any plan for unbounded version...

In other words, if a loop returns or breaks in the middle of an iteration, does CBMC not check the invariant for this last iteration? No, CBMC doesn't check if...