12 #ifndef CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H 13 #define CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H 33 #endif // CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H Goto Programs with Functions.
exprt zero_string_length(const exprt &what, bool write=false)
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
exprt buffer_size(const exprt &what)
Base class for all expressions.
exprt is_zero_string(const exprt &what, bool write=false)