From 3e51f30fff5e57a90ac17c65a46105e5d21136ed Mon Sep 17 00:00:00 2001
From: klaas <klaas@u6001af26f9d45e.ant.amazon.com>
Date: Wed, 1 Aug 2018 09:51:41 -0400
Subject: [PATCH 1/5] Cleans up some loops to have braces

---
 src/analyses/dependence_graph.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index 24c0320af66..ada58117611 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -175,7 +175,9 @@ void dep_graph_domaint::data_dependencies(
     {
       bool found=false;
       for(const auto &wr : w_range.second)
+      {
         for(const auto &r_range : r_ranges)
+        {
           if(!found &&
              may_be_def_use_pair(wr.first, wr.second,
                                  r_range.first, r_range.second))
@@ -184,6 +186,8 @@ void dep_graph_domaint::data_dependencies(
             data_deps.insert(w_range.first);
             found=true;
           }
+        }
+      }
     }
 
     dep_graph.reaching_definitions()[to].clear_cache(it->first);

From f1ff824d00fb4d9994af7aedd7bd609f1ee98247 Mon Sep 17 00:00:00 2001
From: klaas <klaas@u6001af26f9d45e.ant.amazon.com>
Date: Thu, 28 Jun 2018 12:04:05 -0400
Subject: [PATCH 2/5] Disambiguates two exprts with the same ID.

This commit resolves an issue where ID_dynamic_object was used to
label two semantically distinct exprts.

One, with a single operand, was a boolean expression meaning that
the operand is a pointer to a dynamic object. This has been renamed
to ID_is_dynamic_object.

The second, with two operands, is an exprt representing a dynamic
object itself. This has stayed ID_dynamic_object.

Disambiguating which meaning was intended in each case was relatively
easy, as uses of these exprts frequently come with assertions
about the number of operands, and so this was used to inform which
instances of ID_dynamic_object should be changed and which should
be left the same.
---
 regression/goto-instrument/slice19/test.desc |  2 +-
 src/ansi-c/c_typecheck_expr.cpp              |  7 ++-
 src/ansi-c/expr2c.cpp                        |  4 +-
 src/solvers/flattening/bv_pointers.cpp       |  4 +-
 src/solvers/smt2/smt2_conv.cpp               |  2 +-
 src/util/irep_ids.def                        |  1 +
 src/util/pointer_predicates.cpp              |  2 +-
 src/util/simplify_expr.cpp                   |  4 +-
 src/util/simplify_expr_class.h               |  2 +-
 src/util/simplify_expr_int.cpp               |  4 +-
 src/util/simplify_expr_pointer.cpp           | 12 ++---
 src/util/std_expr.h                          | 48 ++++++++++++++++++++
 12 files changed, 70 insertions(+), 22 deletions(-)

diff --git a/regression/goto-instrument/slice19/test.desc b/regression/goto-instrument/slice19/test.desc
index 03cff4a4fac..3793f7374e1 100644
--- a/regression/goto-instrument/slice19/test.desc
+++ b/regression/goto-instrument/slice19/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice
 ^EXIT=0$
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 26091bb88ca..f5ec9945673 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2141,11 +2141,10 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
-    dynamic_object_expr.operands()=expr.arguments();
-    dynamic_object_expr.add_source_location()=source_location;
+    exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]);
+    is_dynamic_object_expr.add_source_location() = source_location;
 
-    return dynamic_object_expr;
+    return is_dynamic_object_expr;
   }
   else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
   {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 80b5515dd0f..e5318b5e730 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3580,8 +3580,8 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_invalid_pointer)
     return convert_function(src, "__CPROVER_invalid_pointer", precedence=16);
 
-  else if(src.id()==ID_dynamic_object)
-    return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
+  else if(src.id()==ID_is_dynamic_object)
+    return convert_function(src, "IS_DYNAMIC_OBJECT", precedence=16);
 
   else if(src.id()=="is_zero_string")
     return convert_function(src, "IS_ZERO_STRING", precedence=16);
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 5cf7ade92c8..5de771c07e9 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -45,7 +45,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
       }
     }
   }
