19{

21

23 {

25 return to_code(op0()).first_statement();

27 return to_code(op0()).first_statement();

28 }

29

30 return *this;

31}

36{

38

40 {

42 return to_code(op0()).first_statement();

44 return to_code(op0()).first_statement();

45 }

46

47 return *this;

48}

53{

55

57 {

62 }

63

64 return *this;

65}

70{

72

74 {

79 }

80

81 return *this;

82}

87{

89

90 for(const auto &statement : extra_block.statements())

91 {

92 add(statement);

93 }

94}

97{

99

100 while(true)

101 {

103

106 {

108 }

110 {

112 }

113 else

114 break;

115 }

116

117 return *last;

118}

122{

124

125 for(auto &op : result.statements())

127

128 result.add_source_location() = loc;

129

130 return result;

131}

134{

136 std::vector<irep_idt> result;

137 result.reserve(sub.size());

138 for(const auto &s : sub)

140 return result;

141}

144 const std::vector<irep_idt> &parameter_identifiers)

145{

147 sub.reserve(parameter_identifiers.size());

148 for(const auto &id : parameter_identifiers)

149 {

152 }

153}

161{

167 location);

168

172 std::move(inc),

173 std::move(body)};

174}

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

A base class for relations, i.e., binary predicates whose two operands have the same type.

A non-fatal assertion, which checks a condition then permits execution to continue.

An assumption, which must hold in subsequent code.

A codet representing sequential composition of program statements.

code_operandst & statements()

void append(const code_blockt &extra_block)

Add all the codets from extra_block to the current code_blockt.

void add(const codet &code)

codet & find_last_statement()

codet representation of a for statement.

static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)

Produce a code_fort representing:

const codet & body() const

A codet representing an assignment in the program.

std::vector< irep_idt > get_parameter_identifiers() const

void set_parameter_identifiers(const std::vector< irep_idt > &)

Data structure for representing an arbitrary statement in a program.

codet & first_statement()

In the case of a codet type that represents multiple statements, return the first of them.

codet & last_statement()

In the case of a codet type that represents multiple statements, return the last of them.

const irep_idt & get_statement() const

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Base class for all expressions.

bool has_operands() const

Return true if there is at least one operand.

source_locationt & add_source_location()

const irept & find(const irep_idt &name) const

irept & add(const irep_idt &name)

The plus expression Associativity is not specified.

A side_effect_exprt that performs an assignment.

Expression to hold a symbol (variable)

#define PRECONDITION(CONDITION)

code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &loc)

Create a fatal assertion, which checks a condition and then halts if it does not hold.

const code_labelt & to_code_label(const codet &code)

const code_blockt & to_code_block(const codet &code)

const codet & to_code(const exprt &expr)