1 /* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */
2 /* SPDX-License-Identifier: Apache-2.0 */
3 
4 /**
5  * @file s2n_socket_write_snapshot_harness.c
6  * @brief Implements the proof harness for s2n_socket_write_snapshot function.
7  */
8 
9 #include <utils/s2n_socket.h>
10 #include <cbmc_proof/make_common_datastructures.h>
11 
s2n_socket_write_snapshot_harness()12 void s2n_socket_write_snapshot_harness()
13 {
14   /* Non-deterministic inputs. */
15   struct s2n_connection *s2n_connection = malloc(sizeof(*s2n_connection));
16   if (s2n_connection != NULL) {
17     s2n_connection->send_io_context = cbmc_allocate_s2n_socket_write_io_context();
18   }
19 
20   /* Operation under verification. */
21   int result = s2n_socket_write_snapshot(s2n_connection);
22 
23   /* Post-condition. */
24   assert(S2N_IMPLIES(result == S2N_SUCCESS, s2n_connection->send_io_context != NULL));
25   assert(S2N_IMPLIES(s2n_connection == NULL, result != S2N_SUCCESS));
26 }
27