Skip to content

Commit 4cfbfb5

Browse files
author
Owen Jones
committed
Updated two unit tests
1 parent 7aaf761 commit 4cfbfb5

File tree

2 files changed

+103
-52
lines changed

2 files changed

+103
-52
lines changed

‎unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp

Lines changed: 89 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -15,27 +15,97 @@
1515
#include <util/simplify_expr.h>
1616
#include <util/std_types.h>
1717

18+
19+
1820
SCENARIO("get_numeric_value_from_character",
1921
"[core][solvers][refinement][string_constraint_generator_valueof]")
2022
{
21-
typet char_type=unsignedbv_typet(16);
22-
typet int_type=signedbv_typet(32);
23+
const typet char_type_1=unsignedbv_typet(8);
24+
const typet char_type_2=unsignedbv_typet(16);
25+
const typet char_type_3=unsignedbv_typet(32);
26+
const typet int_type_1=signedbv_typet(8);
27+
const typet int_type_2=signedbv_typet(16);
28+
const typet int_type_3=signedbv_typet(32);
29+
const typet int_type_4=signedbv_typet(64);
2330
symbol_tablet symtab;
24-
namespacet ns(symtab);
25-
26-
REQUIRE(from_integer(0, int_type)==simplify_expr(
27-
get_numeric_value_from_character(
28-
from_integer('0', char_type), char_type, int_type), ns));
29-
REQUIRE(from_integer(9, int_type)==simplify_expr(
30-
get_numeric_value_from_character(
31-
from_integer('9', char_type),
32-
char_type, int_type), ns));
33-
REQUIRE(from_integer(10, int_type)==simplify_expr(
34-
get_numeric_value_from_character(
35-
from_integer('A', char_type),
36-
char_type, int_type), ns));
37-
REQUIRE(from_integer(35, int_type)==simplify_expr(
38-
get_numeric_value_from_character(
39-
from_integer('z', char_type),
40-
char_type, int_type), ns));
31+
const namespacet ns(symtab);
32+
33+
WHEN("0")
34+
{
35+
mp_integer character='0';
36+
mp_integer expected_value=0;
37+
const typet& char_type=char_type_1;
38+
const typet& int_type=int_type_1;
39+
constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
40+
exprt actual_value_exprt=simplify_expr(
41+
get_numeric_value_from_character(
42+
from_integer(character, char_type), char_type, int_type),
43+
ns);
44+
REQUIRE(expected_value_exprt==actual_value_exprt);
45+
}
46+
WHEN("9")
47+
{
48+
mp_integer character='9';
49+
mp_integer expected_value=9;
50+
const typet& char_type=char_type_2;
51+
const typet& int_type=int_type_2;
52+
constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
53+
exprt actual_value_exprt=simplify_expr(
54+
get_numeric_value_from_character(
55+
from_integer(character, char_type), char_type, int_type),
56+
ns);
57+
REQUIRE(expected_value_exprt==actual_value_exprt);
58+
}
59+
WHEN("A")
60+
{
61+
mp_integer character='A';
62+
mp_integer expected_value=10;
63+
const typet& char_type=char_type_3;
64+
const typet& int_type=int_type_3;
65+
constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
66+
exprt actual_value_exprt=simplify_expr(
67+
get_numeric_value_from_character(
68+
from_integer(character, char_type), char_type, int_type),
69+
ns);
70+
REQUIRE(expected_value_exprt==actual_value_exprt);
71+
}
72+
WHEN("z")
73+
{
74+
mp_integer character='z';
75+
mp_integer expected_value=35;
76+
const typet& char_type=char_type_1;
77+
const typet& int_type=int_type_4;
78+
constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
79+
exprt actual_value_exprt=simplify_expr(
80+
get_numeric_value_from_character(
81+
from_integer(character, char_type), char_type, int_type),
82+
ns);
83+
REQUIRE(expected_value_exprt==actual_value_exprt);
84+
}
85+
WHEN("+")
86+
{
87+
mp_integer character='+';
88+
mp_integer expected_value=0;
89+
const typet& char_type=char_type_2;
90+
const typet& int_type=int_type_1;
91+
constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
92+
exprt actual_value_exprt=simplify_expr(
93+
get_numeric_value_from_character(
94+
from_integer(character, char_type), char_type, int_type),
95+
ns);
96+
REQUIRE(expected_value_exprt==actual_value_exprt);
97+
}
98+
WHEN("-")
99+
{
100+
mp_integer character='-';
101+
mp_integer expected_value=0;
102+
const typet& char_type=char_type_3;
103+
const typet& int_type=int_type_2;
104+
constant_exprt expected_value_exprt=from_integer(expected_value, int_type);
105+
exprt actual_value_exprt=simplify_expr(
106+
get_numeric_value_from_character(
107+
from_integer(character, char_type), char_type, int_type),
108+
ns);
109+
REQUIRE(expected_value_exprt==actual_value_exprt);
110+
}
41111
}

