Merge pull request #903 from diffblue/smv-empty

SMV: error on empty integer range
diffblue · Jan 3, 2025 · f38d738 · f38d738
2 parents 3ce519c + 264181b
commit f38d738
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 2 deletions.
diff --git a/regression/smv/range-type/empty.desc b/regression/smv/range-type/empty.desc
@@ -0,0 +1,7 @@
+CORE
+empty.smv
+
+^file empty\.smv line 4: range is empty$
+^EXIT=2$
+^SIGNAL=0$
+--
diff --git a/regression/smv/range-type/empty.smv b/regression/smv/range-type/empty.smv
@@ -0,0 +1,5 @@
+MODULE main
+
+-- wrong order
+VAR x : 10..1;
+
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
@@ -472,8 +472,14 @@ smv_ranget smv_typecheckt::convert_type(const typet &src)
   }
   else if(src.id()==ID_range)
   {
-    dest.from=string2integer(src.get_string(ID_from));
-    dest.to=string2integer(src.get_string(ID_to));
+    auto from = string2integer(src.get_string(ID_from));
+    auto to = string2integer(src.get_string(ID_to));
+
+    if(from > to)
+      throw errort().with_location(src.source_location()) << "range is empty";
+
+    dest.from = from;
+    dest.to = to;
   }
   else if(src.id()==ID_enumeration)
   {
@@ -1232,6 +1238,10 @@ void smv_typecheckt::convert(smv_parse_treet::mc_varst &vars)
   {
     const smv_parse_treet::mc_vart &var = var_it.second;
 
+    // check the type, if given
+    if(var.type.is_not_nil() && var.type.id() != "submodule")
+      convert_type(var.type);
+
     symbol.base_name = var_it.first;
 
     if(var.identifier=="")