Merge pull request #1176 from diffblue/smv-typechecking

SMV: tighten expression type checking

Author: tautschnig

regression/smv/range-type/range_type9.desc

@@ -0,0 +1,8 @@
+CORE
+range_type9.smv
+
+^file .* line 5: Expected expression of type `1..6', but got expression `7', which is of type `7..7'$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/smv/range-type/range_type9.smv

@@ -0,0 +1,5 @@
+MODULE main
+VAR x: 1..6;
+
+-- out of range
+ASSIGN x := 7;

src/smvlang/smv_typecheck.cpp

@@ -1297,31 +1297,40 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type)
     }
     else if(type.id() == ID_range)
     {
-      if(expr.id() == ID_constant && expr.type().id() == ID_range)
-      {
-        // re-type the constant
-        auto value = numeric_cast_v<mp_integer>(to_constant_expr(expr));
-        expr = from_integer(value, type);
-        return;
-      }
-      else if(expr.id() == ID_cond && expr.type().id() == ID_range)
+      if(expr.type().id() == ID_range)
       {
-        // re-type the cond
-        bool condition = true;
-
-        for(auto &op : expr.operands())
+        // range to range
+        if(expr.id() == ID_constant)
         {
-          if(!condition)
-            convert_expr_to(op, type);
+          // re-type the constant
+          auto value = numeric_cast_v<mp_integer>(to_constant_expr(expr));
+          if(to_range_type(type).includes(value))
+          {
+            expr = from_integer(value, type);
+            return;
+          }
+        }
+        else if(expr.id() == ID_cond)
+        {
+          // re-type the cond
+          bool condition = true;
+
+          for(auto &op : expr.operands())
+          {
+            if(!condition)
+              convert_expr_to(op, type);
 
-          condition = !condition;
+            condition = !condition;
+          }
+          expr.type() = type;
+          return;
+        }
+        else
+        {
+          expr = typecast_exprt{expr, type};
+          return;
         }
-        expr.type() = type;
-        return;
       }
-
-      expr = typecast_exprt{expr, type};
-      return;
     }
     else if(type.id() == ID_bool)
     {