Unit tests for length_of_decimal_int
This commit is contained in:
parent
f61877a01a
commit
710b1c831f
|
@ -49,6 +49,7 @@ SRC += analyses/ai/ai.cpp \
|
||||||
solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
|
solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
|
||||||
solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp \
|
solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp \
|
||||||
solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp \
|
solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp \
|
||||||
|
solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp \
|
||||||
solvers/strings/string_refinement/concretize_array.cpp \
|
solvers/strings/string_refinement/concretize_array.cpp \
|
||||||
solvers/strings/string_refinement/sparse_array.cpp \
|
solvers/strings/string_refinement/sparse_array.cpp \
|
||||||
solvers/strings/string_refinement/substitute_array_list.cpp \
|
solvers/strings/string_refinement/substitute_array_list.cpp \
|
||||||
|
|
|
@ -0,0 +1,68 @@
|
||||||
|
/*******************************************************************\
|
||||||
|
|
||||||
|
Module: Unit tests for length_of_decimal_int in
|
||||||
|
solvers/refinement/string_format_builtin_function.cpp
|
||||||
|
|
||||||
|
Author: Diffblue Ltd.
|
||||||
|
|
||||||
|
\*******************************************************************/
|
||||||
|
|
||||||
|
#include <testing-utils/use_catch.h>
|
||||||
|
|
||||||
|
#include <solvers/strings/string_format_builtin_function.h>
|
||||||
|
#include <util/simplify_expr.h>
|
||||||
|
#include <util/symbol_table.h>
|
||||||
|
|
||||||
|
SCENARIO(
|
||||||
|
"length_of_decimal_int",
|
||||||
|
"[core][solvers][strings][string_format_builtin_function]")
|
||||||
|
{
|
||||||
|
const typet type = signedbv_typet(32);
|
||||||
|
|
||||||
|
const symbol_tablet symbol_table;
|
||||||
|
const namespacet ns{symbol_table};
|
||||||
|
|
||||||
|
const std::vector<mp_integer> input_values = {
|
||||||
|
0, 1, 10, 15, 999, 1000000001, -1, -21111111, -1234567890};
|
||||||
|
const std::vector<int> oracles_for_base_10 = {1, 1, 2, 2, 3, 10, 2, 9, 11};
|
||||||
|
const std::vector<int> oracles_for_base_16 = {1, 1, 1, 1, 3, 8, 2, 8, 9};
|
||||||
|
|
||||||
|
WHEN("base = 10")
|
||||||
|
{
|
||||||
|
for(size_t i = 0; i < input_values.size(); i++)
|
||||||
|
{
|
||||||
|
exprt input_expr = from_integer(input_values[i], type);
|
||||||
|
WHEN("input exprt = " << input_values[i])
|
||||||
|
{
|
||||||
|
const exprt actual = length_of_decimal_int(input_expr, type, 10);
|
||||||
|
const int oracle = oracles_for_base_10[i];
|
||||||
|
THEN("length expression is " << oracle)
|
||||||
|
{
|
||||||
|
const int actual_int =
|
||||||
|
numeric_cast<int>(to_constant_expr(simplify_expr(actual, ns)))
|
||||||
|
.value();
|
||||||
|
REQUIRE(actual_int == oracle);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
WHEN("base = 16")
|
||||||
|
{
|
||||||
|
for(size_t i = 0; i < input_values.size(); i++)
|
||||||
|
{
|
||||||
|
exprt input_expr = from_integer(input_values[i], type);
|
||||||
|
WHEN("input exprt = " << input_values[i])
|
||||||
|
{
|
||||||
|
const exprt actual = length_of_decimal_int(input_expr, type, 16);
|
||||||
|
const int oracle = oracles_for_base_16[i];
|
||||||
|
THEN("length expression is " << oracle)
|
||||||
|
{
|
||||||
|
const int actual_int =
|
||||||
|
*numeric_cast<int>(to_constant_expr(simplify_expr(actual, ns)));
|
||||||
|
REQUIRE(actual_int == oracle);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
Loading…
Reference in New Issue