/*
 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 *
 * Licensed under the Apache License, Version 2.0 (the "License"). You may not use
 * this file except in compliance with the License. A copy of the License is
 * located at
 *
 *     http://aws.amazon.com/apache2.0/
 *
 * or in the "license" file accompanying this file. This file is distributed on an
 * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
 * implied. See the License for the specific language governing permissions and
 * limitations under the License.
 */

#pragma once

#include <stdbool.h>
#include <stddef.h>
#include <stdint.h>
#include <sys/stat.h>
#include <sys/types.h>

/**
 * These functions provide a way to get unconstrained values of the correct types for use in CBMC proofs
 * CBMC treats any function which does not have a body as returning an unconstrained value.
 * For example, each call to nondet_uint8_t() will return a different unconstrained value which can be used
 * in CBMC proofs.
 */
bool         nondet_bool();
int          nondet_int();
unsigned int nondet_unsigned_int();
size_t       nondet_size_t();
long         nondet_long();
uint16_t     nondet_uint16_t();
uint32_t     nondet_uint32_t();
uint64_t     nondet_uint64_t();
uint8_t      nondet_uint8_t();
void *       nondet_voidp();
off_t        nondet_off_t();
ssize_t      nondet_ssize_t();