41{

43 {

44 func.second.body.compute_incoming_edges();

45 }

46}

49{

51 {

52 func.second.body.compute_target_numbers();

53 }

54}

57{

59 {

60 func.second.body.compute_loop_numbers();

61 }

62}

67{

68 std::vector<function_mapt::const_iterator> result;

69

71

73 result.push_back(it);

74

75 std::sort(

76 result.begin(),

77 result.end(),

78 [](function_mapt::const_iterator a, function_mapt::const_iterator b) {

79 return id2string(a->first) < id2string(b->first);

80 });

81

82 return result;

83}

87{

88 std::vector<function_mapt::iterator> result;

89

91

93 result.push_back(it);

94

95 std::sort(

96 result.begin(),

97 result.end(),

98 [](function_mapt::iterator a, function_mapt::iterator b) {

99 return id2string(a->first) < id2string(b->first);

100 });

101

102 return result;

103}

106 const

107{

109 {

111 const auto &function_name = entry.first;

115

117 vm,

119 id2string(function_name) + " parameter count inconsistency\n" +

120 "goto program: " +

122 "\nsymbol table: " + std::to_string(parameters.size()));

123

125 for(const auto &parameter : parameters)

126 {

128 vm,

130 id2string(function_name) + " parameter type inconsistency\n" +

131 "goto program: " + ns.lookup(*it).type.id_string() +

132 "\nsymbol table: " + parameter.type().id_string());

133 ++it;

134 }

135

136 goto_function.validate(ns, vm);

137

138

140 {

141 for(const auto &instruction : goto_function.body.instructions)

142 {

144 vm,

145 !instruction.is_set_return_value(),

146 "void function should not return a value");

147 }

148 }

149 }

150}

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

std::vector< parametert > parameterst

void compute_incoming_edges()

void compute_loop_numbers()

unsigned unused_location_number

A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...

function_mapt function_map

void compute_location_numbers()

void validate(const namespacet &, validation_modet) const

Check that the goto functions are well-formed.

std::vector< function_mapt::const_iterator > sorted() const

returns a vector of the iterators in alphabetical order

void compute_target_numbers()

A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...

parameter_identifierst parameter_identifiers

The identifiers of the parameters of this function.

void validate(const namespacet &ns, const validation_modet vm) const

Check that the goto function is well-formed.

A generic container class for the GOTO intermediate representation of one function.

instructionst instructions

The list of instructions in the goto program.

void compute_location_numbers(unsigned &nr)

Compute location numbers.

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

bool lookup(const irep_idt &name, const symbolt *&symbol) const override

See documentation for namespace_baset::lookup().

Goto Programs with Functions.

const std::string & id2string(const irep_idt &d)

const code_typet & to_code_type(const typet &type)

Cast a typet to a code_typet.

#define DATA_CHECK(vm, condition, message)

This macro takes a condition which denotes a well-formedness criterion on goto programs,...