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

@@ -780,7 +780,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());
   }
@@ -1000,7 +1000,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,
@@ -1057,7 +1057,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

@@ -26,12 +26,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
@@ -580,6 +580,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

@@ -172,7 +172,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

@@ -31,7 +31,6 @@ void cpp_typecheckt::convert_parameter(
     parameter.set_base_name(base_name);
   }
 
-  PRECONDITION(!cpp_scopes.current_scope().prefix.empty());
   irep_idt identifier=cpp_scopes.current_scope().prefix+
                       id2string(base_name);
 
@@ -42,15 +41,17 @@ void cpp_typecheckt::convert_parameter(
   if(!lookup(identifier, check_symbol))
     return;
 
-  parameter_symbolt symbol;
+  symbolt symbol;
 
   symbol.name=identifier;
   symbol.base_name=parameter.get_base_name();
   symbol.location=parameter.source_location();
   symbol.mode = current_mode;
   symbol.module=module;
   symbol.type=parameter.type();
+  symbol.is_state_var=true;
   symbol.is_lvalue=!is_reference(symbol.type);
+  symbol.is_parameter=true;
 
   INVARIANT(!symbol.base_name.empty(), "parameter has base name");
 
@@ -91,6 +92,22 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   if(symbol.value.is_nil())
     return;
 
+  // if it is a destructor, add the implicit code
+  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
+  {
+    const symbolt &msymb=lookup(symbol.type.get(ID_C_member_name));
+
+    assert(symbol.value.id()==ID_code);
+    assert(symbol.value.get(ID_statement)==ID_block);
+
+    if(
+      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
+      symbol.value.op0().op0().id() != ID_already_typechecked)
+    {
+      symbol.value.copy_to_operands(dtor(msymb).as_expr());
+    }
+  }
+
   // enter appropriate scope
   cpp_save_scopet saved_scope(cpp_scopes);
   cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
@@ -108,29 +125,13 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
     code_typet::parameterst &parameters=function_type.parameters();
     assert(parameters.size()>=1);
     code_typet::parametert &this_parameter_expr=parameters.front();
-    function_scope.this_expr = symbol_exprt{
-      this_parameter_expr.get_identifier(), this_parameter_expr.type()};
+    function_scope.this_expr=exprt(ID_symbol, this_parameter_expr.type());
+    function_scope.this_expr.set(
+      ID_identifier, this_parameter_expr.get_identifier());
   }
   else
     function_scope.this_expr.make_nil();
 
-  // if it is a destructor, add the implicit code
-  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
-  {
-    const symbolt &msymb = lookup(symbol.type.get(ID_C_member_name));
-
-    PRECONDITION(symbol.value.id() == ID_code);
-    PRECONDITION(symbol.value.get(ID_statement) == ID_block);
-
-    if(
-      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
-      symbol.value.op0().op0().id() != ID_already_typechecked)
-    {
-      symbol.value.copy_to_operands(
-        dtor(msymb, to_symbol_expr(function_scope.this_expr)));
-    }
-  }
-
   // do the function body
   start_typecheck_code();
 
@@ -148,8 +149,6 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   symbol.value.type()=symbol.type;
 
   return_type = old_return_type;
-
-  deferred_typechecking.erase(symbol.name);
 }
 
 /// for function overloading
@@ -174,7 +173,8 @@ irep_idt cpp_typecheckt::function_identifier(const typet &type)
   code_typet::parameterst::const_iterator it=
     parameters.begin();
 
-  if(it != parameters.end() && it->get_this())
+  if(it!=parameters.end() &&
+     it->get_identifier()==ID_this)
   {
     const typet &pointer=it->type();
     const typet &symbol =pointer.subtype();

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();
   }
@@ -309,7 +309,7 @@ void cpp_typecheckt::zero_initializer(
     already_typechecked(assign.lhs());
 
     typecheck_code(assign);
-    ops.push_back(assign);
+    ops.push_back(assign.as_expr());
   }
   else
   {
@@ -330,6 +330,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

@@ -461,15 +461,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_code_cpp_new(src, indent);
+    return convert_cpp_new(src.as_expr(), indent);
 
   return expr2ct::convert_code(src, indent);
 }

src/cpp/parse.cpp

@@ -2711,7 +2711,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;
@@ -2724,7 +2724,7 @@ bool Parser::rConstructorDecl(
           return false;
         }
 
-        constructor.value()=codet(ID_default);
+        constructor.value() = exprt(ID_default);
         set_location(constructor.value(), value);
       }
       break;
@@ -2737,7 +2737,7 @@ bool Parser::rConstructorDecl(
           return false;
         }
 
-        constructor.value()=codet(ID_cpp_delete);
+        constructor.value() = exprt(ID_cpp_delete);
         set_location(constructor.value(), value);
       }
       break;
@@ -2902,7 +2902,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
@@ -2914,7 +2914,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
@@ -3412,7 +3412,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;
@@ -7184,7 +7184,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