23 std::set<irep_idt> &dest)

24{

26

27

29 {

30 if(!identifier.empty())

31 dest.insert(identifier);

32 }

33}

40 const

41{

43 {

45 vm,

46 identifier.empty() || ns.lookup(identifier).is_parameter,

47 "parameter should be marked 'is_parameter' in the symbol table",

48 "affected parameter: ",

49 identifier);

50 }

51

52

54 {

56 vm,

58 "last instruction should be of end function type");

59 }

60

62}

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.

bool body_available() const

instructionst instructions

The list of instructions in the goto program.

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

Check that the goto program is well-formed.

void get_decl_identifiers(decl_identifierst &decl_identifiers) const

get the variables in decl statements

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().

void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)

Return in dest the identifiers of the local variables declared in the goto_function and the identifie...

#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)

#define DATA_CHECK(vm, condition, message)

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