Merge pull request #326 from diffblue/verilog_ift

Verilog: verilog_ift interface

Author: tautschnig

src/verilog/verilog_expr.h

@@ -784,51 +784,73 @@ inline verilog_caset &to_verilog_case(exprt &expr)
 class verilog_ift:public verilog_statementt
 {
 public:
-  verilog_ift():verilog_statementt(ID_if)
+  verilog_ift(exprt __cond, verilog_statementt __then_case)
+    : verilog_statementt(ID_if)
   {
-    operands().resize(3);
+    add_to_operands(std::move(__cond), std::move(__then_case));
   }
 
-  exprt &condition()
+  verilog_ift(
+    exprt __cond,
+    verilog_statementt __then_case,
+    verilog_statementt __else_case)
+    : verilog_statementt(ID_if)
+  {
+    add_to_operands(
+      std::move(__cond), std::move(__then_case), std::move(__else_case));
+  }
+
+  exprt &cond()
   {
     return op0();
   }
 
-  const exprt &condition() const
+  const exprt &cond() const
   {
     return op0();
   }
-  
-  verilog_statementt &true_case()
+
+  verilog_statementt &then_case()
   {
     return static_cast<verilog_statementt &>(op1());
   }
 
-  const verilog_statementt &true_case() const
+  const verilog_statementt &then_case() const
   {
     return static_cast<const verilog_statementt &>(op1());
   }
 
-  verilog_statementt &false_case()
+  bool has_else_case() const
+  {
+    return operands().size() == 3;
+  }
+
+  verilog_statementt &else_case()
   {
     return static_cast<verilog_statementt &>(op2());
   }
 
-  const verilog_statementt &false_case() const
+  const verilog_statementt &else_case() const
   {
     return static_cast<const verilog_statementt &>(op2());
   }
 };
 
 inline const verilog_ift &to_verilog_if(const exprt &expr)
 {
-  assert(expr.id()==ID_if && expr.operands().size()>=2);
+  PRECONDITION(expr.id() == ID_if);
+  DATA_INVARIANT(
+    expr.operands().size() == 2 || expr.operands().size() == 3,
+    "if has two or three operands");
   return static_cast<const verilog_ift &>(expr);
 }
 
 inline verilog_ift &to_verilog_if(exprt &expr)
 {
-  assert(expr.id()==ID_if && expr.operands().size()>=2);
+  PRECONDITION(expr.id() == ID_if);
+  DATA_INVARIANT(
+    expr.operands().size() == 2 || expr.operands().size() == 3,
+    "if has two or three operands");
   return static_cast<verilog_ift &>(expr);
 }
 

src/verilog/verilog_synthesis.cpp

@@ -2067,19 +2067,11 @@ Function: verilog_synthesist::synth_if
 void verilog_synthesist::synth_if(
   const verilog_ift &statement)
 {
-  if(statement.operands().size()!=2 &&
-     statement.operands().size()!=3)
-  {
-    error().source_location=statement.source_location();
-    error() << "if statement expected to have two or three operands" << eom;
-    throw 0;
-  }
-
-  auto if_operand = synth_expr(statement.condition(), symbol_statet::CURRENT);
+  auto if_operand = synth_expr(statement.cond(), symbol_statet::CURRENT);
 
   if(if_operand.is_true())
   {
-    synth_statement(statement.true_case());
+    synth_statement(statement.then_case());
     return;
   }
 
@@ -2091,17 +2083,17 @@ void verilog_synthesist::synth_if(
   true_map.clear_changed();
   false_map.clear_changed();
 
-  // true case
+  // 'then' case
   {
     value_map=&true_map;
-    synth_statement(statement.true_case());
+    synth_statement(statement.then_case());
   }
-  
-  // false case
-  if(statement.operands().size()==3)
+
+  // 'else' case
+  if(statement.has_else_case())
   {
     value_map=&false_map;
-    synth_statement(statement.false_case());
+    synth_statement(statement.else_case());
   }
 
   // restore and merge

src/verilog/verilog_typecheck.cpp

@@ -1245,22 +1245,15 @@ Function: verilog_typecheckt::convert_if
 
 void verilog_typecheckt::convert_if(verilog_ift &statement)
 {
-  if(statement.operands().size()!=2 &&
-     statement.operands().size()!=3)
-  {
-    throw errort().with_location(statement.source_location())
-      << "if statement expected to have two or three operands";
-  }
-
-  exprt &condition=statement.condition();
+  exprt &condition = statement.cond();
 
   convert_expr(condition);
   make_boolean(condition);
 
-  convert_statement(statement.true_case());
+  convert_statement(statement.then_case());
 
-  if(statement.operands().size()==3)
-    convert_statement(statement.false_case());
+  if(statement.has_else_case())
+    convert_statement(statement.else_case());
 }
 
 /*******************************************************************\