12 #ifndef CPROVER_ANALYSES_GOTO_CHECK_H
13 #define CPROVER_ANALYSES_GOTO_CHECK_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
::goto_functiont goto_functiont
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void goto_check(const namespacet &, const optionst &, goto_functionst &, message_handlert &)
Goto Programs with Functions.