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()12void 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