From db79106def9cacf819c47ab8c4c2062c1c4580c8 Mon Sep 17 00:00:00 2001 From: marek-trtik Date: Tue, 17 Oct 2017 23:26:21 +0100 Subject: [PATCH] Added explanatory comment for the introduced condition. --- src/analyses/goto_rw.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index c4f9f262c79..c3c9a2ce9f5 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -613,6 +613,11 @@ void rw_range_set_value_sett::get_objects_dereference( new_size=std::min(size, new_size); } + // We must ensure that the artificial reference (introduced in + // 'value_set_dereferencet::build_reference_to') to a dynamic object + // obtained by dereferencing the pointer in 'deref' gets to the resulting + // points-to-set. The following condition check whether the obtained + // object is the artificial reference. if(object.is_not_nil() && object.id()==ID_symbol && as_string(to_symbol_expr(object).get_identifier()).find( get_vsderef_dynamic_object_prefix())==0UL)