-  else if(expr.id()==ID_dynamic_object)
+  else if(expr.id()==ID_is_dynamic_object)
   {
     if(operands.size()==1 &&
        operands[0].type().id()==ID_pointer)
@@ -735,7 +735,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 void bv_pointerst::do_postponed(
   const postponedt &postponed)
 {
-  if(postponed.expr.id()==ID_dynamic_object)
+  if(postponed.expr.id()==ID_is_dynamic_object)
   {
     const pointer_logict::objectst &objects=
       pointer_logic.objects;
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index c1b14961d76..95493bce85e 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -1367,7 +1367,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     if(ext>0)
       out << ")"; // zero_extend
   }
-  else if(expr.id()==ID_dynamic_object)
+  else if(expr.id()==ID_is_dynamic_object)
   {
     convert_is_dynamic_object(expr);
   }
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index d0066054482..95f7bb6db77 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -448,6 +448,7 @@ IREP_ID_TWO(overflow_minus, overflow--)
 IREP_ID_TWO(overflow_mult, overflow-*)
 IREP_ID_TWO(overflow_unary_minus, overflow-unary-)
 IREP_ID_ONE(object_descriptor)
+IREP_ID_ONE(is_dynamic_object)
 IREP_ID_ONE(dynamic_object)
 IREP_ID_TWO(C_dynamic, #dynamic)
 IREP_ID_ONE(object_size)
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
index 668054bc493..0185d222e54 100644
--- a/src/util/pointer_predicates.cpp
+++ b/src/util/pointer_predicates.cpp
@@ -70,7 +70,7 @@ exprt dynamic_size(const namespacet &ns)
 
 exprt dynamic_object(const exprt &pointer)
 {
-  exprt dynamic_expr(ID_dynamic_object, bool_typet());
+  exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
   dynamic_expr.copy_to_operands(pointer);
   return dynamic_expr;
 }
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index f7e442e40ef..23e19a4c239 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -2266,8 +2266,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_byte_extract(to_byte_extract_expr(expr)) && result;
   else if(expr.id()==ID_pointer_object)
     result=simplify_pointer_object(expr) && result;
-  else if(expr.id()==ID_dynamic_object)
-    result=simplify_dynamic_object(expr) && result;
+  else if(expr.id()==ID_is_dynamic_object)
+    result=simplify_is_dynamic_object(expr) && result;
   else if(expr.id()==ID_invalid_pointer)
     result=simplify_invalid_pointer(expr) && result;
   else if(expr.id()==ID_object_size)
diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h
index 5e192292666..3dd7d8601e1 100644
--- a/src/util/simplify_expr_class.h
+++ b/src/util/simplify_expr_class.h
@@ -96,7 +96,7 @@ class simplify_exprt
   bool simplify_pointer_object(exprt &expr);
   bool simplify_object_size(exprt &expr);
   bool simplify_dynamic_size(exprt &expr);
-  bool simplify_dynamic_object(exprt &expr);
+  bool simplify_is_dynamic_object(exprt &expr);
   bool simplify_invalid_pointer(exprt &expr);
   bool simplify_same_object(exprt &expr);
   bool simplify_good_pointer(exprt &expr);
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 6856c6a38fc..9c6c12635ab 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1699,7 +1699,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
          expr.op0().operands().size()==1)
       {
         if(expr.op0().op0().id()==ID_symbol ||
-           expr.op0().op0().id()==ID_dynamic_object ||
+           expr.op0().op0().id()==ID_is_dynamic_object ||
            expr.op0().op0().id()==ID_member ||
            expr.op0().op0().id()==ID_index ||
            expr.op0().op0().id()==ID_string_constant)
@@ -1715,7 +1715,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
               expr.op0().op0().operands().size()==1)
       {
         if(expr.op0().op0().op0().id()==ID_symbol ||
-           expr.op0().op0().op0().id()==ID_dynamic_object ||
+           expr.op0().op0().op0().id()==ID_is_dynamic_object ||
            expr.op0().op0().op0().id()==ID_member ||
            expr.op0().op0().op0().id()==ID_index ||
            expr.op0().op0().op0().id()==ID_string_constant)
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index b183c81890b..f0e44fc9d2f 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -464,7 +464,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
     {
       if(op.operands().size()!=1 ||
          (op.op0().id()!=ID_symbol &&
-          op.op0().id()!=ID_dynamic_object &&
+          op.op0().id()!=ID_is_dynamic_object &&
           op.op0().id()!=ID_string_constant))
         return true;
     }
@@ -508,18 +508,18 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
   return result;
 }
 
-bool simplify_exprt::simplify_dynamic_object(exprt &expr)
+bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return true;
+  // This should hold as a result of the expr ID being is_dynamic_object.
+  PRECONDITION(expr.operands().size() == 1);
 
   exprt &op=expr.op0();
 
   if(op.id()==ID_if && op.operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
-    simplify_dynamic_object(if_expr.true_case());
-    simplify_dynamic_object(if_expr.false_case());
+    simplify_is_dynamic_object(if_expr.true_case());
+    simplify_is_dynamic_object(if_expr.false_case());
     simplify_if(if_expr);
     expr.swap(if_expr);
 
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index e979f45ee69..bf44ed8451a 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -2106,6 +2106,54 @@ inline void validate_expr(const dynamic_object_exprt &value)
 }
 
 
+/*! \brief Evaluates to true if the operand is a pointer to a dynamic object.
+*/
+class is_dynamic_object_exprt:public unary_predicate_exprt
+{
+public:
+  is_dynamic_object_exprt():unary_predicate_exprt(ID_is_dynamic_object)
+  {
+  }
+
+  explicit is_dynamic_object_exprt(const exprt &op):
+    unary_predicate_exprt(ID_is_dynamic_object, op)
+  {
+  }
+};
+
+/*! \brief Cast a generic exprt to a \ref is_dynamic_object_exprt
+ *
+ * This is an unchecked conversion. \a expr must be known to be \ref
+ * is_dynamic_object_exprt.
+ *
+ * \param expr Source expression
+ * \return Object of type \ref is_dynamic_object_exprt
+ *
+ * \ingroup gr_std_expr
+*/
+inline const is_dynamic_object_exprt &to_is_dynamic_object_expr(
+  const exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_is_dynamic_object);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "is_dynamic_object must have one operand");
+  return static_cast<const is_dynamic_object_exprt &>(expr);
+}
+
+/*! \copydoc to_is_dynamic_object_expr(const exprt &)
+ * \ingroup gr_std_expr
+*/
+inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_is_dynamic_object);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "is_dynamic_object must have one operand");
+  return static_cast<is_dynamic_object_exprt &>(expr);
+}
+
+
 /*! \brief semantic type conversion
 */
 class typecast_exprt:public unary_exprt

