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 | |