Verilog: fix integral vs. bit vector terminology

This changes the naming of methods and error messages.  The term 'integral'
includes non-integer types, e.g., time variables.  Many operators require
operands that are integral but exclude time variables.  The standard calls
these "bit vector types".

Author: kroening

regression/verilog/expressions/concatenation5.desc

@@ -1,7 +1,7 @@
 CORE
 concatenation5.v
 
-^file .* line 4: operand 1.1 must be integral$
+^file .* line 4: operand 1.1 must have a bit vector type$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/verilog/expressions/mod2.desc

@@ -1,7 +1,7 @@
 CORE
 mod2.v
 
-^file .* line 4: operand 1\.1 must be integral$
+^file .* line 4: operand 1\.1 must have a bit vector type$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/verilog/expressions/reduction2.desc

@@ -1,7 +1,7 @@
 CORE
 reduction2.v
 
-^file .* line 4: operand 1\.1 must be integral$
+^file .* line 4: operand 1\.1 must have a bit vector type$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/verilog/expressions/replication3.desc

@@ -1,7 +1,7 @@
 CORE
 replication3.v
 
-^file .* line 3: operand 1\.1 must be integral$
+^file .* line 3: operand 1\.1 must have a bit vector type$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/verilog/expressions/shr2.desc

@@ -1,7 +1,7 @@
 CORE
 shr2.v
 
-^file .* line 4: operand 1\.1 must be integral$
+^file .* line 4: operand 1\.1 must have a bit vector type$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/verilog/expressions/streaming_concatenation2.desc

@@ -1,7 +1,7 @@
 CORE
 streaming_concatenation2.sv
 
-^file .* line 4: operand 1\.1 must be integral$
+^file .* line 4: operand 1\.1 must have a bit vector type$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/verilog/expressions/wildcard_equality2.desc

@@ -1,7 +1,7 @@
 CORE
 wildcard_equality2.v
 
-^file .* line 4: operand 1\.1 must be integral$
+^file .* line 4: operand 1\.1 must have a bit vector type$
 ^EXIT=2$
 ^SIGNAL=0$
 --

src/verilog/verilog_typecheck_expr.cpp

@@ -426,7 +426,7 @@ void verilog_typecheck_exprt::no_bool_ops(exprt &expr)
 
 /*******************************************************************\
 
-Function: verilog_typecheck_exprt::must_be_integral
+Function: verilog_typecheck_exprt::must_be_bit_vector
 
   Inputs:
 
@@ -436,9 +436,9 @@ Function: verilog_typecheck_exprt::must_be_integral
 
 \*******************************************************************/
 
-void verilog_typecheck_exprt::must_be_integral(const exprt &expr)
+void verilog_typecheck_exprt::must_be_bit_vector(exprt &expr)
 {
-  // Throw an error if the given expression doesn't have an integral type.
+  // Throw an error if the given expression doesn't have a bitvector type.
   const auto &type = expr.type();
   if(type.id() == ID_bool)
   {
@@ -452,7 +452,7 @@ void verilog_typecheck_exprt::must_be_integral(const exprt &expr)
   }
   else
     throw errort().with_location(expr.source_location())
-      << "operand " << to_string(expr) << " must be integral";
+      << "operand " << to_string(expr) << " must have a bit vector type";
 }
 
 /*******************************************************************\
@@ -490,7 +490,7 @@ exprt verilog_typecheck_exprt::convert_expr_concatenation(
         << "unsized literals are not allowed in concatenations";
     }
 
-    must_be_integral(*it);
+    must_be_bit_vector(*it);
 
     const typet &type = it->type();
 
@@ -1563,7 +1563,7 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
 
   const std::string &value = id2string(expr.get_value());
 
-  // real or integral?
+  // real or integer?
   if(
     value.find('.') != std::string::npos ||
     (value.find('h') == std::string::npos &&
@@ -2558,10 +2558,11 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
   {
     // these may produce an 'x' if the operand is a verilog_bv
     convert_expr(expr.op());
-    must_be_integral(expr.op());
+    must_be_bit_vector(expr.op());
 
-    if (expr.op().type().id() == ID_verilog_signedbv ||
-        expr.op().type().id() == ID_verilog_unsignedbv)
+    if(
+      expr.op().type().id() == ID_verilog_signedbv ||
+      expr.op().type().id() == ID_verilog_unsignedbv)
     {
       expr.type()=verilog_unsignedbv_typet(1);
     }
@@ -2668,7 +2669,7 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     // slice_size is defaulted to 1
     PRECONDITION(expr.op().operands().size() == 1);
     convert_expr(expr.op().operands()[0]);
-    must_be_integral(expr.op().operands()[0]);
+    must_be_bit_vector(expr.op().operands()[0]);
     expr.type() = expr.op().operands()[0].type();
     return std::move(expr);
   }
@@ -2839,7 +2840,7 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr)
   exprt &op1=expr.op1();
 
   convert_expr(op1);
-  must_be_integral(op1);
+  must_be_bit_vector(op1);
 
   if(op1.type().id()==ID_bool)
     op1 = typecast_exprt{op1, unsignedbv_typet{1}};
@@ -3085,9 +3086,9 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     convert_relation(expr);
 
-    // integral operands only
-    must_be_integral(expr.lhs());
-    must_be_integral(expr.rhs());
+    // bit vector operands only
+    must_be_bit_vector(expr.lhs());
+    must_be_bit_vector(expr.rhs());
 
     return std::move(expr);
   }
@@ -3120,8 +3121,8 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     convert_expr(expr.lhs());
     convert_expr(expr.rhs());
-    must_be_integral(expr.lhs());
-    must_be_integral(expr.rhs());
+    must_be_bit_vector(expr.lhs());
+    must_be_bit_vector(expr.rhs());
     no_bool_ops(expr);
 
     const typet &lhs_type = expr.lhs().type();
@@ -3157,9 +3158,8 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     // logical right shift >>
     convert_expr(expr.lhs());
     convert_expr(expr.rhs());
-    must_be_integral(expr.lhs());
-    must_be_integral(expr.rhs());
-    no_bool_ops(expr);
+    must_be_bit_vector(expr.lhs());
+    must_be_bit_vector(expr.rhs());
 
     const typet &lhs_type = expr.lhs().type();
     const typet &rhs_type = expr.rhs().type();
@@ -3191,12 +3191,13 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
   {
     convert_expr(expr.lhs());
     convert_expr(expr.rhs());
-    must_be_integral(expr.lhs());
-    must_be_integral(expr.rhs());
 
     tc_binary_expr(expr);
     no_bool_ops(expr);
 
+    must_be_bit_vector(expr.lhs());
+    must_be_bit_vector(expr.rhs());
+
     expr.type() = expr.lhs().type();
 
     return std::move(expr);

src/verilog/verilog_typecheck_expr.h

@@ -196,7 +196,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   void tc_binary_expr(const exprt &expr, exprt &op0, exprt &op1);
   void convert_relation(binary_exprt &);
   void no_bool_ops(exprt &);
-  void must_be_integral(const exprt &);
+  void must_be_bit_vector(exprt &);
 
   // SVA
   void convert_sva(exprt &expr)