CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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:
68 std::optional<std::string> format_string;
69 std::vector<array_string_exprt> inputs;
70
77 const exprt &return_code,
78 const std::vector<exprt> &fun_args,
80
81 std::optional<array_string_exprt> string_result() const override
82 {
83 return result;
84 }
85
86 std::vector<array_string_exprt> string_arguments() const override
87 {
88 return inputs;
89 }
90
91 std::optional<exprt>
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
101 message_handlert &message_handler) const override;
102
103 exprt length_constraint() const override;
104
118 bool maybe_testing_function() const override
119 {
120 return false;
121 }
122};
123
125 const exprt &integer,
126 const typet &length_type,
127 const unsigned long base);
128
130 const format_specifiert &fs,
131 const array_string_exprt &arg,
132 const typet &index_type,
133 array_poolt &array_pool);
134
135#endif // CPROVER_SOLVERS_STRINGS_STRING_FORMAT_BUILTIN_FUNCTION_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Correspondance between arrays and pointers string representations.
Definition array_pool.h:42
Base class for all expressions.
Definition expr.h:56
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().
std::optional< array_string_exprt > string_result() const override
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
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
std::optional< std::string > format_string
Only set when the format string is a constant.
bool maybe_testing_function() const override
In principle this function could return true, because the content of the string sometimes needs to be...
std::vector< array_string_exprt > inputs
std::optional< 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,...