forgetunlock

Documentation

Index

• Variables
• func CompareTwoMaps(map1 map[string]bool, map2 map[string]bool) bool
• func ConvertCondsToContraints(conds []stCond) string
• func Detect()
• func GenKillAnalysis(inputFn *ssa.Function)
• func GetLiveMutex(inputInst ssa.Instruction) map[string]bool
• func HandleBinOp(pBinOp *ssa.BinOp) string
• func HandleCall(pCall *ssa.Call) string
• func HandleVarOrInst(pValue ssa.Value) string
• func InitBeforeAfterMap(inputFn *ssa.Function)
• func InitGenKillMap(inputFn *ssa.Function)
• func Initialize()
• func IsDominatedbyShutdown(inputInst ssa.Instruction) bool
• func SearchDeferredUnlock(inputInst ssa.Instruction) []string
• type Assert
• type StSMTSet
  • func Conds2SMTSet(vecCond []stCond) (result *StSMTSet)

Variables

var (
	SMTBool      = "Bool"
	SMTEQL       = "="
	SMTNot       = "not"
	DefaultSorts = []string{"byte", "int", "int64", "bool", "string"}
)

var AnalyzedFNs map[string]bool

var Bugs []ssa.Instruction

var (
	CountSMTSet = 0
)

var FNOnlyContainUnlock map[string]string

Functions

func CompareTwoMaps

func CompareTwoMaps(map1 map[string]bool, map2 map[string]bool) bool

func ConvertCondsToContraints

func ConvertCondsToContraints(conds []stCond) string

func Detect

func Detect()

func GenKillAnalysis

func GenKillAnalysis(inputFn *ssa.Function)

func GetLiveMutex

func GetLiveMutex(inputInst ssa.Instruction) map[string]bool

func HandleBinOp

func HandleBinOp(pBinOp *ssa.BinOp) string

func HandleCall

func HandleCall(pCall *ssa.Call) string

func HandleVarOrInst

func HandleVarOrInst(pValue ssa.Value) string

func InitBeforeAfterMap

func InitBeforeAfterMap(inputFn *ssa.Function)

func InitGenKillMap

func InitGenKillMap(inputFn *ssa.Function)

func Initialize

func Initialize()

func IsDominatedbyShutdown

func IsDominatedbyShutdown(inputInst ssa.Instruction) bool

func SearchDeferredUnlock

func SearchDeferredUnlock(inputInst ssa.Instruction) []string

Types

type Assert

type Assert string

type StSMTSet

type StSMTSet struct {
	DecSorts    []stDecSort
	DecFns      []stDecFn
	DefineSorts []stDefineSort
	DecConsts   []stDecConst
	Asserts     []Assert
	FinalConst  stDecConst
	FinalAssert Assert
	Todo        []ssa.Value
	Status      string
	Index       int
}

func Conds2SMTSet

func Conds2SMTSet(vecCond []stCond) (result *StSMTSet)