Built-in function for String.format. More...

#include <iterator>
#include <string>
#include "format_specifier.h"
#include "string_format_builtin_function.h"
#include "string_refinement_util.h"
#include <util/bitvector_expr.h>
#include <util/message.h>
#include <util/range.h>
#include <util/simplify_expr.h>

Include dependency graph for string_format_builtin_function.cpp:

Go to the source code of this file.

Functions
static exprt	format_arg_from_string (const array_string_exprt &string, const irep_idt &id, array_poolt &array_pool)
	Deserialize an argument for format from `string`. More...

static exprt	is_null (const array_string_exprt &string, array_poolt &array_pool)
	Expression which is true when the string is equal to the literal "null". More...

static std::pair< array_string_exprt, string_constraintst >	add_axioms_for_format_specifier (string_constraint_generatort &generator, const format_specifiert &fs, const array_string_exprt &string_arg, const typet &index_type, const typet &char_type, message_handlert &message_handler)
	Parse `s` and add axioms ensuring the output corresponds to the output of String.format. More...

static std::pair< exprt, string_constraintst >	add_axioms_for_format (string_constraint_generatort &generator, const array_string_exprt &res, const std::string &s, const std::vector< array_string_exprt > &args, message_handlert &message_handler)
	Parse `s` and add axioms ensuring the output corresponds to the output of String.format. More...

static std::vector< mp_integer >	deserialize_constant_int_arg (const std::vector< mp_integer > serialized, const unsigned base)

static bool	eval_is_null (const std::vector< mp_integer > &string)

static std::vector< mp_integer >	eval_format_specifier (const format_specifiert &fs, const std::vector< mp_integer > &arg)
	Return the string to replace the format specifier, as a vector of characters. More...

static exprt	length_of_positive_decimal_int (const exprt &pos_integer, int max_length, const typet &length_type, const unsigned long radix)
	Return an new expression representing the length of the representation of `integer`. More...

exprt	length_of_decimal_int (const exprt &integer, const typet &length_type, const unsigned long radix)
	Compute the length of the decimal representation of an integer. More...

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 constant. More...

Detailed Description

Built-in function for String.format.

Definition in file string_format_builtin_function.cpp.

Function Documentation

◆ add_axioms_for_format()

static std::pair<exprt, string_constraintst> add_axioms_for_format	(	string_constraint_generatort &	generator,
		const array_string_exprt &	res,
		const std::string &	s,
		const std::vector< array_string_exprt > &	args,
		message_handlert &	message_handler
	)

static

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Parameters

generator	constraint generator
res	string expression for the result of the format function
s	a format string
args	a vector of arguments
message_handler	message handler for warnings

Returns: code, 0 on success

Definition at line 297 of file string_format_builtin_function.cpp.

◆ add_axioms_for_format_specifier()

static std::pair<array_string_exprt, string_constraintst> add_axioms_for_format_specifier	(	string_constraint_generatort &	generator,
		const format_specifiert &	fs,
		const array_string_exprt &	string_arg,
		const typet &	index_type,
		const typet &	char_type,
		message_handlert &	message_handler
	)

static

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Assumes the argument is a string representing one of: string expr, int, float, char, boolean, hashcode, date_time. The correct type will be retrieved by calling get_arg with an id depending on the format specifier.

Parameters

generator	constraint generator
fs	a format specifier
string_arg	format string from argument
index_type	type for indexes in strings
char_type	type of characters
message_handler	message handler for warnings

Returns: String expression representing the output of String.format.

Definition at line 118 of file string_format_builtin_function.cpp.

◆ deserialize_constant_int_arg()

static std::vector<mp_integer> deserialize_constant_int_arg	(	const std::vector< mp_integer >	serialized,
		const unsigned	base
	)

static

Definition at line 399 of file string_format_builtin_function.cpp.

◆ eval_format_specifier()

static std::vector<mp_integer> eval_format_specifier	(	const format_specifiert &	fs,
		const std::vector< mp_integer > &	arg
	)

static

Return the string to replace the format specifier, as a vector of characters.

Definition at line 431 of file string_format_builtin_function.cpp.

◆ eval_is_null()

static bool eval_is_null ( const std::vector< mp_integer > & string )

static

Definition at line 423 of file string_format_builtin_function.cpp.

◆ format_arg_from_string()

static exprt format_arg_from_string	(	const array_string_exprt &	string,
		const irep_idt &	id,
		array_poolt &	array_pool
	)

static

Deserialize an argument for format from string.

id should be one of: string_expr, int, char, boolean, float. The primitive values are expected to all be encoded using 4 characters. The characters of string must be of type unsignedbv_typet(16).

Definition at line 243 of file string_format_builtin_function.cpp.

◆ is_null()

static exprt is_null	(	const array_string_exprt &	string,
		array_poolt &	array_pool
	)

static

Expression which is true when the string is equal to the literal "null".

Definition at line 94 of file string_format_builtin_function.cpp.

◆ length_for_format_specifier()

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 constant.

Definition at line 684 of file string_format_builtin_function.cpp.

◆ length_of_decimal_int()

exprt length_of_decimal_int	(	const exprt &	integer,
		const typet &	length_type,
		const unsigned long	radix
	)

Compute the length of the decimal representation of an integer.

Parameters

integer	(not necessarily constant) integer for which to compute the length of the decimal representation.
length_type	type to give to the created expression
radix	radix of the output representation.

Returns: : An exprt representing the length of integer

Definition at line 651 of file string_format_builtin_function.cpp.

◆ length_of_positive_decimal_int()

static exprt length_of_positive_decimal_int	(	const exprt &	pos_integer,
		int	max_length,
		const typet &	length_type,
		const unsigned long	radix
	)

static

Return an new expression representing the length of the representation of integer.

If max_length is less than the length of integer, the returned expression will represent max_length.

Parameters

pos_integer	positive (but not necessarily constant) integer for which to compute the length of the decimal representation.
max_length	max length of the decimal representation. If `max_length` is less than the length of `integer`, the returned expression will represent `max_length`. Choosing a value greater than the actual max possible length is harmless but will result in useless constraints.
length_type	type to give to the created expression
radix	radix of the output representation.

Returns: : An exprt representing the length of integer

Definition at line 623 of file string_format_builtin_function.cpp.

Functions

Detailed Description

Function Documentation

◆ add_axioms_for_format()

◆ add_axioms_for_format_specifier()

◆ deserialize_constant_int_arg()

◆ eval_format_specifier()

◆ eval_is_null()

◆ format_arg_from_string()

◆ is_null()

◆ length_for_format_specifier()

◆ length_of_decimal_int()

◆ length_of_positive_decimal_int()