Merge pull request #2717 from tautschnig/compiled

Move magic "compiled" string behind an API in symbolt

Author: tautschnig

src/goto-cc/compile.cpp

@@ -724,15 +724,13 @@ void compilet::convert_symbols(goto_functionst &dest)
         symbol_table.symbols.find(*it);
       assert(s_it!=symbol_table.symbols.end());
 
-      if(s_it->second.type.id()==ID_code &&
-         !s_it->second.is_macro &&
-         !s_it->second.is_type &&
-          s_it->second.value.id()!="compiled" &&
-          s_it->second.value.is_not_nil())
+      if(
+        s_it->second.is_function() && !s_it->second.is_compiled() &&
+        s_it->second.value.is_not_nil())
       {
         debug() << "Compiling " << s_it->first << eom;
         converter.convert_function(s_it->first, dest.function_map[s_it->first]);
-        symbol_table.get_writeable_ref(*it).value=exprt("compiled");
+        symbol_table.get_writeable_ref(*it).set_compiled();
       }
     }
   }

src/goto-programs/goto_convert_functions.cpp

@@ -152,7 +152,7 @@ void goto_convert_functionst::convert_function(
   f.type=to_code_type(symbol.type);
 
   if(symbol.value.is_nil() ||
-     symbol.value.id()=="compiled") /* goto_inline may have removed the body */
+     symbol.is_compiled()) /* goto_inline may have removed the body */
     return;
 
   if(symbol.value.id()!=ID_code)

src/util/irep_ids.def

@@ -699,6 +699,7 @@ IREP_ID_ONE(w_ok)
 IREP_ID_ONE(super_class)
 IREP_ID_ONE(exceptions_thrown_list)
 IREP_ID_TWO(C_java_method_type, #java_method_type)
+IREP_ID_ONE(compiled)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/symbol.h

@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iosfwd>
 
 #include "expr.h"
+#include "invariant.h"
 
 /*! \brief Symbol table entry.
     \ingroup gr_symbol_table
@@ -107,6 +108,21 @@ class symbolt
   {
     return !is_type && !is_macro && type.id()==ID_code;
   }
+
+  /// Returns true iff the the symbol's value has been compiled to a goto
+  /// program.
+  bool is_compiled() const
+  {
+    return type.id() == ID_code && value == exprt(ID_compiled);
+  }
+
+  /// Set the symbol's value to "compiled"; to be used once the code-typed value
+  /// has been converted to a goto program.
+  void set_compiled()
+  {
+    PRECONDITION(type.id() == ID_code);
+    value = exprt(ID_compiled);
+  }
 };
 
 std::ostream &operator<<(std::ostream &out, const symbolt &symbol);