Skip to content

Commit 57a6cb7

Browse files
author
Owen Jones
committed
Finished factory
Structs work now without segfault
1 parent e72a7c6 commit 57a6cb7

9 files changed

+37
-43
lines changed

‎src/analyses/variable-sensitivity/abstract_enviroment.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ abstract_object_pointert abstract_environmentt::eval(
7272
std::dynamic_pointer_cast<struct_abstract_objectt>(
7373
eval(member_expr.compound(), ns));
7474

75-
return struct_abstract_object->read_component(*this, member_expr);
75+
return struct_abstract_object->read_component(*this, member_expr, ns);
7676
}
7777
},
7878
{
@@ -105,7 +105,7 @@ abstract_object_pointert abstract_environmentt::eval(
105105
std::dynamic_pointer_cast<array_abstract_objectt>(
106106
eval(index_expr.array(), ns));
107107

108-
return array_abstract_object->read_index(*this, index_expr);
108+
return array_abstract_object->read_index(*this, index_expr, ns);
109109
}
110110
}
111111
};
@@ -389,7 +389,7 @@ Function: abstract_environmentt::abstract_object_factory
389389
abstract_object_pointert abstract_environmentt::abstract_object_factory(
390390
const typet type, const namespacet &ns, bool top, bool bottom) const
391391
{
392-
constant_exprt empty_constant_expr=constant_exprt();
392+
exprt empty_constant_expr=exprt();
393393
return abstract_object_factory(type, top, bottom, empty_constant_expr, ns);
394394
}
395395

@@ -409,7 +409,7 @@ Function: abstract_environmentt::abstract_object_factory
409409
\*******************************************************************/
410410

411411
abstract_object_pointert abstract_environmentt::abstract_object_factory(
412-
const typet type, const exprt e, const namespacet &ns) const
412+
const typet type, const exprt &e, const namespacet &ns) const
413413
{
414414
return abstract_object_factory(type, false, false, e, ns);
415415
}
@@ -432,7 +432,7 @@ Function: abstract_environmentt::abstract_object_factory
432432
\*******************************************************************/
433433

434434
abstract_object_pointert abstract_environmentt::abstract_object_factory(
435-
const typet type, bool top, bool bottom, const constant_exprt e,
435+
const typet type, bool top, bool bottom, const exprt &e,
436436
const namespacet &ns) const
437437
{
438438
return variable_sensitivity_object_factoryt::instance().get_abstract_object(

‎src/analyses/variable-sensitivity/abstract_enviroment.h

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ class abstract_environmentt
4343
// For converting constants in the program
4444
// Maybe these two should be compacted to one call...
4545
virtual abstract_object_pointert abstract_object_factory(
46-
const typet type, const exprt e, const namespacet &ns) const;
46+
const typet type, const exprt &e, const namespacet &ns) const;
4747

4848

4949
virtual bool merge(const abstract_environmentt &env);
@@ -73,15 +73,12 @@ class abstract_environmentt
7373
virtual abstract_object_pointert eval_expression(
7474
const exprt &e, const namespacet &ns) const;
7575

76-
// Hook for domain specific handling of operators
77-
virtual abstract_object_pointert eval_rest(const exprt &e) const;
78-
7976
typedef symbol_exprt map_keyt;
8077
std::map<map_keyt, abstract_object_pointert> map;
8178

8279
private:
8380
abstract_object_pointert abstract_object_factory(
84-
const typet type, bool top, bool bottom, const constant_exprt e,
81+
const typet type, bool top, bool bottom, const exprt &e,
8582
const namespacet &ns) const;
8683
};
8784

‎src/analyses/variable-sensitivity/array_abstract_object.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ Function: array_abstract_objectt::array_abstract_objectt
8585
8686
\*******************************************************************/
8787

