Documentation
¶
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type Branch ¶
type Branch interface {
// Instr returns ssa.Instruction value for the branch.
Instr() ssa.Instruction
// To returns ssa.BasicBlock that the branch took.
To() *ssa.BasicBlock
// Other returns ssa.BasicBlock that the branch did not take.
Other() *ssa.BasicBlock
}
Branch represents a branch appeared in a running trace. This includes instructions that may cause a panic (e.g., pointer dereference) as well as ordinary branching by *ssa.If.
type BranchDeref ¶
type BranchDeref struct {
// contains filtered or unexported fields
}
BranchDeref represents a branching (success or panic) caused by dereference (*ssa.UnOp or *ssa.FieldAddr).
func (*BranchDeref) Instr ¶
func (b *BranchDeref) Instr() ssa.Instruction
Instr returns ssa.Instruction value for the branch.
func (*BranchDeref) Other ¶
func (b *BranchDeref) Other() *ssa.BasicBlock
Other returns ssa.BasicBlock that the branch did not take.
func (*BranchDeref) To ¶
func (b *BranchDeref) To() *ssa.BasicBlock
To returns ssa.BasicBlock that the branch took.
type BranchIf ¶
type BranchIf struct {
// contains filtered or unexported fields
}
BranchIf contains a branching instruction (*ssa.If) and the direction taken in the concolic execution.
func (*BranchIf) Instr ¶
func (b *BranchIf) Instr() ssa.Instruction
Instr returns ssa.Instruction value for the branch.
func (*BranchIf) Other ¶
func (b *BranchIf) Other() *ssa.BasicBlock
Other returns ssa.BasicBlock that the branch did not take.
func (*BranchIf) To ¶
func (b *BranchIf) To() *ssa.BasicBlock
To returns ssa.BasicBlock that the branch took.
type Definite ¶
type Definite struct {
// contains filtered or unexported fields
}
Definite represents a solution. If ty is *types.Pointer, then the value is an instance of Solution which represents the referenced value.
func (Definite) Concretize ¶
Concretize returns the value.
type Indefinite ¶
type Indefinite struct {
// contains filtered or unexported fields
}
Indefinite represents an indefinite solution.
func NewIndefinite ¶
func NewIndefinite(ty types.Type) Indefinite
NewIndefinite returns a new indefinite solution.
func (Indefinite) Concretize ¶
func (s Indefinite) Concretize(f func(types.Type) interface{}) interface{}
Concretize returns the value.
type UnsatError ¶
type UnsatError struct{}
UnsatError is an error describing that Z3 constraints were unsatisfied.
func (UnsatError) Error ¶
func (ue UnsatError) Error() string
type Z3Solver ¶
type Z3Solver struct {
// contains filtered or unexported fields
}
Z3Solver is a type that holds the Z3 context, assertions, and symbols.
func CreateZ3Solver ¶
func CreateZ3Solver(symbols []ssa.Value, instrs []ssa.Instruction, isComplete bool) (*Z3Solver, error)
CreateZ3Solver returns a new Z3Solver.
func (*Z3Solver) NumBranches ¶
NumBranches returns the number of branch instructions.
Source Files