Pointer cleanup by kroening · Pull Request #1154 · diffblue/cbmc

kroening · 2017-07-19T11:43:43Z

This is in preparation for giving pointers a width (much like integers), using constructors and a service function to produce pointer and reference types whenever appropriate.

Split off PR #970.

tautschnig · 2017-07-19T11:46:35Z

src/ansi-c/ansi_c_entry_point.cpp

        index.copy_to_operands(zero_string, from_integer(0, uint_type()));
-        exprt address_of("address_of", pointer_typet());
-        address_of.type().subtype()=char_type();
+        exprt address_of("address_of", pointer_type(char_type()));


Please use address_of_exprt

Happy to approve once pushed.

tautschnig · 2017-07-19T11:47:53Z

src/cpp/cpp_constructor.cpp

-    address_of.type().subtype()=object_tc.type();
-    address_of.copy_to_operands(object_tc);
+    exprt address_of=
+      address_of_exprt(object_tc, pointer_type(object_tc.type()));


address_of_exprt address_of(object_tc...);

tautschnig · 2017-07-19T11:48:13Z

src/cpp/cpp_destructor.cpp

-    address_of.type().subtype()=object.type();
-    address_of.copy_to_operands(object);
+    exprt address_of=
+      address_of_exprt(object, pointer_type(object.type()));


tautschnig · 2017-07-19T11:48:39Z

src/cpp/cpp_typecheck_conversions.cpp

+  index_exprt index(
+    expr,
+    from_integer(0, index_type()),
+    expr.type().subtype());


The third argument is not necessary

tautschnig · 2017-07-19T11:49:36Z

src/cpp/cpp_typecheck_conversions.cpp

-                  expr_pfrom, pto, expr_ptmp, tmp_rank))
+            // try derived-to-base conversion
+            exprt expr_pfrom=
+              address_of_exprt(expr, pointer_type(expr.type()));


addres_of_exprt expr_pfrom...

tautschnig · 2017-07-19T11:55:08Z

src/goto-symex/auto_objects.cpp


      address_of_exprt address_of_expr=
-        address_of_exprt(make_auto_object(type.subtype()));
+        address_of_exprt(


Use constructor, not assignment

tautschnig · 2017-07-19T11:55:28Z

src/java_bytecode/java_bytecode_convert_class.cpp


 #include <util/namespace.h>
 #include <util/std_expr.h>
+#include <util/c_types.h>


Nit picking as above

tautschnig · 2017-07-19T11:55:38Z

src/java_bytecode/java_bytecode_convert_method.cpp

 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
 #include <util/simplify_expr.h>
+#include <util/c_types.h>


Nit picking as above

tautschnig · 2017-07-19T11:56:44Z

src/solvers/smt2/smt2_conv.cpp

 #include <util/base_type.h>
 #include <util/string2int.h>
 #include <util/invariant.h>
+#include <util/c_types.h>


Nit picking as above

tautschnig · 2017-07-19T11:58:22Z

src/util/std_expr.cpp

+
+\*******************************************************************/
+
+address_of_exprt::address_of_exprt(const exprt &_op):


Is this actually being used? Most (all?) calls above appear to use a two-argument constructor

Now using it more.

tautschnig · 2017-07-20T09:57:20Z

src/ansi-c/ansi_c_entry_point.cpp

Could use array_of_exprt array_of(... here

tautschnig · 2017-07-20T09:58:13Z

src/ansi-c/ansi_c_entry_point.cpp

index_exprt index_expr(...) and the lines below should be eliminated

tautschnig · 2017-07-20T09:58:48Z

src/ansi-c/ansi_c_entry_point.cpp

index_exprt index_expr(... and again code below to be eliminated

tautschnig · 2017-07-20T10:00:52Z

src/cpp/cpp_typecheck_conversions.cpp

Might be a candidate for address_of_exprt address_of(...

Unfortunately not, as this might turn into a dereference expression.

tautschnig · 2017-07-20T10:02:23Z

src/goto-programs/string_instrumentation.cpp

index_exprt index(...

kroening mentioned this pull request Jul 19, 2017

Pointers get a width #970

Merged

tautschnig requested changes Jul 19, 2017

View reviewed changes

kroening force-pushed the pointer-cleanup branch 2 times, most recently from 894a5b3 to c73ee7a Compare July 20, 2017 09:54

tautschnig requested changes Jul 20, 2017

View reviewed changes

kroening force-pushed the pointer-cleanup branch from c73ee7a to 9dd44d6 Compare July 20, 2017 13:25

tautschnig approved these changes Jul 20, 2017

View reviewed changes

kroening added 5 commits July 20, 2017 15:02

get rid of typet(ID_pointer)

d0c9bd3

use pointer_type() instead of pointer_typet()

13f3d5f

address_of now needs a pointer type

636655d

removed an assert

d430319

include order cleanup

db71221

kroening force-pushed the pointer-cleanup branch from 9dd44d6 to db71221 Compare July 20, 2017 14:02

tautschnig merged commit f8b8f9e into master Jul 20, 2017

tautschnig deleted the pointer-cleanup branch July 20, 2017 18:24


		\*******************************************************************/

		address_of_exprt::address_of_exprt(const exprt &_op):

Conversation

kroening commented Jul 19, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants