vcg 0.1.0

Utilities for manipulating verification conditions.
Documentation 
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

#[derive(Clone,Debug,PartialEq)]
pub enum Bytecode {
    // Declarations
    Assert,
    Fun(usize),
    RecFun(usize),
    // Logical
    Not,
    And,
    Or,
    Implies,
    HasType,
    // Comparators
    Eq,
    Neq,
    Lt,
    LtEq,
    Gt,
    GtEq,
    // Arithmetic
    Add,
    Sub,
    Mul,
    Div,
    Rem,
    // Other
    If,
    Invoke(usize,usize),
    // Literals
    Int(usize),
    Bool(bool),
    Var(usize),
    // Type Tests
    IsUint,
    IsBool
}