Goose  Artifact [bc804e690d]

Artifact bc804e690da5a0e57f6912300ecea9072fedb828adc78d72d641cffed981522c:

• File bs/verify/value.h — part of check-in [98739f02b6] at 2020-06-01 18:39:30 on branch trunk — Verifier: go through the LowerConstantForVerification extension point when building a constant expression. (user: achavasse size: 967)

#ifndef GOOSE_VERIFY_VALUE_H
#define GOOSE_VERIFY_VALUE_H

#include "z3++.h"
#include "llr/llr.h"

namespace goose::verify
{
    struct Z3Val
    {
        z3::expr expr;
        ir::Value type;
    };

    extern optional< Z3Val > BuildZ3ValFromConstant( const sema::Context& c, const Value& val );
    extern optional< Z3Val > BuildZ3ExprFromValue( Builder& b, const Value& val );
    extern optional< Z3Val > BuildZ3ConstantFromType( const sema::Context& c, const Value& type, const string& name );
    extern optional< Z3Val > BuildZ3ConstantFromType( const sema::Context& c, const Term& type, const string& name );
    extern optional< Z3Val > BuildZ3Op( Builder& b, const llr::Instruction& instr );

    extern z3::expr GetAsBitVec( const z3::expr& expr, const Value& type );
    extern z3::expr GetAsBitVec( const Z3Val& zv );

    extern z3::expr GetAsInt( const z3::expr& expr, const Value& type );
    extern z3::expr GetAsInt( const Z3Val& zv );
}

#endif