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 #include <util/exception_utils.h>
18 
19 class message_handlert;
20 class goto_modelt;
21 
23 {
24 public:
26  std::string message,
28  : message(std::move(message)), source_location(std::move(source_location))
29  {
30  }
31  std::string what() const override
32  {
33  return message + " (at: " + source_location.as_string() + ")";
34  }
35 
36 private:
37  std::string message;
39 };
40 
42  symbol_tablet &,
44  goto_programt &);
45 
47  symbol_tablet &,
49  goto_functionst &);
50 
52  goto_modelt &,
54 
55 predicate_exprt is_zero_string(const exprt &what, bool write = false);
56 exprt zero_string_length(const exprt &what, bool write=false);
57 exprt buffer_size(const exprt &what);
58 
59 #endif // CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
exception_utils.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:26
string_instrumentation
void string_instrumentation(symbol_tablet &, message_handlert &, goto_programt &)
Definition: string_instrumentation.cpp:157
is_zero_string
predicate_exprt is_zero_string(const exprt &what, bool write=false)
Definition: string_instrumentation.cpp:30
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
incorrect_source_program_exceptiont::incorrect_source_program_exceptiont
incorrect_source_program_exceptiont(std::string message, source_locationt source_location)
Definition: string_instrumentation.h:25
incorrect_source_program_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: string_instrumentation.h:31
predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:535
buffer_size
exprt buffer_size(const exprt &what)
Definition: string_instrumentation.cpp:48
message_handlert
Definition: message.h:28
source_locationt
Definition: source_location.h:20
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
zero_string_length
exprt zero_string_length(const exprt &what, bool write=false)
Definition: string_instrumentation.cpp:38
incorrect_source_program_exceptiont
Definition: string_instrumentation.h:23
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
incorrect_source_program_exceptiont::source_location
source_locationt source_location
Definition: string_instrumentation.h:38
incorrect_source_program_exceptiont::message
std::string message
Definition: string_instrumentation.h:37
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition: exception_utils.h:25