// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: MIT-0

/*
 * Insert copyright notice
 */

/**
 * @file <__FUNCTION_NAME__>_harness.c
 * @brief Implements the proof harness for <__FUNCTION_NAME__> function.
 */

/*
 * Insert project header files that
 *   - include the declaration of the function
 *   - include the types needed to declare function arguments
 */

/**
 * @brief Starting point for formal analysis
 * 
 */
void harness(void)
{

  /* Insert argument declarations */

  <__FUNCTION_NAME__>( /* Insert arguments */ );
}