Merge pull request #1474 from diffblue/smv-divmod-int

SMV: error mod and div on integers

Author: tautschnig

regression/smv/expressions/div1.desc

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 div1.smv
 
-^EXIT=0$
+^file .* line 4: no support for / on integer operands$
+^EXIT=2$
 ^SIGNAL=0$
 --
 --
-div is not implemented.

regression/smv/expressions/mod1.desc

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 mod1.smv
 
-^EXIT=0$
+^file .* line 4: no support for % on integer operands$
+^EXIT=2$
 ^SIGNAL=0$
 --
 --
-mod is not implemented.

src/smvlang/smv_typecheck.cpp

@@ -806,9 +806,15 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
       else if(expr.id() == ID_mult)
         new_range = smv_range0 * smv_range1;
       else if(expr.id() == ID_div)
-        new_range = smv_range0;
+      {
+        throw errort().with_location(expr.source_location())
+          << "no support for / on integer operands";
+      }
       else if(expr.id() == ID_mod)
-        new_range = smv_range1;
+      {
+        throw errort().with_location(expr.source_location())
+          << "no support for % on integer operands";
+      }
       else
         assert(false);