AbsBasilIR (basil_ast.BasilIR.AbsBasilIR)

type bVTYPE =

| BVTYPE of (int * int) * string

and iNTTYPE =

| INTTYPE of (int * int) * string

and bOOLTYPE =

| BOOLTYPE of (int * int) * string

and bIdent =

| BIdent of (int * int) * string

and localIdent =

| LocalIdent of (int * int) * string

and globalIdent =

| GlobalIdent of (int * int) * string

and blockIdent =

| BlockIdent of (int * int) * string

and procIdent =

| ProcIdent of (int * int) * string

and beginList =

| BeginList of (int * int) * string

and endList =

| EndList of (int * int) * string

and beginRec =

| BeginRec of (int * int) * string

and endRec =

| EndRec of (int * int) * string

and lambdaSep =

| LambdaSep of string

and str =

| Str of string

and integerHex =

| IntegerHex of (int * int) * string

and integerDec =

| IntegerDec of (int * int) * string

and moduleT =

| Module1 of decl list

and semicolons =

| Semicolons_Empty
| Semicolons_Some of semicolons

and decl =

| Decl_Axiom of attribSet * expr
| Decl_SharedMem of globalIdent * typeT
| Decl_UnsharedMem of globalIdent * typeT
| Decl_Var of globalIdent * typeT
| Decl_UninterpFun of attribSet * globalIdent * typeT list * typeT
| Decl_Fun of attribSet * globalIdent * params list * typeT * expr
| Decl_ProgEmpty of procIdent * attribSet
| Decl_ProgWithSpec of procIdent * attribSet * beginList * progSpec list * endList
| Decl_Proc of procIdent * params list * params list * attribSet * funSpec list * procDef

and procDef =

| ProcDef_Empty
| ProcDef_Some of beginList * block list * endList

and intType =

| IntType1 of iNTTYPE

and boolType =

| BoolType1 of bOOLTYPE

and mapType =

| MapType1 of typeT * typeT

and bVType =

| BVType1 of bVTYPE

and typeT =

| TypeIntType of intType
| TypeBoolType of boolType
| TypeMapType of mapType
| TypeBVType of bVType

and intVal =

| IntVal_Hex of integerHex
| IntVal_Dec of integerDec

and bVVal =

| BVVal1 of intVal * bVType

and endian =

| Endian_Little
| Endian_Big

and assignment =

| Assignment1 of lVar * expr

and stmt =

| Stmt_SingleAssign of assignment
| Stmt_MultiAssign of assignment list
| Stmt_Load of lVar * endian * globalIdent * expr * intVal
| Stmt_Store of endian * globalIdent * expr * expr * intVal
| Stmt_DirectCall of lVars * procIdent * expr list
| Stmt_IndirectCall of expr
| Stmt_Assume of expr
| Stmt_Guard of expr
| Stmt_Assert of expr

and localVar =

| LocalVar1 of localIdent * typeT

and globalVar =

| GlobalVar1 of globalIdent * typeT

and lVars =

| LVars_Empty
| LVars_LocalList of localVar list
| LVars_List of lVar list

and jump =

| Jump_GoTo of blockIdent list
| Jump_Unreachable
| Jump_Return of expr list

and lVar =

| LVar_Local of localVar
| LVar_Global of globalVar

and stmtWithAttrib =

| StmtWithAttrib1 of stmt * attribSet

and jumpWithAttrib =

| JumpWithAttrib1 of jump * attribSet

and block =

| Block1 of blockIdent * attribSet * beginList * stmtWithAttrib list * jumpWithAttrib * endList

and attrKeyValue =

| AttrKeyValue1 of bIdent * attr

and attribSet =

| AttribSet_Some of beginRec * attrKeyValue list * semicolons * endRec
| AttribSet_Empty

and attr =

| Attr_Map of beginRec * attrKeyValue list * semicolons * endRec
| Attr_List of beginList * attr list * endList
| Attr_Lit of value
| Attr_Str of str

and params =

| Params1 of localIdent * typeT

and value =

| Value_BV of bVVal
| Value_Int of intVal
| Value_True
| Value_False

and expr =

| Expr_Literal of value
| Expr_Local of localVar
| Expr_Global of globalVar
| Expr_Forall of lambdaDef
| Expr_Exists of lambdaDef
| Expr_Old of expr
| Expr_FunctionOp of globalIdent * expr list
| Expr_Binary of binOp * expr * expr
| Expr_Assoc of boolBinOp * expr list
| Expr_Unary of unOp * expr
| Expr_ZeroExtend of intVal * expr
| Expr_SignExtend of intVal * expr
| Expr_Extract of intVal * intVal * expr
| Expr_Concat of expr * expr

and lambdaDef =

| LambdaDef1 of localVar list * lambdaSep * expr

and binOp =

| BinOpBVBinOp of bVBinOp
| BinOpBVLogicalBinOp of bVLogicalBinOp
| BinOpBoolBinOp of boolBinOp
| BinOpIntLogicalBinOp of intLogicalBinOp
| BinOpIntBinOp of intBinOp
| BinOpEqOp of eqOp

and unOp =

| UnOpBVUnOp of bVUnOp
| UnOp_boolnot
| UnOp_intneg
| UnOp_booltobv1

and eqOp =

| EqOp_eq
| EqOp_neq

and bVUnOp =

| BVUnOp_bvnot
| BVUnOp_bvneg

and bVBinOp =

| BVBinOp_bvand
| BVBinOp_bvor
| BVBinOp_bvadd
| BVBinOp_bvmul
| BVBinOp_bvudiv
| BVBinOp_bvurem
| BVBinOp_bvshl
| BVBinOp_bvlshr
| BVBinOp_bvnand
| BVBinOp_bvnor
| BVBinOp_bvxor
| BVBinOp_bvxnor
| BVBinOp_bvcomp
| BVBinOp_bvsub
| BVBinOp_bvsdiv
| BVBinOp_bvsrem
| BVBinOp_bvsmod
| BVBinOp_bvashr

and bVLogicalBinOp =

| BVLogicalBinOp_bvule
| BVLogicalBinOp_bvugt
| BVLogicalBinOp_bvuge
| BVLogicalBinOp_bvult
| BVLogicalBinOp_bvslt
| BVLogicalBinOp_bvsle
| BVLogicalBinOp_bvsgt
| BVLogicalBinOp_bvsge

and intBinOp =

| IntBinOp_intadd
| IntBinOp_intmul
| IntBinOp_intsub
| IntBinOp_intdiv
| IntBinOp_intmod

and intLogicalBinOp =

| IntLogicalBinOp_intlt
| IntLogicalBinOp_intle
| IntLogicalBinOp_intgt
| IntLogicalBinOp_intge

and boolBinOp =

| BoolBinOp_booland
| BoolBinOp_boolor
| BoolBinOp_boolimplies

and requireTok =

| RequireTok_require
| RequireTok_requires

and ensureTok =

| EnsureTok_ensure
| EnsureTok_ensures

and funSpec =

| FunSpec_Require of requireTok * expr
| FunSpec_Ensure of ensureTok * expr
| FunSpec_Invariant of blockIdent * expr

and progSpec =

| ProgSpec_Rely of expr
| ProgSpec_Guarantee of expr