Module BasilIR.ParBasilIR

type token =
  1. | TOK_String of string
  2. | TOK_Str of string
  3. | TOK_ProcIdent of (int * int) * string
  4. | TOK_LocalIdent of (int * int) * string
  5. | TOK_LambdaSep of string
  6. | TOK_IntegerHex of (int * int) * string
  7. | TOK_IntegerDec of (int * int) * string
  8. | TOK_Integer of int
  9. | TOK_Ident of string
  10. | TOK_INTTYPE of (int * int) * string
  11. | TOK_GlobalIdent of (int * int) * string
  12. | TOK_EndRec of (int * int) * string
  13. | TOK_EndList of (int * int) * string
  14. | TOK_EOF
  15. | TOK_Double of float
  16. | TOK_Char of char
  17. | TOK_BlockIdent of (int * int) * string
  18. | TOK_BeginRec of (int * int) * string
  19. | TOK_BeginList of (int * int) * string
  20. | TOK_BVTYPE of (int * int) * string
  21. | TOK_BOOLTYPE of (int * int) * string
  22. | TOK_BIdent of (int * int) * string
  23. | SYMB9
  24. | SYMB8
  25. | SYMB7
  26. | SYMB6
  27. | SYMB5
  28. | SYMB4
  29. | SYMB3
  30. | SYMB2
  31. | SYMB10
  32. | SYMB1
  33. | KW_zero_extend
  34. | KW_var
  35. | KW_unreachable
  36. | KW_true
  37. | KW_store
  38. | KW_sign_extend
  39. | KW_shared
  40. | KW_return
  41. | KW_requires
  42. | KW_require
  43. | KW_rely
  44. | KW_prog
  45. | KW_proc
  46. | KW_old
  47. | KW_neq
  48. | KW_memory
  49. | KW_load
  50. | KW_le
  51. | KW_invariant
  52. | KW_intsub
  53. | KW_intneg
  54. | KW_intmul
  55. | KW_intmod
  56. | KW_intlt
  57. | KW_intle
  58. | KW_intgt
  59. | KW_intge
  60. | KW_intdiv
  61. | KW_intadd
  62. | KW_indirect
  63. | KW_guard
  64. | KW_guarantee
  65. | KW_goto
  66. | KW_forall
  67. | KW_false
  68. | KW_extract
  69. | KW_exists
  70. | KW_eq
  71. | KW_entry
  72. | KW_ensures
  73. | KW_ensure
  74. | KW_call
  75. | KW_bvxor
  76. | KW_bvxnor
  77. | KW_bvurem
  78. | KW_bvult
  79. | KW_bvule
  80. | KW_bvugt
  81. | KW_bvuge
  82. | KW_bvudiv
  83. | KW_bvsub
  84. | KW_bvsrem
  85. | KW_bvsmod
  86. | KW_bvslt
  87. | KW_bvsle
  88. | KW_bvshl
  89. | KW_bvsgt
  90. | KW_bvsge
  91. | KW_bvsdiv
  92. | KW_bvor
  93. | KW_bvnot
  94. | KW_bvnor
  95. | KW_bvneg
  96. | KW_bvnand
  97. | KW_bvmul
  98. | KW_bvlshr
  99. | KW_bvconcat
  100. | KW_bvcomp
  101. | KW_bvashr
  102. | KW_bvand
  103. | KW_bvadd
  104. | KW_booltobv1
  105. | KW_boolor
  106. | KW_boolnot
  107. | KW_boolimplies
  108. | KW_booland
  109. | KW_block
  110. | KW_be
  111. | KW_axiom
  112. | KW_assume
  113. | KW_assert
exception Error
val pValue : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.value
val pUnOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.unOp
val pTypeT_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.typeT list
val pTypeT : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.typeT
val pStmtWithAttrib_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.stmtWithAttrib list
val pStmtWithAttrib : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.stmtWithAttrib
val pStmt : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.stmt
val pSemicolons : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.semicolons
val pRequireTok : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.requireTok
val pProgSpec_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.progSpec list
val pProgSpec : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.progSpec
val pProcDef : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.procDef
val pParams_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.params list
val pParams : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.params
val pModuleT : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.moduleT
val pMapType : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.mapType
val pLocalVar_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.localVar list
val pLocalVar : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.localVar
val pLambdaDef : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.lambdaDef
val pLVars : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.lVars
val pLVar_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.lVar list
val pLVar : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.lVar
val pJumpWithAttrib : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.jumpWithAttrib
val pJump : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.jump
val pIntVal : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.intVal
val pIntType : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.intType
val pIntLogicalBinOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.intLogicalBinOp
val pIntBinOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.intBinOp
val pGlobalVar : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.globalVar
val pFunSpec_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.funSpec list
val pFunSpec : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.funSpec
val pExpr_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.expr list
val pExpr : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.expr
val pEqOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.eqOp
val pEnsureTok : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.ensureTok
val pEndian : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.endian
val pDecl_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.decl list
val pDecl : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.decl
val pBoolType : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.boolType
val pBoolBinOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.boolBinOp
val pBlock_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.block list
val pBlockIdent_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.blockIdent list
val pBlock : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.block
val pBinOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.binOp
val pBVVal : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.bVVal
val pBVUnOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.bVUnOp
val pBVType : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.bVType
val pBVLogicalBinOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.bVLogicalBinOp
val pBVBinOp : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.bVBinOp
val pAttribSet : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.attribSet
val pAttr_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.attr list
val pAttrKeyValue_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.attrKeyValue list
val pAttrKeyValue : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.attrKeyValue
val pAttr : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.attr
val pAssignment_list : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.assignment list
val pAssignment : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> AbsBasilIR.assignment