blob: 964f666755e0d98687f91ba5461db48e33a21016 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
namespace BoogieAst
type BType = BInt | BBool
type BOperator = BEq | BNeq | BPlus | BMinus | BTimes | BLess | BAtMost | BAnd | BOr
type BExpression =
| BConstant of int
| BFalse
| BTrue
| BNull
| BIdentifier of string
| BNot of BExpression
| BBinary of BOperator * BExpression * BExpression
| BSelect of string * BExpression
| BToPred of BExpression // BToPred(e) == (e != 0)
| BToTerm of BExpression // BToTerm(e) == (if e then 1 else 0)
| BOld of BExpression
| BFunc of string * BExpression list
type BStmtList =
BBlock of Statement list
and Statement =
| BAssign of string * BExpression
| BUpdate of string * BExpression * BExpression
| BHavoc of string list
| BAssert of BExpression
| BAssume of BExpression
| BIfStmt of BExpression * BStmtList * BStmtList
| BWhileStmt of BExpression * BExpression list * BStmtList
| BCallStmt of string list * string * BExpression list
type BVarDecl = BVar of string * BType
type BProcedure =
BProc of string * BVarDecl list * BVarDecl list * BExpression * string list * BExpression * BVarDecl list * BStmtList
type BProgram =
BProg of string * BProcedure list
|
