Module Verify.Domain

valueAnalysis :: Analysis AType   

The CASS analysis to approximate result values.

emptyType :: AType   

Abstract representation of no possible value.

Further infos:

• solution complete, i.e., able to compute all solutions

isEmptyType :: AType -> Bool   

Does an abstract type represent no value?

Further infos:

• solution complete, i.e., able to compute all solutions

anyType :: AType   

Abstract representation of the type of all values.

Further infos:

• solution complete, i.e., able to compute all solutions

isAnyType :: AType -> Bool   

Does an abstract type represent any value?

Further infos:

• solution complete, i.e., able to compute all solutions

lubType :: AType -> AType -> AType   

Least upper bound of abstract values.

joinType :: AType -> AType -> AType   

Join two abstract values. The result is emptyType if they are not compatible.

aCons :: (String,String) -> [AType] -> AType   

The representation of a constructor application to a list of abstract argument types.

Further infos:

• solution complete, i.e., able to compute all solutions

aLit :: Literal -> AType   

litAsCons :: Literal -> (String,String)   

The representation of a literal as a constructor.

consOfType :: AType -> [(String,String)]   

The list of top-level constructors covered by an abstract type. The list is empty for anyType.

Further infos:

• solution complete, i.e., able to compute all solutions

argTypesOfCons :: (String,String) -> Int -> AType -> [AType]   

The argument types of an abstract type (given as the last argument) when it matches a given constructor/arity. For the top constructor domain, the arguments have always any type.

showType :: AType -> String   

Shows an abstract value.