cprover
Loading...
Searching...
No Matches
string_instrumentation.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String Abstraction
4
5Author: 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
15class exprt;
16class goto_functionst;
17class goto_modelt;
18class goto_programt;
19class symbol_table_baset;
20
21void string_instrumentation(symbol_table_baset &, goto_programt &);
22
23void string_instrumentation(symbol_table_baset &, goto_functionst &);
24
25void string_instrumentation(goto_modelt &);
26
27exprt is_zero_string(const exprt &what, bool write = false);
28exprt zero_string_length(const exprt &what, bool write = false);
29exprt buffer_size(const exprt &what);
30
31#endif // CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
exprt
Base class for all expressions.
Definition expr.h:57
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:72
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:44
zero_string_length
exprt zero_string_length(const exprt &what, bool write=false)
Definition string_instrumentation.cpp:36
is_zero_string
exprt is_zero_string(const exprt &what, bool write=false)
Definition string_instrumentation.cpp:28
string_instrumentation
void string_instrumentation(symbol_table_baset &, goto_programt &)
Definition string_instrumentation.cpp:154