cprover
string_format_builtin_function.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Built-in function for String.format
4 
5 Author: Romain Brenguier, Joel Allred
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_STRINGS_STRING_FORMAT_BUILTIN_FUNCTION_H
13 #define CPROVER_SOLVERS_STRINGS_STRING_FORMAT_BUILTIN_FUNCTION_H
14 
16 
17 class format_specifiert;
18 
63 {
64 public:
69  std::vector<array_string_exprt> inputs;
70 
77  const exprt &return_code,
78  const std::vector<exprt> &fun_args,
80 
82  {
83  return result;
84  }
85 
86  std::vector<array_string_exprt> string_arguments() const override
87  {
88  return inputs;
89  }
90 
92  eval(const std::function<exprt(const exprt &)> &get_value) const override;
93 
94  std::string name() const override
95  {
96  return "format";
97  }
98 
100  constraints(string_constraint_generatort &generator) const override;
101 
102  exprt length_constraint() const override;
103 
117  bool maybe_testing_function() const override
118  {
119  return false;
120  }
121 };
122 
124  const exprt &integer,
125  const typet &length_type,
126  const unsigned long base);
127 
129  const format_specifiert &fs,
130  const array_string_exprt &arg,
131  const typet &index_type,
132  array_poolt &array_pool);
133 
134 #endif // CPROVER_SOLVERS_STRINGS_STRING_FORMAT_BUILTIN_FUNCTION_H
bitvector_typet index_type()
Definition: c_types.cpp:16
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
Base class for all expressions.
Definition: expr.h:54
Field names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f9...
Base class for string functions that are built in the solver.
Built-in function for String.format().
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
std::vector< array_string_exprt > string_arguments() const override
bool maybe_testing_function() const override
In principle this function could return true, because the content of the string sometimes needs to be...
optionalt< std::string > format_string
Only set when the format string is a constant.
optionalt< array_string_exprt > string_result() const override
string_format_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
std::vector< array_string_exprt > inputs
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
The type of an expression, extends irept.
Definition: type.h:28
nonstd::optional< T > optionalt
Definition: optional.h:35
exprt length_of_decimal_int(const exprt &integer, const typet &length_type, const unsigned long base)
Compute the length of the decimal representation of an integer.
exprt length_for_format_specifier(const format_specifiert &fs, const array_string_exprt &arg, const typet &index_type, array_poolt &array_pool)
Return an expression representing the length of the format specifier Does not assume that arg is cons...
Collection of constraints of different types: existential formulas, universal formulas,...