‎unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp

Lines changed: 14 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -18,57 +18,38 @@
1818
SCENARIO("is_digit_with_radix",
1919
"[core][solvers][refinement][string_constraint_generator_valueof]")
2020
{
21-
typet char_type=unsignedbv_typet(16);
22-
typet int_type=signedbv_typet(32);
21+
const typet char_type=unsignedbv_typet(16);
2322
symbol_tablet symtab;
24-
namespacet ns(symtab);
23+
const namespacet ns(symtab);
2524

2625
WHEN("Radix 10")
2726
{
28-
int radix=10;
27+
const constant_exprt radix_expr=from_integer(10, char_type);
2928
REQUIRE(true_exprt()==simplify_expr(
30-
is_digit_with_radix(
31-
from_integer('0', char_type),
32-
from_integer(radix, int_type)), ns));
29+
is_digit_with_radix(from_integer('0', char_type), radix_expr), ns));
3330
REQUIRE(true_exprt()==simplify_expr(
34-
is_digit_with_radix(
35-
from_integer('9', char_type),
36-
from_integer(radix, int_type)), ns));
31+
is_digit_with_radix(from_integer('9', char_type), radix_expr), ns));
3732
REQUIRE(false_exprt()==simplify_expr(
38-
is_digit_with_radix(
39-
from_integer('a', char_type),
40-
from_integer(radix, int_type)), ns));
33+
is_digit_with_radix(from_integer('a', char_type), radix_expr), ns));
4134
}
4235
WHEN("Radix 8")
4336
{
44-
int radix=8;
37+
const constant_exprt radix_expr=from_integer(8, char_type);
4538
REQUIRE(true_exprt()==simplify_expr(
46-
is_digit_with_radix(
47-
from_integer('7', char_type),
48-
from_integer(radix, int_type)), ns));
39+
is_digit_with_radix(from_integer('7', char_type), radix_expr), ns));
4940
REQUIRE(false_exprt()==simplify_expr(
50-
is_digit_with_radix(
51-
from_integer('8', char_type),
52-
from_integer(radix, int_type)), ns));
41+
is_digit_with_radix(from_integer('8', char_type), radix_expr), ns));
5342
}
5443
WHEN("Radix 16")
5544
{
56-
int radix=16;
45+
const constant_exprt radix_expr=from_integer(16, char_type);
5746
REQUIRE(true_exprt()==simplify_expr(
58-
is_digit_with_radix(
59-
from_integer('a', char_type),
60-
from_integer(radix, int_type)), ns));
47+
is_digit_with_radix(from_integer('a', char_type), radix_expr), ns));
6148
REQUIRE(true_exprt()==simplify_expr(
62-
is_digit_with_radix(
63-
from_integer('A', char_type),
64-
from_integer(radix, int_type)), ns));
49+
is_digit_with_radix(from_integer('A', char_type), radix_expr), ns));
6550
REQUIRE(true_exprt()==simplify_expr(
66-
is_digit_with_radix(
67-
from_integer('f', char_type),
68-
from_integer(radix, int_type)), ns));
51+
is_digit_with_radix(from_integer('f', char_type), radix_expr), ns));
6952
REQUIRE(false_exprt()==simplify_expr(
70-
is_digit_with_radix(
71-
from_integer('g', char_type),
72-
from_integer(radix, int_type)), ns));
53+
is_digit_with_radix(from_integer('g', char_type), radix_expr), ns));
7354
}
7455
}

0 commit comments

Comments
 (0)