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
16
17class exprt;
18class goto_functionst;
19class goto_modelt;
20class goto_programt;
21class symbol_tablet;
22
24{
25public:
32 std::string what() const override
33 {
34 return message + " (at: " + source_location.as_string() + ")";
35 }
36
37private:
38 std::string message;
40};
41
45
49
51
52exprt is_zero_string(const exprt &what, bool write = false);
53exprt zero_string_length(const exprt &what, bool write=false);
54exprt buffer_size(const exprt &what);
55
56#endif // CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
Base class for exceptions thrown in the cprover project.
Base class for all expressions.
Definition expr.h:54
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
incorrect_source_program_exceptiont(std::string message, source_locationt source_location)
std::string what() const override
A human readable description of what went wrong.
std::string as_string() const
The symbol table.
STL namespace.
void string_instrumentation(symbol_tablet &, goto_programt &)
exprt buffer_size(const exprt &what)
exprt zero_string_length(const exprt &what, bool write=false)
exprt is_zero_string(const exprt &what, bool write=false)