81 lines
3.3 KiB
C++
81 lines
3.3 KiB
C++
#include <catch2/catch_test_macros.hpp>
|
|
|
|
#include "fold/symbolic/encoder_callee_predicates.hpp"
|
|
|
|
using fold::symbolic::isAssertCall;
|
|
using fold::symbolic::isContractAssumeCall;
|
|
using fold::symbolic::isFreeCall;
|
|
using fold::symbolic::isMallocLikeCall;
|
|
using fold::symbolic::isNonNullAssumeCall;
|
|
|
|
TEST_CASE("isMallocLikeCall matches the modeled allocators",
|
|
"[encoder][callee_predicates][malloc]") {
|
|
REQUIRE(isMallocLikeCall("malloc"));
|
|
REQUIRE(isMallocLikeCall("calloc"));
|
|
REQUIRE(isMallocLikeCall("alloca"));
|
|
REQUIRE(isMallocLikeCall("_alloca"));
|
|
REQUIRE(isMallocLikeCall("__builtin_alloca"));
|
|
}
|
|
|
|
TEST_CASE("isMallocLikeCall rejects similar but distinct callees",
|
|
"[encoder][callee_predicates][malloc]") {
|
|
REQUIRE_FALSE(isMallocLikeCall(""));
|
|
REQUIRE_FALSE(isMallocLikeCall("realloc"));
|
|
REQUIRE_FALSE(isMallocLikeCall("memalign"));
|
|
REQUIRE_FALSE(isMallocLikeCall("posix_memalign"));
|
|
REQUIRE_FALSE(isMallocLikeCall("free"));
|
|
REQUIRE_FALSE(isMallocLikeCall("malloc_usable_size"));
|
|
REQUIRE_FALSE(isMallocLikeCall("Malloc")); // case sensitive
|
|
}
|
|
|
|
TEST_CASE("isFreeCall is exact-match", "[encoder][callee_predicates][free]") {
|
|
REQUIRE(isFreeCall("free"));
|
|
REQUIRE_FALSE(isFreeCall(""));
|
|
REQUIRE_FALSE(isFreeCall("Free"));
|
|
REQUIRE_FALSE(isFreeCall("_free"));
|
|
REQUIRE_FALSE(isFreeCall("free_all"));
|
|
REQUIRE_FALSE(isFreeCall("delete"));
|
|
}
|
|
|
|
TEST_CASE("isAssertCall covers C/C++ assert family across platforms",
|
|
"[encoder][callee_predicates][assert]") {
|
|
REQUIRE(isAssertCall("assert"));
|
|
REQUIRE(isAssertCall("__assert"));
|
|
REQUIRE(isAssertCall("__assert_rtn")); // macOS
|
|
REQUIRE(isAssertCall("__assert_fail")); // glibc
|
|
REQUIRE(isAssertCall("__assert2")); // glibc variant
|
|
REQUIRE(isAssertCall("_assert")); // Windows debug runtime
|
|
REQUIRE(isAssertCall("_wassert")); // Windows wide-char variant
|
|
}
|
|
|
|
TEST_CASE("isAssertCall rejects unrelated callees", "[encoder][callee_predicates][assert]") {
|
|
REQUIRE_FALSE(isAssertCall(""));
|
|
REQUIRE_FALSE(isAssertCall("ASSERT"));
|
|
REQUIRE_FALSE(isAssertCall("assert_eq"));
|
|
REQUIRE_FALSE(isAssertCall("DEBUGASSERT")); // curl's macro — expands TO assert,
|
|
// but isn't itself a callee name
|
|
// the encoder sees.
|
|
REQUIRE_FALSE(isAssertCall("abort"));
|
|
REQUIRE_FALSE(isAssertCall("static_assert"));
|
|
}
|
|
|
|
TEST_CASE("isContractAssumeCall recognizes generic contract predicates",
|
|
"[encoder][callee_predicates][contract]") {
|
|
REQUIRE(isContractAssumeCall("assert"));
|
|
REQUIRE(isContractAssumeCall("Expects"));
|
|
REQUIRE(isContractAssumeCall("Ensures"));
|
|
REQUIRE(isContractAssumeCall("FOLD_ASSERT"));
|
|
REQUIRE(isContractAssumeCall("FOLD_PRECONDITION"));
|
|
REQUIRE(isContractAssumeCall("FOLD_POSTCONDITION"));
|
|
REQUIRE(isContractAssumeCall("FOLD_DCHECK"));
|
|
REQUIRE_FALSE(isContractAssumeCall("observe"));
|
|
}
|
|
|
|
TEST_CASE("isNonNullAssumeCall recognizes Fold-local non-null contracts",
|
|
"[encoder][callee_predicates][nonnull-assume]") {
|
|
REQUIRE(isNonNullAssumeCall("fold_assume_nonnull"));
|
|
REQUIRE(isNonNullAssumeCall("FOLD_ASSUME_NONNULL"));
|
|
REQUIRE(isNonNullAssumeCall("__fold_assume_nonnull"));
|
|
REQUIRE_FALSE(isNonNullAssumeCall("assume"));
|
|
REQUIRE_FALSE(isNonNullAssumeCall("assert"));
|
|
}
|