Merge pull request #988 from diffblue/smv_enum_type

SMV: type check SMV enum literals

Author: kroening

regression/smv/enums/enum3.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 enum3.smv
 
-^EXIT=0$
+^file .* line 7: enum c not a member of \{ a, b \}$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This should be a type error.

src/smvlang/smv_typecheck.cpp

@@ -79,6 +79,8 @@ class smv_typecheckt:public typecheckt
   bool do_spec;
 
   smv_ranget convert_type(const typet &);
+  static bool is_contained_in(irep_idt, const enumeration_typet &);
+
   void convert(smv_parse_treet::modulet::itemt &);
   void typecheck(smv_parse_treet::modulet::itemt &);
   void typecheck_expr_rec(exprt &, const typet &, modet);
@@ -137,6 +139,26 @@ class smv_typecheckt:public typecheckt
 
 /*******************************************************************\
 
+Function: smv_typecheckt::is_contained_in
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_typecheckt::is_contained_in(irep_idt id, const enumeration_typet &type)
+{
+  for(auto &element : type.elements())
+    if(element.id() == id)
+      return true;
+  return false;
+}
+
+/*******************************************************************\
+
 Function: smv_typecheckt::convert_ports
 
   Inputs:
@@ -749,10 +771,11 @@ void smv_typecheckt::typecheck_expr_rec(
   }
   else if(expr.id()==ID_constant)
   {
+    const auto value = to_constant_expr(expr).get_value();
+
     if(expr.type().id()==ID_integer)
     {
-      const std::string &value=expr.get_string(ID_value);
-      mp_integer int_value=string2integer(value);
+      mp_integer int_value = string2integer(id2string(value));
 
       if(dest_type.is_nil())
       {
@@ -796,6 +819,12 @@ void smv_typecheckt::typecheck_expr_rec(
     {
       if(dest_type.id() == ID_enumeration)
       {
+        if(!is_contained_in(value, to_enumeration_type(dest_type)))
+        {
+          throw errort().with_location(expr.find_source_location())
+            << "enum " << value << " not a member of " << to_string(dest_type);
+        }
+
         if(to_enumeration_type(expr.type()).elements().empty())
           expr.type() = dest_type;
       }