1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
/*
* 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();
|
