string_constraint_generator_valueof.cpp File Reference

Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool. More...

#include "string_constraint_generator.h"
#include <util/deprecate.h>
#include <util/mathematical_expr.h>
#include <util/simplify_expr.h>
#include <cmath>

Include dependency graph for string_constraint_generator_valueof.cpp:

Go to the source code of this file.

Functions
static unsigned long	to_integer_or_default (const exprt &expr, unsigned long def, const namespacet &ns)
	If the expression is a constant expression then we get the value of it as an unsigned long. More...
static exprt	int_of_hex_char (const exprt &chr)
	Returns the integer value represented by the character. More...
exprt	is_digit_with_radix (const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
	Check if a character is a digit with respect to the given radix, e.g. More...
exprt	get_numeric_value_from_character (const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, const unsigned long radix_ul)
	Get the numeric value of a character, assuming that the radix is large enough. More...
size_t	max_printed_string_length (const typet &type, unsigned long radix_ul)
	Calculate the string length needed to represent any value of the given type using the given radix. More...

Detailed Description

Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool.

Definition in file string_constraint_generator_valueof.cpp.

Function Documentation

get_numeric_value_from_character()

exprt get_numeric_value_from_character	(	const exprt &	chr,
		const typet &	char_type,
		const typet &	type,
		const bool	strict_formatting,
		const unsigned long	radix_ul
	)

Get the numeric value of a character, assuming that the radix is large enough.

'+' and '-' yield 0.

Parameters

chr	the character to get the numeric value of
char_type	the type to use for characters
type	the type to use for the return value
strict_formatting	if true, don't allow upper case characters
radix_ul	the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix

Returns

an integer expression of the given type with the numeric value of the char

There are four cases, which occur in ASCII in the following order: '+' and '-', digits, upper case letters, lower case letters

return char >= '0' ? (char - '0') : 0

return char >= 'a' ? (char - 'a' + 10) : char >= '0' ? (char - '0') : 0

return char >= 'a' ? (char - 'a' + 10) : char >= 'A' ? (char - 'A' + 10) : char >= '0' ? (char - '0') : 0

Definition at line 623 of file string_constraint_generator_valueof.cpp.

int_of_hex_char()

static exprt int_of_hex_char ( const exprt &  chr )

static

Returns the integer value represented by the character.

Parameters

chr	a character expression in the following set: 0123456789abcdef

Returns

an integer expression

Definition at line 181 of file string_constraint_generator_valueof.cpp.

is_digit_with_radix()

exprt is_digit_with_radix	(	const exprt &	chr,
		const bool	strict_formatting,
		const exprt &	radix_as_char,
		const unsigned long	radix_ul
	)

Check if a character is a digit with respect to the given radix, e.g.

if the radix is 10 then check if the character is in the range 0-9.

Parameters

chr	the character
strict_formatting	if true, don't allow upper case characters
radix_as_char	the radix as an expression of the same type as chr
radix_ul	the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix

Returns

an expression for the condition

Definition at line 555 of file string_constraint_generator_valueof.cpp.

max_printed_string_length()

size_t max_printed_string_length	(	const typet &	type,
		unsigned long	radix_ul
	)

Calculate the string length needed to represent any value of the given type using the given radix.

Due to floating point rounding errors we sometimes return a value 1 larger than needed, which is fine for our purposes.

Parameters

type	the type that we are considering values of
radix_ul	the radix we are using, or 0, in which case the return value will work for any radix

Returns

the maximum string length

We want to calculate max, the maximum number of characters needed to represent any value of the given type.

For signed types, the longest string will be for -2^(n_bits-1), so max = 1 + min{k: 2^(n_bits-1) < radix^k} (the 1 is for the minus sign) = 1 + min{k: n_bits-1 < k log_2(radix)} = 1 + min{k: k > (n_bits-1) / log_2(radix)} = 1 + min{k: k > floor((n_bits-1) / log_2(radix))} = 1 + (1 + floor((n_bits-1) / log_2(radix))) = 2 + floor((n_bits-1) / log_2(radix))

For unsigned types, the longest string will be for (2^n_bits)-1, so max = min{k: (2^n_bits)-1 < radix^k} = min{k: 2^n_bits <= radix^k} = min{k: n_bits <= k log_2(radix)} = min{k: k >= n_bits / log_2(radix)} = min{k: k >= ceil(n_bits / log_2(radix))} = ceil(n_bits / log_2(radix))

Definition at line 697 of file string_constraint_generator_valueof.cpp.

to_integer_or_default()

static unsigned long to_integer_or_default ( const exprt &  expr, unsigned long  def, const namespacet &  ns  )

static

If the expression is a constant expression then we get the value of it as an unsigned long.

If not we return a default value.

Parameters

expr	input expression
def	default value to return if we cannot evaluate expr
ns	namespace used to simplify the expression

Returns

the output as an unsigned long

Definition at line 28 of file string_constraint_generator_valueof.cpp.