Documentation ¶
Index ¶
- func ExprString(e Expr) string
- func GetBVLen(e Expr) int
- func RegisterErrorHandler()
- type Expr
- type Solver
- func (s *Solver) Add(in string)
- func (s *Solver) AndExpr(left, right Expr) Expr
- func (s *Solver) AssertFormula(e Expr)
- func (s *Solver) BitVec(in string, bitWidth int) Expr
- func (s *Solver) BvAndExpr(left, right Expr) Expr
- func (s *Solver) BvConstExprFromInt(bitWidth int, value uint) Expr
- func (s *Solver) BvDivExpr(bitWidth int, dividend Expr, divisor Expr) Expr
- func (s *Solver) BvGeExpr(left, right Expr) Expr
- func (s *Solver) BvGtExpr(left, right Expr) Expr
- func (s *Solver) BvLShiftExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvLeExpr(left, right Expr) Expr
- func (s *Solver) BvLtExpr(left, right Expr) Expr
- func (s *Solver) BvMinusExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvModExpr(bitWidth int, dividend Expr, divisor Expr) Expr
- func (s *Solver) BvMultExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvNotExpr(child Expr) Expr
- func (s *Solver) BvOrExpr(left, right Expr) Expr
- func (s *Solver) BvPlusExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvRShiftExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvType(no_bits int) Type
- func (s *Solver) BvUMinusExpr(child Expr) Expr
- func (s *Solver) BvXorExpr(left, right Expr) Expr
- func (s *Solver) Destroy()
- func (s *Solver) EqExpr(child0 Expr, child1 Expr) Expr
- func (s *Solver) Eval(exp ast.Expr) Expr
- func (s *Solver) EvalBinaryExpr(exp *ast.BinaryExpr) Expr
- func (s *Solver) EvalUnaryExpr(exp *ast.UnaryExpr) Expr
- func (s *Solver) FalseExpr() Expr
- func (s *Solver) GetTermFromCounterExample(e Expr, c WholeCounterExample) Expr
- func (s *Solver) GetWholeCounterExample() WholeCounterExample
- func (s *Solver) H2i(in string) uint64
- func (s *Solver) ImpliesExpr(hyp Expr, conc Expr) Expr
- func (s *Solver) NotExpr(child Expr) Expr
- func (s *Solver) OrExpr(left, right Expr) Expr
- func (s *Solver) PrintAsserts(simplify_print int)
- func (s *Solver) PrintCounterExample()
- func (s *Solver) PrintQuery()
- func (s *Solver) Query(e Expr) int
- func (s *Solver) SH2i(in string) int64
- func (s *Solver) SSolve(vars ...Expr) []int64
- func (s *Solver) Solve(vars ...Expr) []uint64
- func (s *Solver) TrueExpr() Expr
- func (s *Solver) VarExpr(name string, typ Type) Expr
- func (s *Solver) XorExpr(left, right Expr) Expr
- type Type
- type VC
- type WholeCounterExample
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ExprString ¶
HIGH LEVEL API FUNCTIONS ExprString converts an Expr e into its string counterpart
func RegisterErrorHandler ¶
func RegisterErrorHandler()
SOLVER RELATED FUNCTIONS RegisterErrorHandler registers an error handler which triggers when there is an error in the C api
Types ¶
type Solver ¶
type Solver struct {
// contains filtered or unexported fields
}
func (*Solver) AssertFormula ¶
AssertFormula adds constraint e to the solver
func (*Solver) BitVec ¶
BitVec returns an Expr which is symbollic of string in with bit length bithWidth
func (*Solver) BvAndExpr ¶
BvAndExpr returns an Expr of bit length bitWidth between two Exprs left and right which are bitwise and
func (*Solver) BvConstExprFromInt ¶
BvConstExprFromInt returns an Expr of bit length bitWidth which is a constant of value
func (*Solver) BvDivExpr ¶
BvDivExpr returns an Expr of bit length bitWidth between two Exprs dividend and divisor which are divided
func (*Solver) BvLShiftExpr ¶
BvLShiftExpr returns an Expr of bit length bitWidth where left << right
func (*Solver) BvMinusExpr ¶
BVPlusExpr returns an Expr of bit length bitWidth between two Exprs left and right which are subtracted
func (*Solver) BvModExpr ¶
BvDivExpr returns an Expr of bit length bitWidth between two Exprs dividend and divisor which are in modulo
func (*Solver) BvMultExpr ¶
BvMultExpr returns an Expr of bit length bitWidth between two Exprs left and right which are multiplied
func (*Solver) BvOrExpr ¶
BvAndExpr returns an Expr of bit length bitWidth between two Exprs left and right which are bitwise or
func (*Solver) BvPlusExpr ¶
BVPlusExpr returns an Expr of bit length bitWidth between two Exprs left and right which are added
func (*Solver) BvRShiftExpr ¶
BvRShiftExpr returns an Expr of bit length bitWidth where left >> right
func (*Solver) BvType ¶
BITVECTOR RELATED FUNCTIONS BvType returns a type of bitwidth no_bits that could be used in VarExpr
func (*Solver) BvUMinusExpr ¶
BvUMinusExpr returns the arithmetic negation of Expr child
func (*Solver) BvXorExpr ¶
BvAndExpr returns an Expr of bit length bitWidth between two Exprs left and right which are bitwise xor
func (*Solver) Eval ¶
Eval recursively traverses the ast and returns the associated Expr form of the ast
func (*Solver) EvalBinaryExpr ¶
func (s *Solver) EvalBinaryExpr(exp *ast.BinaryExpr) Expr
EvalBinaryExpr returns an associated Expr which is representive of the BinaryExpr within an ast
func (*Solver) EvalUnaryExpr ¶
EvalUnaryExpr returns an associated Expr which is representive of the UnaryExpr within an ast
func (*Solver) GetTermFromCounterExample ¶
func (s *Solver) GetTermFromCounterExample(e Expr, c WholeCounterExample) Expr
GetTermFromCounterExample returns an Expr that is associated with Expr e from the WholeCounterExample c
func (*Solver) GetWholeCounterExample ¶
func (s *Solver) GetWholeCounterExample() WholeCounterExample
GetWholeCounterExample returns the full CounterExample that invalidates the Queried Expr
func (*Solver) ImpliesExpr ¶
ImpliesExpr returns an Expr where hyp implies conc
func (*Solver) PrintAsserts ¶
PrintAsserts prints to stdout the assertions made to the checker
func (*Solver) PrintCounterExample ¶
func (s *Solver) PrintCounterExample()
PrintCounterExample prints to stdout the CounterExample which invalidates the Queried Expr
func (*Solver) PrintQuery ¶
func (s *Solver) PrintQuery()
PrintQuery prints to stdout the most recent Query
func (*Solver) SSolve ¶
Signed solve evaluates the assertions which returns values of symbollic inputs vars in int form
func (*Solver) Solve ¶
Solve evaluates the assertions which returns values of symbollic inputs vars in int form
type WholeCounterExample ¶
type WholeCounterExample C.WholeCounterExample