CBMC
Loading...
Searching...
No Matches
sentinel_dll.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Sentinel Doubly Linked Lists
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "sentinel_dll.h"
13
14#include <util/c_types.h>
15#include <util/namespace.h>
16#include <util/pointer_expr.h>
17
18#include "state.h"
19
20std::optional<exprt> sentinel_dll_member(
21 const exprt &state,
22 const exprt &node,
23 bool next, // vs. prev
24 const namespacet &ns)
25{
26 if(node.type().id() != ID_pointer)
27 return {};
28
29 if(to_pointer_type(node.type()).base_type().id() != ID_struct_tag)
30 return {};
31
32 const auto &struct_type =
33 ns.follow_tag(to_struct_tag_type(to_pointer_type(node.type()).base_type()));
34
35 // the first pointer to a struct is 'next', the second 'prev'
36 const struct_typet::componentt *next_m = nullptr, *prev_m = nullptr;
37
38 for(auto &m : struct_type.components())
39 {
40 if(m.type() == node.type()) // we are strict on the type
41 {
42 if(next_m == nullptr)
43 next_m = &m;
44 else
45 prev_m = &m;
46 }
47 }
48
50
51 if(next)
52 {
53 if(next_m == nullptr)
54 return {};
55 else
57 }
58 else
59 {
60 if(prev_m == nullptr)
61 return {};
62 else
64 }
65
67 node, component.get_name(), pointer_type(component.type()));
68
69 return evaluate_exprt(state, field_address, component.type());
70}
71
72std::optional<exprt>
73sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &ns)
74{
75 return sentinel_dll_member(state, node, true, ns);
76}
77
78std::optional<exprt>
79sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
80{
81 return sentinel_dll_member(state, node, false, ns);
82}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
Operator to return the address of a field relative to a base address.
const irep_idt & id() const
Definition irep.h:388
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< exprt > sentinel_dll_member(const exprt &state, const exprt &node, bool next, const namespacet &ns)
std::optional< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
std::optional< exprt > sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &ns)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:122
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518