CBMC
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 class exprt;
16 class goto_functionst;
17 class goto_modelt;
18 class goto_programt;
19 class symbol_table_baset;
20 
21 void string_instrumentation(symbol_table_baset &, goto_programt &);
22 
23 void string_instrumentation(symbol_table_baset &, goto_functionst &);
24 
25 void string_instrumentation(goto_modelt &);
26 
27 exprt is_zero_string(const exprt &what, bool write = false);
28 exprt zero_string_length(const exprt &what, bool write=false);
29 exprt buffer_size(const exprt &what);
30 
31 #endif // CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
exprt
Base class for all expressions.
Definition: expr.h:56
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt
Definition: goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
buffer_size
exprt buffer_size(const exprt &what)
Definition: string_instrumentation.cpp:45
zero_string_length
exprt zero_string_length(const exprt &what, bool write=false)
Definition: string_instrumentation.cpp:35
is_zero_string
exprt is_zero_string(const exprt &what, bool write=false)
Definition: string_instrumentation.cpp:27
string_instrumentation
void string_instrumentation(symbol_table_baset &, goto_programt &)
Definition: string_instrumentation.cpp:155
write
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition: unistd.c:195