#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"));
}