Replace 3-valued char by enum

Author: tautschnig

src/goto-programs/interpreter.cpp

@@ -503,7 +503,9 @@ exprt interpretert::get_value(
     }
     return result;
   }
-  if(use_non_det && (memory[offset].initialized>=0))
+  if(use_non_det &&
+     memory[offset].initialized!=
+     memory_cellt::initializedt::WRITTEN_BEFORE_READ)
     return side_effect_expr_nondett(type);
   mp_vectort rhs;
   rhs.push_back(memory[offset].value);
@@ -681,7 +683,8 @@ void interpretert::execute_assign()
       size_t size=get_size(code_assign.lhs().type());
       for(size_t i=0; i<size; i++)
       {
-        memory[address+i].initialized=-1;
+        memory[address+i].initialized=
+          memory_cellt::initializedt::READ_BEFORE_WRITTEN;
       }
     }
   }
@@ -706,8 +709,8 @@ void interpretert::assign(
                  << "\n" << eom;
       }
       cell.value=rhs[i];
-      if(cell.initialized==0)
-        cell.initialized=1;
+      if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
+        cell.initialized=memory_cellt::initializedt::WRITTEN_BEFORE_READ;
     }
   }
 }

src/goto-programs/interpreter_class.h

@@ -161,12 +161,18 @@ class interpretert:public messaget
   public:
     memory_cellt() :
     value(0),
-    initialized(0)
+    initialized(initializedt::UNKNOWN)
     {}
     mp_integer value;
     // Initialized is annotated even during reads
+    enum class initializedt
+    {
+      UNKNOWN,
+      WRITTEN_BEFORE_READ,
+      READ_BEFORE_WRITTEN
+    };
     // Set to 1 when written-before-read, -1 when read-before-written
-    mutable char initialized;
+    mutable initializedt initialized;
   };
 
   typedef sparse_vectort<memory_cellt> memoryt;

src/goto-programs/interpreter_evaluate.cpp

@@ -36,8 +36,8 @@ void interpretert::read(
     {
       const memory_cellt &cell=memory[integer2size_t(address+i)];
       value=cell.value;
-      if(cell.initialized==0)
-        cell.initialized=-1;
+      if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
+        cell.initialized=memory_cellt::initializedt::READ_BEFORE_WRITTEN;
     }
     else
       value=0;
@@ -64,8 +64,8 @@ void interpretert::read_unbounded(
     {
       const memory_cellt &cell=memory[integer2size_t(address+i)];
       value=cell.value;
-      if(cell.initialized==0)
-        cell.initialized=-1;
+      if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
+        cell.initialized=memory_cellt::initializedt::READ_BEFORE_WRITTEN;
     }
     else
       value=0;
@@ -86,7 +86,7 @@ void interpretert::allocate(
     {
       memory_cellt &cell=memory[integer2size_t(address+i)];
       cell.value=0;
-      cell.initialized=0;
+      cell.initialized=memory_cellt::initializedt::UNKNOWN;
     }
   }
 }
@@ -96,8 +96,9 @@ void interpretert::clear_input_flags()
 {
   for(auto &cell : memory)
   {
-    if(cell.second.initialized>0)
-      cell.second.initialized=0;
+    if(cell.second.initialized==
+       memory_cellt::initializedt::WRITTEN_BEFORE_READ)
+      cell.second.initialized=memory_cellt::initializedt::UNKNOWN;
   }
 }