1 /**
2  * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3  * SPDX-License-Identifier: Apache-2.0.
4  */
5 
6 #define DEST_TYPE uint16_t
7 #define BYTE_WIDTH 2
8 #define BYTE_CURSOR_READ aws_byte_cursor_read_be16
9 #define AWS_NTOH aws_ntoh16
10 
11 #include <proof_helpers/aws_byte_cursor_read_common.h>
12 
aws_byte_cursor_read_be16_harness()13 void aws_byte_cursor_read_be16_harness() {
14     aws_byte_cursor_read_common_harness();
15 }
16