Module Cgil_lib.Annot_parser

type token =
  1. | ZEROS
  2. | VERIFY
  3. | UNFOLD_ALL
  4. | UNFOLD
  5. | UNDEFS
  6. | TRUE
  7. | SYMB_EXEC
  8. | STRUCT
  9. | STRING of string
  10. | STAR
  11. | SPECIFICATION
  12. | SINGLET
  13. | SETUNION
  14. | SETSUB
  15. | SETOP
  16. | SETMEM
  17. | SETDIFF
  18. | SETCL
  19. | SCOLON
  20. | REQUIRES
  21. | REC_UNFOLD
  22. | RDBRACK
  23. | RCBRACE
  24. | RBRACK
  25. | RBRACE
  26. | PURE
  27. | PTRT
  28. | PTRPLUS
  29. | PROOF
  30. | PREDICATE
  31. | POINTSTO
  32. | PLUS
  33. | OR
  34. | NULL
  35. | NOUNFOLD
  36. | NIL
  37. | MINUS
  38. | MALLOCPOINTSTO
  39. | MALLOCED_ARRAY
  40. | MALLOCED
  41. | LVAR of string
  42. | LT
  43. | LSUB
  44. | LSTCONS
  45. | LSTCAT
  46. | LSETMEM
  47. | LOR
  48. | LONGT
  49. | LOC of string
  50. | LNOT
  51. | LLT
  52. | LLEQ
  53. | LEQ
  54. | LEN
  55. | LEMMA
  56. | LDBRACK
  57. | LCBRACE
  58. | LBRACK
  59. | LBRACE
  60. | LAND
  61. | INVARIANT
  62. | INTT
  63. | INTEGER of Z.t
  64. | INT16T
  65. | IMPORT
  66. | IMPLIES
  67. | IF
  68. | IDENTIFIER of string
  69. | HYPOTHESIS
  70. | GSETT
  71. | GLOBALPOINTSTO
  72. | GLISTT
  73. | GINTT
  74. | FUNPTRT
  75. | FOR_LOOP
  76. | FORALL
  77. | FOLD
  78. | FLOATT
  79. | FALSE
  80. | EQ
  81. | EOF
  82. | ENSURES
  83. | ENOT
  84. | EMP
  85. | ELSE
  86. | DOT
  87. | DIV
  88. | CTRUE
  89. | CONCLUSIONS
  90. | COMMA
  91. | COLON
  92. | CHART
  93. | CFALSE
  94. | BRANCH
  95. | BIND
  96. | BIGOR
  97. | AXIOMATIC
  98. | ASSERT
  99. | ARRAY
  100. | APPLY
  101. | ANNOT_OPEN
  102. | ANNOT_CLOSE
  103. | AND
  104. | ABSTRACT
exception Error
val prog : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> CLogic.CProg.t
val logic_command_entry : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> CLogic.CLCmd.t