cprover
string_instrumentation.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String Abstraction
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
13 #define CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
14 
15 #include "goto_functions.h"
16 
17 class message_handlert;
18 
20  symbol_tablet &symbol_table,
21  message_handlert &message_handler,
22  goto_programt &dest);
23 
25  symbol_tablet &symbol_table,
26  message_handlert &message_handler,
27  goto_functionst &dest);
28 
29 exprt is_zero_string(const exprt &what, bool write=false);
30 exprt zero_string_length(const exprt &what, bool write=false);
31 exprt buffer_size(const exprt &what);
32 
33 #endif // CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
Goto Programs with Functions.
exprt zero_string_length(const exprt &what, bool write=false)
The symbol table.
Definition: symbol_table.h:52
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...
Definition: goto_program.h:24
exprt buffer_size(const exprt &what)
Base class for all expressions.
Definition: expr.h:46
exprt is_zero_string(const exprt &what, bool write=false)