CBMC
flatten_ok_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Flatten OK Expressions
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_CPROVER_FLATTEN_OK_EXPR_H
10 #define CPROVER_CPROVER_FLATTEN_OK_EXPR_H
11 
12 class exprt;
13 class state_ok_exprt;
14 
15 // X_ok(p, s) <-->
16 // live_object(p)
17 // ∧ offset(p)+s≤object_size(p)
18 // ∧ writeable_object(p) if applicable
19 
20 exprt flatten(const state_ok_exprt &);
21 
22 #endif // CPROVER_CPROVER_FLATTEN_OK_EXPR_H
exprt
Base class for all expressions.
Definition: expr.h:56
state_ok_exprt
Definition: state.h:823
flatten
exprt flatten(const state_ok_exprt &)
Definition: flatten_ok_expr.cpp:15