codet now inherits from irept

Author: Daniel Kroening

src/ansi-c/c_typecheck_code.cpp

@@ -32,8 +32,6 @@ void c_typecheck_baset::typecheck_code(codet &code)
     throw 0;
   }
 
-  code.type() = empty_typet();
-
   const irep_idt &statement=code.get_statement();
 
   if(statement==ID_expression)

src/ansi-c/c_typecheck_expr.cpp

@@ -773,7 +773,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
     code_declt decl(symbol.symbol_expr());
     decl.add_source_location()=declaration.source_location();
 
-    expr.op0()=decl;
+    expr.get_sub()[0] = decl;
 
     typecheck_expr(expr.op1());
   }
@@ -991,7 +991,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
       ID_statement_expression, void_type(), expr.source_location());
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
-    side_effect_expr.copy_to_operands(decl_block);
+    side_effect_expr.get_sub().push_back(decl_block);
     clean_code.clear();
 
     // We merge the side-effect into the operand of the typecast,
@@ -1048,7 +1048,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
       ID_statement_expression, void_type(), expr.source_location());
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
-    side_effect_expr.copy_to_operands(decl_block);
+    side_effect_expr.get_sub().push_back(decl_block);
     clean_code.clear();
 
     // We merge the side-effect into the operand of the typecast,

src/cpp/cpp_destructor.cpp

@@ -64,7 +64,7 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
 
       auto i_code = cpp_destructor(source_location, index);
       if(i_code.has_value())
-        new_code.add_to_operands(std::move(i_code.value()));
+        new_code.add(std::move(i_code.value()));
     }
 
     return std::move(new_code);

src/cpp/cpp_typecheck_code.cpp

@@ -25,12 +25,10 @@ void cpp_typecheckt::typecheck_code(codet &code)
 
   if(statement==ID_try_catch)
   {
-    code.type() = empty_typet();
     typecheck_try_catch(code);
   }
   else if(statement==ID_member_initializer)
   {
-    code.type() = empty_typet();
     typecheck_member_initializer(code);
   }
   else if(statement==ID_msc_if_exists ||

src/cpp/cpp_typecheck_compound_type.cpp

@@ -671,14 +671,16 @@ void cpp_typecheckt::typecheck_compound_declarator(
           exprt already_typechecked(ID_already_typechecked);
           already_typechecked.add_to_operands(std::move(expr_call));
 
-          func_symb.value = code_returnt(already_typechecked).make_block();
+          func_symb.value =
+            code_returnt(already_typechecked).make_block().as_expr();
         }
         else
         {
           exprt already_typechecked(ID_already_typechecked);
           already_typechecked.add_to_operands(std::move(expr_call));
 
-          func_symb.value = code_expressiont(already_typechecked).make_block();
+          func_symb.value =
+            code_expressiont(already_typechecked).make_block().as_expr();
         }
 
         // add this new function to the list of components

src/cpp/cpp_typecheck_constructor.cpp

@@ -47,7 +47,7 @@ static void copy_parent(
   code_assignt code(dereference_exprt(op0), op1);
   code.add_source_location() = source_location;
 
-  block.operands().push_back(code);
+  block.operands().push_back(code.as_expr());
 }
 
 /// Generate code to copy the member.
@@ -76,7 +76,7 @@ static void copy_member(
   code_expressiont code(assign);
   code.add_source_location() = source_location;
 
-  block.operands().push_back(code);
+  block.operands().push_back(code.as_expr());
 }
 
 /// Generate code to copy the member.
@@ -113,7 +113,7 @@ static void copy_array(
   code_expressiont code(assign);
   code.add_source_location() = source_location;
 
-  block.operands().push_back(code);
+  block.operands().push_back(code.as_expr());
 }
 
 /// Generate code for implicit default constructors
@@ -579,6 +579,7 @@ void cpp_typecheckt::full_member_initialization(
 
       code_ifthenelset cond(
         cpp_namet("@most_derived").as_expr(), std::move(block));
+
       final_initializers.move_to_sub(cond);
     }
 

src/cpp/cpp_typecheck_declaration.cpp

@@ -173,7 +173,7 @@ void cpp_typecheckt::convert_non_template_declaration(
         declarator.init_args().operands());
 
       if(constructor.has_value())
-        symbol.value = constructor.value();
+        symbol.value = constructor.value().as_expr();
       else
         symbol.value = nil_exprt();
     }

