CBMC
Loading...
Searching...
No Matches
flatten_ok_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Flatten OK Expressions
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
9#include "flatten_ok_expr.h"
10
11#include <util/c_types.h>
12
13#include "state.h"
14
16{
17 const auto &state = ok_expr.state();
18 const auto &pointer = ok_expr.address();
19 const auto &size = ok_expr.size();
20
21 // X_ok(p, s) <-->
22 // live_object(p)
23 // ∧ offset(p)+s≤object_size(p)
24 // ∧ writeable_object(p) if applicable
25
26 auto live_object = state_live_object_exprt(state, pointer);
27
28 auto writeable_object = state_writeable_object_exprt(state, pointer);
29
31 auto offset = pointer_offset_exprt(pointer, ssize_type);
32
33 auto size_type = ::size_type();
34
35 // extend one bit, to cover overflow case
36 auto size_type_ext = unsignedbv_typet(size_type.get_width() + 1);
37
38 auto object_size = state_object_size_exprt(state, pointer, size_type);
39
41
44 auto offset_extended =
47 auto upper = binary_relation_exprt(
49
50 auto conjunction = and_exprt(live_object, upper);
51
52 if(ok_expr.id() == ID_state_w_ok || ok_expr.id() == ID_state_rw_ok)
53 conjunction.add_to_operands(std::move(writeable_object));
54
55 return std::move(conjunction);
56}
signedbv_typet signed_size_type()
Definition c_types.cpp:66
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Base class for all expressions.
Definition expr.h:56
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The offset (in bytes) of a pointer relative to the object.
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
Fixed-width bit-vector with unsigned binary interpretation.
exprt flatten(const state_ok_exprt &ok_expr)
exprt object_size(const exprt &pointer)
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:83
#define size_type
Definition unistd.c:186