From d57e21bc8ba1313ed1b5707d31616d80a0350736 Mon Sep 17 00:00:00 2001 From: Owen Date: Thu, 28 Feb 2019 10:05:22 +0000 Subject: [PATCH] Remove redundant code in ID_dynamic_object branch This branch is not taken by symex but it is taken by the slicer. The code I've removed has no effect, as far as I can tell, and may have been left over from an old implementation from before the beginning of the git history. Note, there is a commit that splits ID_dynamic_object into two different ids. See #2646 and #3769 for more details. --- src/pointer-analysis/value_set_dereference.cpp | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index c125e2a41cc..fddb2a77568 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -293,15 +293,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( } else if(root_object.id()==ID_dynamic_object) { - // const dynamic_object_exprt &dynamic_object= - // to_dynamic_object_expr(root_object); - - // the object produced by malloc - exprt malloc_object= - ns.lookup(CPROVER_PREFIX "malloc_object").symbol_expr(); - - exprt is_malloc_object=same_object(pointer_expr, malloc_object); - // constraint that it actually is a dynamic object // this is also our guard result.pointer_guard = dynamic_object(pointer_expr);