88-
array_abstract_objectt::array_abstract_objectt(const constant_exprt &e):
88+
array_abstract_objectt::array_abstract_objectt(const exprt &e):
8989
abstract_objectt(e)
9090
{
9191
assert(e.type().id()==ID_array);

‎src/analyses/variable-sensitivity/array_abstract_object.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ class array_abstract_objectt:public abstract_objectt
2222
explicit array_abstract_objectt(const typet &type);
2323
array_abstract_objectt(const typet &type, bool top, bool bottom);
2424
explicit array_abstract_objectt(const array_abstract_objectt &old);
25-
explicit array_abstract_objectt(const constant_exprt &expr);
25+
explicit array_abstract_objectt(const exprt &expr);
2626

2727
CLONE
2828
MERGE(abstract_objectt)

‎src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -276,7 +276,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
276276
// Return top if dereferencing a null pointer or we are top
277277
bool is_value_top = top || value.id()==ID_nil;
278278
return env.abstract_object_factory(
279-
type.subtype(), is_value_top, !is_value_top);
279+
type.subtype(), ns, is_value_top, !is_value_top);
280280
}
281281
else
282282
{
@@ -287,11 +287,11 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
287287
else if(value.id()==ID_constant)
288288
{
289289
// Reading a null pointer, return top
290-
return env.abstract_object_factory(type.subtype(), true, false);
290+
return env.abstract_object_factory(type.subtype(), ns, true, false);
291291
}
292292
else
293293
{
294-
return env.abstract_object_factory(type.subtype(), true, false);
294+
return env.abstract_object_factory(type.subtype(), ns, true, false);
295295
}
296296
}
297297
}

‎src/analyses/variable-sensitivity/struct_abstract_object.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,7 @@ Function: struct_abstract_objectt::struct_abstract_objectt
8686
8787
\*******************************************************************/
8888

