1#ifndef AWS_COMMON_PREDICATES_H
2#define AWS_COMMON_PREDICATES_H
3/*
4 * Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
5 *
6 * Licensed under the Apache License, Version 2.0 (the "License").
7 * You may not use this file except in compliance with the License.
8 * A copy of the License is located at
9 *
10 * http://aws.amazon.com/apache2.0
11 *
12 * or in the "license" file accompanying this file. This file is distributed
13 * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
14 * express or implied. See the License for the specific language governing
15 * permissions and limitations under the License.
16 */
17
18/**
19 * Returns whether all bytes of the two byte arrays match.
20 */
21#if (AWS_DEEP_CHECKS == 1)
22# ifdef CBMC
23/* clang-format off */
24# define AWS_BYTES_EQ(arr1, arr2, len) \
25 __CPROVER_forall { \
26 int i; \
27 (i >= 0 && i < len) ==> ((const uint8_t *)&arr1)[i] == ((const uint8_t *)&arr2)[i] \
28 }
29/* clang-format on */
30# else
31# define AWS_BYTES_EQ(arr1, arr2, len) (memcmp(arr1, arr2, len) == 0)
32# endif /* CBMC */
33#else
34# define AWS_BYTES_EQ(arr1, arr2, len) (1)
35#endif /* (AWS_DEEP_CHECKS == 1) */
36
37#endif /* AWS_COMMON_PREDICATES_H */
38