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 goto_modelt;
20 
22 {
23 public:
25  std::string message,
27  : message(std::move(message)), source_location(std::move(source_location))
28  {
29  }
30  std::string what() const override
31  {
32  return message + " (at: " + source_location.as_string() + ")";
33  }
34 
35 private:
36  std::string message;
38 };
39 
41  symbol_tablet &,
42  goto_programt &);
43 
45  symbol_tablet &,
46  goto_functionst &);
47 
49 
50 predicate_exprt is_zero_string(const exprt &what, bool write = false);
51 exprt zero_string_length(const exprt &what, bool write=false);
52 exprt buffer_size(const exprt &what);
53 
54 #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.
Definition: goto_program.h:74
incorrect_source_program_exceptiont(std::string message, source_locationt source_location)
std::string what() const override
A human readable description of what went wrong.
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:485
std::string as_string() const
The symbol table.
Definition: symbol_table.h:20
Goto Programs with Functions.
void string_instrumentation(symbol_tablet &, goto_programt &)
exprt buffer_size(const exprt &what)
exprt zero_string_length(const exprt &what, bool write=false)
predicate_exprt is_zero_string(const exprt &what, bool write=false)