cprover
|
Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool. More...
Go to the source code of this file.
Functions | |
exprt | get_exponent (const exprt &src, const ieee_float_spect &spec) |
Gets the unbiased exponent in a floating-point bit-vector. More... | |
exprt | get_fraction (const exprt &src, const ieee_float_spect &spec) |
Gets the fraction without hidden bit. More... | |
exprt | get_significand (const exprt &src, const ieee_float_spect &spec, const typet &type) |
Gets the significand as a java integer, looking for the hidden bit. More... | |
exprt | constant_float (const double f, const ieee_float_spect &float_spec) |
Create an expression to represent a float or double value. More... | |
exprt | round_expr_to_zero (const exprt &f) |
Round a float expression to an integer closer to 0. More... | |
exprt | floatbv_mult (const exprt &f, const exprt &g) |
Multiplication of expressions representing floating points. More... | |
exprt | floatbv_of_int_expr (const exprt &i, const ieee_float_spect &spec) |
Convert integers to floating point to be used in operations with other values that are in floating point representation. More... | |
exprt | estimate_decimal_exponent (const exprt &f, const ieee_float_spect &spec) |
Estimate the decimal exponent that should be used to represent a given floating point value in decimal. More... | |
Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool.
Definition in file string_constraint_generator_float.cpp.
exprt constant_float | ( | const double | f, |
const ieee_float_spect & | float_spec | ||
) |
Create an expression to represent a float or double value.
f | a floating point value in double precision |
float_spec | a specification for floats |
Definition at line 76 of file string_constraint_generator_float.cpp.
References ieee_float_spect::double_precision(), ieee_floatt::from_double(), ieee_floatt::from_float(), ieee_float_spect::single_precision(), ieee_floatt::to_expr(), and UNREACHABLE.
Referenced by string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_from_float_scientific_notation(), and estimate_decimal_exponent().
exprt estimate_decimal_exponent | ( | const exprt & | f, |
const ieee_float_spect & | spec | ||
) |
Estimate the decimal exponent that should be used to represent a given floating point value in decimal.
We are looking for \(d\) such that \(n * 10^d = m * 2^e\), so: \(d = log_10(m) + log_10(2) * e - log_10(n)\) m – the fraction – should be between 1 and 2 so log_10(m) in [0,log_10(2)]. n – the fraction in base 10 – should be between 1 and 10 so log_10(n) in [0, 1]. So the estimate is given by: d ~=~ floor(log_10(2) * e)
f | a floating point expression |
spec | specification for floating point |
Definition at line 137 of file string_constraint_generator_float.cpp.
References constant_float(), floatbv_mult(), floatbv_of_int_expr(), get_exponent(), and round_expr_to_zero().
Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation().
Multiplication of expressions representing floating points.
Note that the rounding mode is set to ROUND_TO_EVEN.
f | a floating point expression |
g | a floating point expression |
Definition at line 102 of file string_constraint_generator_float.cpp.
References exprt::copy_to_operands(), from_integer(), PRECONDITION, ieee_floatt::ROUND_TO_EVEN, and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_from_float_scientific_notation(), and estimate_decimal_exponent().
exprt floatbv_of_int_expr | ( | const exprt & | i, |
const ieee_float_spect & | spec | ||
) |
Convert integers to floating point to be used in operations with other values that are in floating point representation.
i | an expression representing an integer |
spec | specification for floating point numbers |
Definition at line 119 of file string_constraint_generator_float.cpp.
References from_integer(), ieee_floatt::ROUND_TO_ZERO, and ieee_float_spect::to_type().
Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation(), and estimate_decimal_exponent().
exprt get_exponent | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Gets the unbiased exponent in a floating-point bit-vector.
src | a floating point expression |
spec | specification for floating points |
Definition at line 27 of file string_constraint_generator_float.cpp.
References ieee_float_spect::bias(), ieee_float_spect::e, ieee_float_spect::f, and from_integer().
Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation(), estimate_decimal_exponent(), and get_significand().
exprt get_fraction | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Gets the fraction without hidden bit.
src | a floating point expression |
spec | specification for floating points |
Definition at line 44 of file string_constraint_generator_float.cpp.
References ieee_float_spect::f.
Referenced by get_significand().
exprt get_significand | ( | const exprt & | src, |
const ieee_float_spect & | spec, | ||
const typet & | type | ||
) |
Gets the significand as a java integer, looking for the hidden bit.
Since the most significant bit is 1 for normalized number, it is not part of the encoding of the significand and is 0 only if all the bits of the exponent are 0, that is why it is called the hidden bit.
src | a floating point expression |
spec | specification for floating points |
type | type of the output, should be unsigned with width greater than the width of the significand in the given spec |
Definition at line 59 of file string_constraint_generator_float.cpp.
References ieee_float_spect::f, from_integer(), get_exponent(), get_fraction(), irept::id(), PRECONDITION, to_unsignedbv_type(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation().
Round a float expression to an integer closer to 0.
f | expression representing a float |
Definition at line 91 of file string_constraint_generator_float.cpp.
References from_integer(), and ieee_floatt::ROUND_TO_ZERO.
Referenced by string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_from_float_scientific_notation(), and estimate_decimal_exponent().