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