src/cpp/cpp_typecheck_function.cpp

@@ -104,7 +104,7 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
       !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
       symbol.value.op0().op0().id() != ID_already_typechecked)
     {
-      symbol.value.copy_to_operands(dtor(msymb));
+      symbol.value.copy_to_operands(dtor(msymb).as_expr());
     }
   }
 

src/cpp/cpp_typecheck_initializer.cpp

@@ -180,7 +180,7 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol)
       cpp_constructor(symbol.value.source_location(), expr_symbol, ops);
 
     if(constructor.has_value())
-      symbol.value = constructor.value();
+      symbol.value = constructor.value().as_expr();
     else
       symbol.value = nil_exprt();
   }
@@ -308,7 +308,7 @@ void cpp_typecheckt::zero_initializer(
     already_typechecked(assign.lhs());
 
     typecheck_code(assign);
-    ops.push_back(assign);
+    ops.push_back(assign.as_expr());
   }
   else
   {
@@ -329,6 +329,6 @@ void cpp_typecheckt::zero_initializer(
     already_typechecked(assign.lhs());
 
     typecheck_code(assign);
-    ops.push_back(assign);
+    ops.push_back(assign.as_expr());
   }
 }

src/cpp/expr2cpp.cpp

@@ -398,15 +398,15 @@ std::string expr2cppt::convert_code(
   const codet &src,
   unsigned indent)
 {
-  const irep_idt &statement=src.get(ID_statement);
+  const irep_idt &statement = src.get_statement();
 
   if(statement==ID_cpp_delete ||
      statement==ID_cpp_delete_array)
-    return convert_code_cpp_delete(src, indent);
+    return convert_code_cpp_delete(src.as_expr(), indent);
 
   if(statement==ID_cpp_new ||
      statement==ID_cpp_new_array)
-    return convert_cpp_new(src, indent);
+    return convert_cpp_new(src.as_expr(), indent);
 
   return expr2ct::convert_code(src, indent);
 }

src/cpp/parse.cpp

@@ -2714,7 +2714,7 @@ bool Parser::rConstructorDecl(
     {
     case TOK_INTEGER:
       {
-        constructor.value()=codet("cpp-pure-virtual");
+        constructor.value() = exprt("cpp-pure-virtual");
         set_location(constructor.value(), value);
       }
       break;
@@ -2727,7 +2727,7 @@ bool Parser::rConstructorDecl(
           return false;
         }
 
-        constructor.value()=codet(ID_default);
+        constructor.value() = exprt(ID_default);
         set_location(constructor.value(), value);
       }
       break;
@@ -2740,7 +2740,7 @@ bool Parser::rConstructorDecl(
           return false;
         }
 
-        constructor.value()=codet(ID_cpp_delete);
+        constructor.value() = exprt(ID_cpp_delete);
         set_location(constructor.value(), value);
       }
       break;
@@ -2905,7 +2905,7 @@ bool Parser::rDeclaratorWithInit(
         }
 
         lex.get_token(tk);
-        declarator.value()=codet(ID_default);
+        declarator.value() = exprt(ID_default);
         set_location(declarator.value(), tk);
       }
       else if(lex.LookAhead(0)==TOK_DELETE) // C++0x
@@ -2917,7 +2917,7 @@ bool Parser::rDeclaratorWithInit(
         }
 
         lex.get_token(tk);
-        declarator.value()=codet(ID_cpp_delete);
+        declarator.value() = exprt(ID_cpp_delete);
         set_location(declarator.value(), tk);
       }
       else
