mirror of
https://github.com/uroni/urbackup_backend.git
synced 2025-10-26 11:36:50 +00:00
160 lines
8.8 KiB
C
Executable File
160 lines
8.8 KiB
C
Executable File
#ifndef AWS_COMMON_ASSERT_H
|
|
#define AWS_COMMON_ASSERT_H
|
|
|
|
/*
|
|
* Copyright 2010-2018 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.
|
|
*/
|
|
|
|
#include <aws/common/exports.h>
|
|
#include <aws/common/macros.h>
|
|
#include <stdio.h>
|
|
|
|
AWS_EXTERN_C_BEGIN
|
|
|
|
AWS_COMMON_API
|
|
AWS_DECLSPEC_NORETURN
|
|
void aws_fatal_assert(const char *cond_str, const char *file, int line) AWS_ATTRIBUTE_NORETURN;
|
|
|
|
AWS_EXTERN_C_END
|
|
|
|
#if defined(CBMC)
|
|
# define AWS_ASSUME(cond) __CPROVER_assume(cond)
|
|
#elif defined(_MSC_VER)
|
|
# define AWS_ASSUME(cond) __assume(cond)
|
|
# define AWS_UNREACHABLE() __assume(0)
|
|
#elif defined(__clang__)
|
|
# define AWS_ASSUME(cond) \
|
|
do { \
|
|
bool _result = (cond); \
|
|
__builtin_assume(_result); \
|
|
} while (false)
|
|
# define AWS_UNREACHABLE() __builtin_unreachable()
|
|
#elif defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 5))
|
|
# define AWS_ASSUME(cond) ((cond) ? (void)0 : __builtin_unreachable())
|
|
# define AWS_UNREACHABLE() __builtin_unreachable()
|
|
#else
|
|
# define AWS_ASSUME(cond)
|
|
# define AWS_UNREACHABLE()
|
|
#endif
|
|
|
|
#if defined(CBMC)
|
|
# include <assert.h>
|
|
# define AWS_ASSERT(cond) assert(cond)
|
|
#elif defined(DEBUG_BUILD) || __clang_analyzer__
|
|
# define AWS_ASSERT(cond) AWS_FATAL_ASSERT(cond)
|
|
#else
|
|
# define AWS_ASSERT(cond)
|
|
#endif /* defined(CBMC) */
|
|
|
|
#if defined(CBMC)
|
|
# define AWS_FATAL_ASSERT(cond) AWS_ASSERT(cond)
|
|
#elif __clang_analyzer__
|
|
# define AWS_FATAL_ASSERT(cond) \
|
|
if (!(cond)) { \
|
|
abort(); \
|
|
}
|
|
#else
|
|
# if defined(_MSC_VER)
|
|
# define AWS_FATAL_ASSERT(cond) \
|
|
__pragma(warning(push)) __pragma(warning(disable : 4127)) /* conditional expression is constant */ \
|
|
if (!(cond)) { \
|
|
aws_fatal_assert(#cond, __FILE__, __LINE__); \
|
|
} \
|
|
__pragma(warning(pop))
|
|
# else
|
|
# define AWS_FATAL_ASSERT(cond) \
|
|
if (!(cond)) { \
|
|
aws_fatal_assert(#cond, __FILE__, __LINE__); \
|
|
}
|
|
# endif /* defined(_MSC_VER) */
|
|
#endif /* defined(CBMC) */
|
|
|
|
/**
|
|
* Define function contracts.
|
|
* When the code is being verified using CBMC these contracts are formally verified;
|
|
* When the code is built in debug mode, they are checked as much as possible using assertions
|
|
* When the code is built in production mode, non-fatal contracts are not checked.
|
|
* Violations of the function contracts are undefined behaviour.
|
|
*/
|
|
#ifdef CBMC
|
|
# define AWS_PRECONDITION2(cond, explanation) __CPROVER_precondition((cond), (explanation))
|
|
# define AWS_PRECONDITION1(cond) __CPROVER_precondition((cond), # cond " check failed")
|
|
# define AWS_FATAL_PRECONDITION2(cond, explanation) __CPROVER_precondition((cond), (explanation))
|
|
# define AWS_FATAL_PRECONDITION1(cond) __CPROVER_precondition((cond), # cond " check failed")
|
|
# define AWS_POSTCONDITION2(cond, explanation) __CPROVER_assert((cond), (explanation))
|
|
# define AWS_POSTCONDITION1(cond) __CPROVER_assert((cond), # cond " check failed")
|
|
# define AWS_FATAL_POSTCONDITION2(cond, explanation) __CPROVER_assert((cond), (explanation))
|
|
# define AWS_FATAL_POSTCONDITION1(cond) __CPROVER_assert((cond), # cond " check failed")
|
|
#else
|
|
# define AWS_PRECONDITION2(cond, expl) AWS_ASSERT(cond)
|
|
# define AWS_PRECONDITION1(cond) AWS_ASSERT(cond)
|
|
# define AWS_FATAL_PRECONDITION2(cond, expl) AWS_FATAL_ASSERT(cond)
|
|
# define AWS_FATAL_PRECONDITION1(cond) AWS_FATAL_ASSERT(cond)
|
|
# define AWS_POSTCONDITION2(cond, expl) AWS_ASSERT(cond)
|
|
# define AWS_POSTCONDITION1(cond) AWS_ASSERT(cond)
|
|
# define AWS_FATAL_POSTCONDITION2(cond, expl) AWS_FATAL_ASSERT(cond)
|
|
# define AWS_FATAL_POSTCONDITION1(cond) AWS_FATAL_ASSERT(cond)
|
|
#endif /* CBMC */
|
|
|
|
/* the C runtime does not give a way to check these properties,
|
|
* but we can at least check that the pointer is valid.
|
|
* these macros are intended to be used with CBMC proofs, but will not use CBMC
|
|
* intrinsics until https://github.com/diffblue/cbmc/issues/5194 is fixed.*/
|
|
#define AWS_MEM_IS_READABLE(base, len) (((len) == 0) || (base))
|
|
#define AWS_MEM_IS_WRITABLE(base, len) (((len) == 0) || (base))
|
|
|
|
#define __CPROVER_r_ok(base, len) (AWS_MEM_IS_READABLE(base, len))
|
|
#define __CPROVER_w_ok(base, len) (AWS_MEM_IS_WRITEABLE(base, len))
|
|
|
|
#define AWS_RETURN_ERROR_IF_IMPL(type, cond, err, explanation) \
|
|
do { \
|
|
if (!(cond)) { \
|
|
return aws_raise_error(err); \
|
|
} \
|
|
} while (0)
|
|
|
|
#define AWS_RETURN_ERROR_IF3(cond, err, explanation) AWS_RETURN_ERROR_IF_IMPL("InternalCheck", cond, err, explanation)
|
|
#define AWS_RETURN_ERROR_IF2(cond, err) AWS_RETURN_ERROR_IF3(cond, err, #cond " check failed")
|
|
#define AWS_RETURN_ERROR_IF(...) CALL_OVERLOAD(AWS_RETURN_ERROR_IF, __VA_ARGS__)
|
|
|
|
#define AWS_ERROR_PRECONDITION3(cond, err, explanation) AWS_RETURN_ERROR_IF_IMPL("Precondition", cond, err, explanation)
|
|
#define AWS_ERROR_PRECONDITION2(cond, err) AWS_ERROR_PRECONDITION3(cond, err, #cond " check failed")
|
|
#define AWS_ERROR_PRECONDITION1(cond) AWS_ERROR_PRECONDITION2(cond, AWS_ERROR_INVALID_ARGUMENT)
|
|
|
|
#define AWS_ERROR_POSTCONDITION3(cond, err, explanation) \
|
|
AWS_RETURN_ERROR_IF_IMPL("Postcondition", cond, err, explanation)
|
|
#define AWS_ERROR_POSTCONDITION2(cond, err) AWS_ERROR_POSTCONDITION3(cond, err, #cond " check failed")
|
|
#define AWS_ERROR_POSTCONDITION1(cond) AWS_ERROR_POSTCONDITION2(cond, AWS_ERROR_INVALID_ARGUMENT)
|
|
|
|
// The UNUSED is used to silence the complains of GCC for zero arguments in variadic macro
|
|
#define AWS_PRECONDITION(...) CALL_OVERLOAD(AWS_PRECONDITION, __VA_ARGS__)
|
|
#define AWS_FATAL_PRECONDITION(...) CALL_OVERLOAD(AWS_FATAL_PRECONDITION, __VA_ARGS__)
|
|
#define AWS_POSTCONDITION(...) CALL_OVERLOAD(AWS_POSTCONDITION, __VA_ARGS__)
|
|
#define AWS_FATAL_POSTCONDITION(...) CALL_OVERLOAD(AWS_FATAL_POSTCONDITION, __VA_ARGS__)
|
|
#define AWS_ERROR_PRECONDITION(...) CALL_OVERLOAD(AWS_ERROR_PRECONDITION, __VA_ARGS__)
|
|
#define AWS_ERROR_POSTCONDITION(...) CALL_OVERLOAD(AWS_ERROR_PRECONDITION, __VA_ARGS__)
|
|
|
|
#define AWS_RETURN_WITH_POSTCONDITION(_rval, ...) \
|
|
do { \
|
|
AWS_POSTCONDITION(__VA_ARGS__); \
|
|
return _rval; \
|
|
} while (0)
|
|
|
|
#define AWS_SUCCEED_WITH_POSTCONDITION(...) AWS_RETURN_WITH_POSTCONDITION(AWS_OP_SUCCESS, __VA_ARGS__)
|
|
|
|
#define AWS_OBJECT_PTR_IS_READABLE(ptr) AWS_MEM_IS_READABLE((ptr), sizeof(*(ptr)))
|
|
#define AWS_OBJECT_PTR_IS_WRITABLE(ptr) AWS_MEM_IS_WRITABLE((ptr), sizeof(*(ptr)))
|
|
|
|
#endif /* AWS_COMMON_ASSERT_H */
|