#pragma once

#include <cstdint>
#include <utility>
#include <memory>
#include <string>

#include <brick-assert>
#include <brick-except>

DIVINE_RELAX_WARNINGS
#include <llvm/IR/LLVMContext.h>
#include <llvm/IR/Module.h>
#include <llvm/Support/Casting.h>
DIVINE_UNRELAX_WARNINGS

// The infrastructure common to the whole SHOOP. Also a single place to define various constants
// and an index of general purpose includes.

namespace shoop
{

using ctx_ptr = std::shared_ptr< llvm::LLVMContext >;
using mod_ptr = std::unique_ptr< llvm::Module >;

// This is the name for a function used as a DiOS entrypoint. The function that is tested
// during a specific Divine invocation is called from it.
//
// See also:
// - dios/config/static.cpp
constexpr const char *test_runner_name = "__tester";

// This is the name of the pointer in the verified module that acts as a pointer to
// an array of bytes representing the current precondition.
constexpr const char *precondition_var_name = "__precondition";

struct cli_error : brq::error
{
    using brq::error::error;
};

inline void die( const std::string &reason, int exit_code = 1 )
{
    brq::raise< cli_error >( exit_code ) << reason;
}

}