-
Notifications
You must be signed in to change notification settings - Fork 30
Closed
Labels
cpp-syntaxRelated to generation tests for C++Related to generation tests for C++
Description
Add ability to generate tests for classes with private member.
Access to private in klee and tests by hliberacki/cpp-member-accessor.
For check access right add AccessSpecifier to field and fill by clang getAccess().
planned klee file code
MEMBER_ACCESSOR(point_x, point, x, int)
MEMBER_ACCESSOR(point_y, point, y, int)
int klee_entry__private_set_zero(int utbot_argc, char ** utbot_argv, char ** utbot_envp) {
class point t;
klee_make_symbolic(&t, sizeof(t), "t");
klee_prefer_cex(&t, accessor::accessMember<point_x>(t) >= -10 & accessor::accessMember<point_x>(t) <= 10);
klee_prefer_cex(&t, accessor::accessMember<point_y>(t) >= -10 & accessor::accessMember<point_y>(t) <= 10);
////////////////////////////////////////////
class point t_post;
klee_make_symbolic(&t_post, sizeof(t_post), "t_post");
set_zero(t);
klee_assume(accessor::accessMember<point_x>(t) == accessor::accessMember<point_x>(t_post));
klee_assume(accessor::accessMember<point_y>(t) == accessor::accessMember<point_y>(t_post));
return 0;
}
planned result test code (probably MEMBER_ACCESSOR will move to header)
MEMBER_ACCESSOR(point_x, point, x, int)
MEMBER_ACCESSOR(point_y, point, y, int)
TEST(regression, set_zero_test_1)
{
class point t = {0, 0};
set_zero(t);
class point expected_t = {0, 0};
EXPECT_EQ(accessor::accessMember<point_x>(expected_t), accessor::accessMember<point_x>(t));
EXPECT_EQ(accessor::accessMember<point_y>(expected_t), accessor::accessMember<point_y>(t));
}
Metadata
Metadata
Assignees
Labels
cpp-syntaxRelated to generation tests for C++Related to generation tests for C++
Type
Projects
Status
Done