Modified the write stack to not throw away certain pointers

Pointers into arrays was creating a top stack even though the result was
valid. Corrected so didn't throw them away (need to look at the base of
the stack, not the top). Also made the tests verify that they don't
create a top stack when they shouldn't. Also made it impossible to get
the expression of a top stack.

Author: thk123

src/analyses/variable-sensitivity/write_stack.cpp

@@ -105,10 +105,12 @@ void write_stackt::construct_stack_to_pointer(
 
     if(!top_stack)
     {
-      // check the top of the stack is pointing at an array - we don't support
-      // offset apart from within arrays
-      std::shared_ptr<const write_stack_entryt> entry=
-        *std::prev(stack.cend());
+      // check the symbol at the bottom of the stack
+      std::shared_ptr<const write_stack_entryt> entry=*stack.cbegin();
+      INVARIANT(
+        entry->get_access_expr().id()==ID_symbol,
+        "The base should be an addressable location (i.e. symbol)");
+
       if(entry->get_access_expr().type().id()!=ID_array)
       {
         top_stack=true;
@@ -175,6 +177,8 @@ void write_stackt::construct_stack_to_array_index(
 ///   for top elements.
 exprt write_stackt::to_expression() const
 {
+  // A top stack is useless and its expression should not be evaluated
+  PRECONDITION(!is_top_value());
   exprt access_expr=nil_exprt();
   for(const std::shared_ptr<write_stack_entryt> &entry : stack)
   {

unit/analyses/variable-sensitivity/write_stack.cpp

@@ -64,6 +64,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &x")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -86,6 +87,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &a[0]")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -103,6 +105,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &a")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -120,6 +123,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &a[0]")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -139,6 +143,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &a[1]")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -157,6 +162,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &a[1]")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -176,6 +182,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &a[2]")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -195,6 +202,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &a[0]")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -214,6 +222,7 @@ SCENARIO("Constructing write stacks",
       THEN("The constructed stack should be &a[2]")
       {
         auto stack=write_stackt(in_expr, environment, ns);
+        REQUIRE_FALSE(stack.is_top_value());
         const exprt &out_expr=stack.to_expression();
 
         CAPTURE(expr2c(out_expr, ns));
@@ -239,6 +248,7 @@ SCENARIO("Constructing write stacks",
         THEN("The constructed stack should be &a[TOP]")
         {
           auto stack=write_stackt(in_expr, environment, ns);
+          REQUIRE_FALSE(stack.is_top_value());
           const exprt &out_expr=stack.to_expression();
 
           CAPTURE(expr2c(out_expr, ns));
@@ -265,6 +275,7 @@ SCENARIO("Constructing write stacks",
         THEN("The constructed stack should be &a[2]")
         {
           auto stack=write_stackt(in_expr, environment, ns);
+          REQUIRE_FALSE(stack.is_top_value());
           const exprt &out_expr=stack.to_expression();
 
           CAPTURE(expr2c(out_expr, ns));
@@ -308,6 +319,7 @@ SCENARIO("Constructing write stacks",
         THEN("The constructed stack should be &s.comp")
         {
           auto stack=write_stackt(in_expr, environment, ns);
+          REQUIRE_FALSE(stack.is_top_value());
           const exprt &out_expr=stack.to_expression();
 
           CAPTURE(expr2c(out_expr, ns));
@@ -327,6 +339,7 @@ SCENARIO("Constructing write stacks",
         THEN("The constructed stack should be &s.comp2")
         {
           auto stack=write_stackt(in_expr, environment, ns);
+          REQUIRE_FALSE(stack.is_top_value());
           const exprt &out_expr=stack.to_expression();
 
           CAPTURE(expr2c(out_expr, ns));
@@ -384,6 +397,7 @@ SCENARIO("Constructing write stacks",
         THEN("The constructed stack should be &arr_s[1].comp")
         {
           auto stack=write_stackt(in_expr, environment, ns);
+          REQUIRE_FALSE(stack.is_top_value());
           const exprt &out_expr=stack.to_expression();
 
           CAPTURE(expr2c(out_expr, ns));
@@ -424,6 +438,7 @@ SCENARIO("Constructing write stacks",
           THEN("The constructed stack should be &arr_s[TOP].comp")
           {
             auto stack=write_stackt(in_expr, environment, ns);
+            REQUIRE_FALSE(stack.is_top_value());
             const exprt &out_expr=stack.to_expression();
 
             CAPTURE(expr2c(out_expr, ns));