From 9d8cef40c35c8c66379ef070bdc01506d9625d77 Mon Sep 17 00:00:00 2001
From: klaas <klaas@u6001af26f9d45e.ant.amazon.com>
Date: Thu, 2 Aug 2018 16:54:10 -0400
Subject: [PATCH 3/5] Turns some checks into DATA_INVARIANTs

---
 src/solvers/flattening/bv_pointers.cpp | 22 +++++++++++-----------
 src/util/simplify_expr_pointer.cpp     |  6 ++++--
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 5de771c07e9..5a69827092c 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -47,19 +47,19 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
   }
   else if(expr.id()==ID_is_dynamic_object)
   {
-    if(operands.size()==1 &&
-       operands[0].type().id()==ID_pointer)
-    {
-      // we postpone
-      literalt l=prop.new_variable();
+    DATA_INVARIANT(operands.size() == 1 &&
+                   operands[0].type().id() == ID_pointer,
+                   std::string("is_dynamic_object_exprt should have one") +
+                   "operand, which should have pointer type.");
+    // we postpone
+    literalt l=prop.new_variable();
 
-      postponed_list.push_back(postponedt());
-      postponed_list.back().op=convert_bv(operands[0]);
-      postponed_list.back().bv.push_back(l);
-      postponed_list.back().expr=expr;
+    postponed_list.push_back(postponedt());
+    postponed_list.back().op=convert_bv(operands[0]);
+    postponed_list.back().bv.push_back(l);
+    postponed_list.back().expr=expr;
 
-      return l;
-    }
+    return l;
   }
   else if(expr.id()==ID_lt || expr.id()==ID_le ||
           expr.id()==ID_gt || expr.id()==ID_ge)
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index f0e44fc9d2f..82764d52b10 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -510,8 +510,10 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
 
 bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
 {
-  // This should hold as a result of the expr ID being is_dynamic_object.
-  PRECONDITION(expr.operands().size() == 1);
+  DATA_INVARIANT(expr.operands().size() == 1 &&
+                 expr.op0().type().id() == ID_pointer,
+                 std::string("is_dynamic_object_exprt should have one") +
+                 "operand, which should have pointer type.");
 
   exprt &op=expr.op0();
 

From b2950c441805663f61f9475d863d30aa91e623a8 Mon Sep 17 00:00:00 2001
From: klaas <klaas@u6001af26f9d45e.ant.amazon.com>
Date: Wed, 1 Aug 2018 09:55:54 -0400
Subject: [PATCH 4/5]  Fixes bugs making goto_rw too conservative

When handling the case of pointers, goto_rw would mark both the object pointed
to and the pointer itself as written. For example, if x = &i, the line `*x = 1'
would yield a write set containing both x and i, instead of just i.

This resolves that issue by ensuring that value_set_dereference always
gives at least one object that the dereference can refer to.

This also resolves a bug wherein &a is marked as reading from a by
removing the ID_symbol special case from get_objects_address_of.A
---
 src/analyses/goto_rw.cpp                      | 23 +++++++++++--------
 src/analyses/reaching_definitions.cpp         | 14 +++++------
 .../value_set_dereference.cpp                 |  8 +++++--
 3 files changed, 26 insertions(+), 19 deletions(-)

diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 55236145ab8..8b9a73181b9 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -128,8 +128,6 @@ void rw_range_sett::get_objects_dereference(
 {
   const exprt &pointer=deref.pointer();
   get_objects_rec(get_modet::READ, pointer);
-  if(mode!=get_modet::READ)
-    get_objects_rec(mode, pointer);
 }
 
 void rw_range_sett::get_objects_byte_extract(
@@ -414,16 +412,19 @@ void rw_range_sett::get_objects_typecast(
 
 void rw_range_sett::get_objects_address_of(const exprt &object)
 {
-  if(object.id() == ID_string_constant ||
+  if(object.id() == ID_symbol ||
+     object.id() == ID_string_constant ||
      object.id() == ID_label ||
      object.id() == ID_array ||
      object.id() == ID_null_object)
     // constant, nothing to do
+  {
     return;
-  else if(object.id()==ID_symbol)
-    get_objects_rec(get_modet::READ, object);
+  }
   else if(object.id()==ID_dereference)
+  {
     get_objects_rec(get_modet::READ, object);
+  }
   else if(object.id()==ID_index)
   {
     const index_exprt &index=to_index_expr(object);
@@ -524,6 +525,11 @@ void rw_range_sett::get_objects_rec(
     get_objects_array(mode, to_array_expr(expr), range_start, size);
   else if(expr.id()==ID_struct)
     get_objects_struct(mode, to_struct_expr(expr), range_start, size);
+  else if(expr.id()==ID_dynamic_object)
+  {
+    const auto obj_instance = to_dynamic_object_expr(expr).get_instance();
+    add(mode, "goto_rw::dynamic_object-" + std::to_string(obj_instance), 0, -1);
+  }
   else if(expr.id()==ID_symbol)
   {
     const symbol_exprt &symbol=to_symbol_expr(expr);
@@ -564,11 +570,6 @@ void rw_range_sett::get_objects_rec(
   {
     // dereferencing may yield some weird ones, ignore these
   }
-  else if(mode==get_modet::LHS_W)
-  {
-    forall_operands(it, expr)
-      get_objects_rec(mode, *it);
-  }
   else
     throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
 }
@@ -605,6 +606,8 @@ void rw_range_set_value_sett::get_objects_dereference(
   exprt object=deref;
   dereference(target, object, ns, value_sets);
 
+  PRECONDITION(object.is_not_nil());
+
   range_spect new_size=
     to_range_spect(pointer_offset_bits(object.type(), ns));
 
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index 7788835f0db..e3fae64dceb 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -307,19 +307,19 @@ void rd_range_domaint::transform_assign(
   {
     const irep_idt &identifier=it->first;
     // ignore symex::invalid_object
-    const symbolt *symbol_ptr;
-    if(ns.lookup(identifier, symbol_ptr))
+    const symbolt *symbol_ptr = nullptr;
+    bool not_found = ns.lookup(identifier, symbol_ptr);
+    if(not_found && has_prefix(id2string(identifier), "symex::invalid_object"))
+    {
       continue;
-    INVARIANT_STRUCTURED(
-      symbol_ptr!=nullptr,
-      nullptr_exceptiont,
-      "Symbol is in symbol table");
+    }
 
     const range_domaint &ranges=rw_set.get_ranges(it);
 
     if(is_must_alias &&
        (!rd.get_is_threaded()(from) ||
-        (!symbol_ptr->is_shared() &&
+        (symbol_ptr != nullptr &&
+         symbol_ptr->is_shared() &&
          !rd.get_is_dirty()(identifier))))
       for(const auto &range : ranges)
         kill(identifier, range.first, range.second);
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index b22ced28326..4b4ee52609e 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -358,8 +358,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     // this is also our guard
     result.pointer_guard = dynamic_object(pointer_expr);
 
-    // can't remove here, turn into *p
-    result.value=dereference_exprt(pointer_expr, dereference_type);
+    // TODO should this be object or root_object?
+    // TODO It's unclear whether this is a good approach to take --- it
+    // successfully ensures that every (non-null) dereference points to
+    // something, making the write set computation work correctly, but dynamic
+    // objects do not seem to be intended to be used in this way.
+    result.value = object;
 
     if(options.get_bool_option("pointer-check"))
     {

From 098a9a9da5e9f07fa1c68824cb4496914a062315 Mon Sep 17 00:00:00 2001
From: klaas <klaas@u6001af26f9d45e.ant.amazon.com>
Date: Tue, 31 Jul 2018 10:54:06 -0400
Subject: [PATCH 5/5] Adds slice24 test.

---
 regression/goto-instrument/slice24/main.c    | 14 ++++++++++++++
 regression/goto-instrument/slice24/test.desc |  8 ++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 regression/goto-instrument/slice24/main.c
 create mode 100644 regression/goto-instrument/slice24/test.desc

diff --git a/regression/goto-instrument/slice24/main.c b/regression/goto-instrument/slice24/main.c
new file mode 100644
index 00000000000..2149d6ba087
--- /dev/null
+++ b/regression/goto-instrument/slice24/main.c
@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+static void f(int *x) { *x = 5; }
+static void g(int *x) { assert(*x == 5); }
+
+int main(int argc, char **argv)
+{
+  int *x = (int*)malloc(sizeof(int));
+  f(x);
+  g(x);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc
new file mode 100644
index 00000000000..3906443eafc
--- /dev/null
+++ b/regression/goto-instrument/slice24/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+Data dependencies across function calls are still not working correctly.