cprover
Loading...
Searching...
No Matches
string_format_builtin_function.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Built-in function for String.format
4
5Author: 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
18
63{
64public:
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:22
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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< array_string_exprt > string_result() const override
optionalt< std::string > format_string
Only set when the format string is a constant.
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:29
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,...