Forked from
pub / Frama Clang
633 commits behind the upstream repository.
-
Virgile Prevosto authored
it seems that this is not consistent across clang versions.
Virgile Prevosto authoredit seems that this is not consistent across clang versions.
pointer_to_virtual_method.res.oracle 11.17 KiB
[kernel] Parsing tests/basic/pointer_to_virtual_method.cpp (external front-end)
Now output intermediate result
/* Generated by Frama-C */
struct _frama_c_vmt_content {
void (*method_ptr)() ;
int shift_this ;
};
struct _frama_c_rtti_name_info_node;
struct _frama_c_vmt {
struct _frama_c_vmt_content *table ;
int table_size ;
struct _frama_c_rtti_name_info_node *rtti_info ;
};
struct _frama_c_rtti_name_info_content {
struct _frama_c_rtti_name_info_node *value ;
int shift_object ;
int shift_vmt ;
};
struct _frama_c_rtti_name_info_node {
char const *name ;
struct _frama_c_rtti_name_info_content *base_classes ;
int number_of_base_classes ;
struct _frama_c_vmt *pvmt ;
};
struct Foo;
struct Foo {
struct _frama_c_vmt *pvmt ;
};
struct Bar;
struct Bar {
struct Foo _frama_c__Z3Foo ;
};
static int g = 0;
void Foo::Ctor(struct Foo const *this);
void Foo::Dtor(struct Foo const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid(this); */
void m(struct Foo *this, int i)
{
g = i;
return;
}
/*@ requires \valid_read(this); */
void Foo::Dtor(struct Foo const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
return;
}
/*@ requires \valid_read(this); */
void Foo::Ctor(struct Foo const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
return;
}
int _frama_c_find_dynamic_cast_aux(struct _frama_c_rtti_name_info_node *target_info,
struct _frama_c_rtti_name_info_content *concrete_base,
int number_of_bases,
int found_shift_object,
int found_shift_vmt, int last_shift_vmt,
int *shift_object, int *distance){
int result = 0;
struct _frama_c_rtti_name_info_content *cursor = concrete_base;
int is_over = 0;
int base_index = 0;
while (base_index < number_of_bases) {
if (cursor->value == target_info) {
if (*distance < 0) goto _LOR;
else
if (*distance >= 1) {
_LOR:
{
if (found_shift_vmt == cursor->shift_vmt) *distance = 0;
else *distance = 1;
*shift_object = found_shift_object - cursor->shift_object;
result = 1;
}
}
}
else
if (cursor->shift_vmt <= found_shift_vmt) {
int tmp_5;
if (base_index < number_of_bases - 1) tmp_5 = (cursor + 1)->shift_vmt > found_shift_vmt;
else {
int tmp_4;
if (last_shift_vmt == -1) tmp_4 = 1;
else
if (found_shift_vmt < last_shift_vmt) tmp_4 = 1; else tmp_4 = 0;
tmp_5 = tmp_4;
}
if (tmp_5) {
int tmp_0;
int tmp;
int local_distance = 0;
int local_shift_object = 0;
if (base_index < number_of_bases - 1) tmp = (cursor + 1)->shift_vmt;
else tmp = last_shift_vmt;
;
;
;
;
;
tmp_0 = _frama_c_find_dynamic_cast_aux(target_info,
(cursor->value)->base_classes,
(cursor->value)->number_of_base_classes,
found_shift_object - cursor->shift_object,
found_shift_vmt - cursor->shift_vmt,
tmp,& local_shift_object,
& local_distance);
int local_result = tmp_0;
if (local_result != 0)
if (local_distance >= 0)
if (*distance < 0) goto _LOR_0;
else
if (*distance >= local_distance) {
_LOR_0:
{
result = local_result;
*shift_object = local_shift_object - cursor->shift_object;
*distance = local_distance;
}
}
is_over = 1;
}
else goto _LAND;
}
else {
_LAND: ;
if (*distance < 0) goto _LOR_2;
else if (*distance >= 1) {
_LOR_2:
{
int tmp_2;
int tmp_1;
int local_distance_0 = 0;
int local_shift_object_0 = 0;
if (base_index < number_of_bases + 1) tmp_1 = (cursor + 1)->shift_vmt;
else tmp_1 = last_shift_vmt;
;
;
;
;
;
tmp_2 = _frama_c_find_dynamic_cast_aux(target_info,
(cursor->value)->base_classes,
(cursor->value)->number_of_base_classes,
found_shift_object - cursor->shift_object,
found_shift_vmt - cursor->shift_vmt,
tmp_1,
& local_shift_object_0,
& local_distance_0);
int local_result_0 = tmp_2;
if (local_result_0 != 0)
if (local_distance_0 >= 0)
if (*distance < 0) goto _LOR_1;
else {
int tmp_3;
if (is_over == 0) tmp_3 = local_distance_0;
else tmp_3 = local_distance_0 + 1;
;
if (*distance > tmp_3) {
_LOR_1:
{
result = local_result_0;
*shift_object = local_shift_object_0 - cursor->shift_object;
*distance = local_distance_0 + 1;
}
}
}
}
}
}
cursor ++;
base_index ++;
}
return result;
}
int _frama_c_find_dynamic_cast(struct _frama_c_rtti_name_info_node *declared_info,
struct _frama_c_vmt *declared_vmt,
struct _frama_c_rtti_name_info_node *target_info,
int *shift_object)
{
int __retres;
int shift_vmt;
int elaborated_shift_target;
struct _frama_c_rtti_name_info_content *cursor;
int number_of_bases;
int tmp_0;
struct _frama_c_rtti_name_info_node *concrete_info =
declared_vmt->rtti_info;
int elaborated_shift_vmt = 0;
int elaborated_shift_object = 0;
int cursor_index = 0;
int distance = -1;
if (concrete_info->pvmt > declared_vmt) {
__retres = 0;
goto return_label;
} else
if (declared_vmt > concrete_info->pvmt + declared_vmt->table_size) {
__retres = 0;
goto return_label;
}
shift_vmt = declared_vmt - concrete_info->pvmt;
if (concrete_info == declared_info) {
*shift_object = 0;
__retres = target_info == declared_info;
goto return_label;
}
if (target_info == concrete_info) elaborated_shift_target = 0;
else elaborated_shift_target = -1;
cursor = concrete_info->base_classes;
number_of_bases = concrete_info->number_of_base_classes;
while (1) {
while (1) {
if (cursor_index < number_of_bases) {
if (! (elaborated_shift_vmt + cursor->shift_vmt < shift_vmt))
break;
}
else break;
{
struct _frama_c_rtti_name_info_content *tmp;
if (cursor_index < number_of_bases - 1) tmp = cursor + 1;
else tmp = (struct _frama_c_rtti_name_info_content *)0;
struct _frama_c_rtti_name_info_content *next_cursor = tmp;
if (next_cursor != (struct _frama_c_rtti_name_info_content *)0)
if (elaborated_shift_vmt + next_cursor->shift_vmt <= shift_vmt) {
cursor = next_cursor;
cursor_index ++;
}
else break;
else break;
}
}
if (cursor_index < number_of_bases) {
elaborated_shift_vmt += cursor->shift_vmt;
elaborated_shift_object += cursor->shift_object;
if (cursor->value == target_info) elaborated_shift_target = elaborated_shift_object;
if (elaborated_shift_vmt == shift_vmt)
if (cursor->value == declared_info) {
if (elaborated_shift_target >= 0) {
*shift_object = elaborated_shift_target - elaborated_shift_object;
__retres = 1;
goto return_label;
}
break;
}
cursor = (cursor->value)->base_classes;
number_of_bases = (cursor->value)->number_of_base_classes;
cursor_index = 0;
}
if (! (cursor_index < number_of_bases)) break;
}
if (cursor_index >= number_of_bases) {
__retres = 0;
goto return_label;
}
tmp_0 = _frama_c_find_dynamic_cast_aux(target_info,
concrete_info->base_classes,
concrete_info->number_of_base_classes,
elaborated_shift_object,shift_vmt,
-1,shift_object,& distance);
__retres = tmp_0;
return_label: return __retres;
}
struct _frama_c_vmt_content _frama_c_vmt[1] =
{{.method_ptr = (void (*)())(& m), .shift_this = 0}};struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "Foo",
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 1,
.rtti_info = & _frama_c_rtti_name_info};
void Bar::Ctor(struct Bar const *this);
void Bar::Dtor(struct Bar const *this);
struct _frama_c_vmt _frama_c_vmt_header;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];
struct _frama_c_vmt_content _frama_c_vmt[1];
/*@ requires \valid(this); */
void m(struct Bar *this, int i)
{
g = 2 * i;
return;
}
/*@ requires \valid_read(this); */
void Bar::Dtor(struct Bar const *this)
{
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
Foo::Dtor(& this->_frama_c__Z3Foo);
return;
}
/*@ requires \valid_read(this); */
void Bar::Ctor(struct Bar const *this)
{
Foo::Ctor(& this->_frama_c__Z3Foo);
*((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
return;
}
struct _frama_c_vmt_content _frama_c_vmt[1] =
{{.method_ptr = (void (*)())(& m), .shift_this = 0}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
{{.value = & _frama_c_rtti_name_info,
.shift_object = (char *)0 - (char *)(& ((struct Bar *)0)->_frama_c__Z3Foo),
.shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "Bar",
.base_classes = _frama_c_base_classes,
.number_of_base_classes = 1,
.pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
{.table = _frama_c_vmt,
.table_size = 1,
.rtti_info = & _frama_c_rtti_name_info};
int main(void)
{
void (*mptr)(struct Foo *, int ) = & m;
struct Bar bar;
Bar::Ctor(& bar);
struct Foo *mbar = & bar._frama_c__Z3Foo;
(*mptr)(mbar,42);
Bar::Dtor((struct Bar const *)(& bar));
return g;
}