89-
struct_abstract_objectt::struct_abstract_objectt(const constant_exprt &e):
89+
struct_abstract_objectt::struct_abstract_objectt(const exprt &e):
9090
abstract_objectt(e)
9191
{
9292
assert(e.type().id()==ID_struct);

‎src/analyses/variable-sensitivity/struct_abstract_object.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ class struct_abstract_objectt:public abstract_objectt
2121
explicit struct_abstract_objectt(const typet &type);
2222
struct_abstract_objectt(const typet &type, bool top, bool bottom);
2323
explicit struct_abstract_objectt(const struct_abstract_objectt &old);
24-
explicit struct_abstract_objectt(const constant_exprt &expr);
24+
explicit struct_abstract_objectt(const exprt &expr);
2525

2626
CLONE
2727
MERGE(abstract_objectt)

‎src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp

Lines changed: 20 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -4,24 +4,19 @@
44
variable_sensitivity_object_factoryt
55
variable_sensitivity_object_factoryt::s_instance;
66

7-
variable_sensitivity_object_factoryt::variable_sensitivity_object_factoryt()
8-
{
9-
10-
}
11-
127
variable_sensitivity_object_factoryt::ABSTRACT_OBJECT_TYPET
138
variable_sensitivity_object_factoryt::get_abstract_object_type(
149
const typet type, const namespacet &ns)
1510
{
1611
ABSTRACT_OBJECT_TYPET abstract_object_type=TWO_VALUE;
17-
typet followed_type = ns.follow(type);
18-
if(followed_type.id()==ID_signedbv || followed_type.id()==ID_unsignedbv ||
19-
followed_type.id()==ID_floatbv || followed_type.id()==ID_fixedbv ||
20-
followed_type.id()==ID_c_bool)
12+
13+
if(type.id()==ID_signedbv || type.id()==ID_unsignedbv ||
14+
type.id()==ID_floatbv || type.id()==ID_fixedbv ||
15+
type.id()==ID_c_bool)
2116
{
2217
abstract_object_type=CONSTANT;
2318
}
24-
else if(followed_type.id()==ID_array)
19+
else if(type.id()==ID_array)
2520
{
2621
if(has_arrays_flag)
2722
{
@@ -32,7 +27,7 @@ variable_sensitivity_object_factoryt::ABSTRACT_OBJECT_TYPET
3227
abstract_object_type=ARRAY_INSENSITIVE;
3328
}
3429
}
35-
else if(followed_type.id()==ID_pointer)
30+
else if(type.id()==ID_pointer)
3631
{
3732
if(has_pointers_flag)
3833
{
@@ -43,7 +38,7 @@ variable_sensitivity_object_factoryt::ABSTRACT_OBJECT_TYPET
4338
abstract_object_type=POINTER_INSENSITIVE;
4439
}
4540
}
46-
else if(followed_type.id()==ID_struct)
41+
else if(type.id()==ID_struct)
4742
{
4843
if(has_structs_flag)
4944
{
@@ -62,46 +57,47 @@ variable_sensitivity_object_factoryt::ABSTRACT_OBJECT_TYPET
6257

6358
abstract_object_pointert variable_sensitivity_object_factoryt::
6459
get_abstract_object(
65-
const typet type, bool top, bool bottom, const constant_exprt e,
60+
const typet type, bool top, bool bottom, const exprt &e,
6661
const namespacet &ns)
6762
{
68-
ABSTRACT_OBJECT_TYPET abstract_object_type=get_abstract_object_type(type, ns);
63+
typet followed_type = ns.follow(type);
64+
ABSTRACT_OBJECT_TYPET abstract_object_type=get_abstract_object_type(followed_type, ns);
6965

7066
if(top || bottom)
7167
{
7268
switch(abstract_object_type)
7369
{
7470
case CONSTANT:
7571
return abstract_object_pointert(
76-
new constant_abstract_valuet(type, top, bottom));
72+
new constant_abstract_valuet(followed_type, top, bottom));
7773
case ARRAY_SENSITIVE:
7874
return abstract_object_pointert(
79-
new array_abstract_objectt(type, top, false));
75+
new array_abstract_objectt(followed_type, top, false));
8076
case ARRAY_INSENSITIVE:
8177
return abstract_object_pointert(
82-
new array_abstract_objectt(type, top, false));
78+
new array_abstract_objectt(followed_type, top, false));
8379
case POINTER_SENSITIVE:
8480
return abstract_object_pointert(
85-
new pointer_abstract_objectt(type, top, false));
81+
new pointer_abstract_objectt(followed_type, top, false));
8682
case POINTER_INSENSITIVE:
8783
return abstract_object_pointert(
88-
new pointer_abstract_objectt(type, top, false));
84+
new pointer_abstract_objectt(followed_type, top, false));
8985
case STRUCT_SENSITIVE:
9086
return abstract_object_pointert(
91-
new struct_abstract_objectt(type, top, false));
87+
new struct_abstract_objectt(followed_type, top, false));
9288
case STRUCT_INSENSITIVE:
9389
return abstract_object_pointert(
94-
new struct_abstract_objectt(type, top, false));
90+
new struct_abstract_objectt(followed_type, top, false));
9591
case TWO_VALUE:
96-
return abstract_object_pointert(new abstract_objectt(type, top, false));
92+
return abstract_object_pointert(new abstract_objectt(followed_type, top, false));
9793
default:
9894
assert(false);
99-
return abstract_object_pointert(new abstract_objectt(type, top, false));
95+
return abstract_object_pointert(new abstract_objectt(followed_type, top, false));
10096
}
10197
}
10298
else
10399
{
104-
assert(type==e.type());
100+
assert(followed_type==e.type());
105101
switch(abstract_object_type)
106102
{
107103
case CONSTANT:

‎src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,12 +16,13 @@ class variable_sensitivity_object_factoryt
1616
return s_instance;
1717
}
1818
abstract_object_pointert get_abstract_object(
19-
const typet type, bool top, bool bottom, const constant_exprt e,
19+
const typet type, bool top, bool bottom, const exprt &e,
2020
const namespacet &ns);
2121
void set_options(optionst &options);
2222

2323
private:
24-
variable_sensitivity_object_factoryt();
24+
variable_sensitivity_object_factoryt()
25+
{}
2526
static variable_sensitivity_object_factoryt s_instance;
2627
enum ABSTRACT_OBJECT_TYPET
2728
{

0 commit comments

Comments
 (0)