@@ -3415,7 +3415,7 @@ bool Parser::rMemberInit(exprt &init)
   std::cout << std::string(__indent, ' ') << "Parser::rMemberInit 2\n";
 #endif
 
-  init=codet(ID_member_initializer);
+  init = exprt(ID_member_initializer);
   init.add(ID_member).swap(name);
 
   cpp_tokent tk1, tk2;
@@ -7187,7 +7187,7 @@ bool Parser::rFunctionBody(cpp_declaratort &declarator)
     if(lex.get_token(cb)!='}')
       return false;
 
-    declarator.value()=body;
+    declarator.value() = body.as_expr();
     return true;
   }
   else

src/goto-symex/goto_symex.h

@@ -203,6 +203,7 @@ class goto_symext
   // c) clean up byte_extract on the lhs of an assignment
   void clean_expr(
     exprt &, statet &, bool write);
+  void clean_expr(codet &, statet &, bool write);
 
   void trigger_auto_object(const exprt &, statet &);
   void initialize_auto_object(const exprt &, statet &);
@@ -383,7 +384,7 @@ class goto_symext
     statet &, const exprt &lhs, const side_effect_exprt &);
   virtual void symex_fkt(statet &, const code_function_callt &);
   virtual void symex_trace(statet &, const code_function_callt &);
-  virtual void symex_printf(statet &, const exprt &rhs);
+  virtual void symex_printf(statet &, const irept &);
   virtual void symex_input(statet &, const codet &);
   virtual void symex_output(statet &, const codet &);
 

src/goto-symex/symex_builtin_functions.cpp

@@ -303,12 +303,11 @@ irep_idt get_string_argument(const exprt &src, const namespacet &ns)
   return get_string_argument_rec(tmp);
 }
 
-void goto_symext::symex_printf(
-  statet &state,
-  const exprt &rhs)
+void goto_symext::symex_printf(statet &state, const irept &rhs)
 {
-  PRECONDITION(!rhs.operands().empty());
+  //PRECONDITION(!rhs.operands().empty());
 
+#if 0
   exprt tmp_rhs=rhs;
   state.rename(tmp_rhs, ns);
   do_simplify(tmp_rhs);
@@ -326,6 +325,7 @@ void goto_symext::symex_printf(
     target.output_fmt(
       state.guard.as_expr(),
       state.source, "printf", format_string, args);
+#endif
 }
 
 void goto_symext::symex_input(

src/jsil/jsil_entry_point.cpp

@@ -38,7 +38,7 @@ static void create_initialize(symbol_tablet &symbol_table)
   code_assignt a(rounding_mode, from_integer(0, rounding_mode.type()));
   init_code.add(a);
 
-  initialize.value=init_code;
+  initialize.value = init_code.as_expr();
 
   if(symbol_table.add(initialize))
     throw "failed to add " INITIALIZE_FUNCTION;

src/jsil/parser.y

@@ -210,7 +210,7 @@ statements: statement
 
 statement: TOK_NEWLINE
          {
-           newstack($$)=code_skipt();
+           newstack($$)=code_skipt().as_expr();
          }
          | instruction TOK_NEWLINE
          {
@@ -241,7 +241,7 @@ instruction: TOK_LABEL TOK_IDENTIFIER
            }
            | TOK_SKIP
            {
-             newstack($$)=code_skipt();
+             newstack($$)=code_skipt().as_expr();
            }
            | TOK_IDENTIFIER TOK_DEFEQ rhs
            {

src/linking/static_lifetime_init.cpp

@@ -109,10 +109,8 @@ void static_lifetime_init(
 
   symbolt &init_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
 
-  init_symbol.value=code_blockt();
-  init_symbol.value.add_source_location()=source_location;
-
-  code_blockt &dest=to_code_block(to_code(init_symbol.value));
+  code_blockt dest;
+  dest.add_source_location() = source_location;
 
   // add the magic label to hide
   dest.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
@@ -164,4 +162,6 @@ void static_lifetime_init(
       dest.add(function_call);
     }
   }
+
+  init_symbol.value = dest.as_expr();
 }