Modification to use enumeration literal position as its value.

Using an enumeration literal position as its value maintains an
order relation between literals of an enumeration, whereas using
an enumeration literal's representation value does not necessarily.
Also updated range checks on enumeration literals.

Author: tjj2017

gnat2goto/driver/range_check.adb

@@ -76,7 +76,8 @@ package body Range_Check is
       case Kind (Bound_Type) is
          when I_Bounded_Signedbv_Type
             | I_Bounded_Unsignedbv_Type
-            | I_Bounded_Floatbv_Type =>
+            | I_Bounded_Floatbv_Type
+            | I_C_Enum_Type =>
             return Get_Bound_Of_Bounded_Type (Bound_Type, Pos);
          when I_Unsignedbv_Type =>
             --  this case is probably unnecessary:
@@ -450,14 +451,18 @@ package body Range_Check is
                                     Bounds_Type : Irep)
                                     return Irep
    is
-      Followed_Bound_Type : constant Irep := Follow_Symbol_Type (Bounds_Type,
-                                                         Global_Symbol_Table);
-
+      Followed_Bound_Type : constant Irep :=
+        Follow_Symbol_Type (Bounds_Type,
+                            Global_Symbol_Table);
+      Lower_Bound : constant Irep :=
+        Get_Bound (N, Followed_Bound_Type, Bound_Low);
+      Upper_Bound : constant Irep :=
+        Get_Bound (N, Followed_Bound_Type, Bound_High);
    begin
       return Make_Range_Assert_Expr (N           => N,
                  Value       => Value,
-                 Lower_Bound => Get_Bound (N, Followed_Bound_Type, Bound_Low),
-                 Upper_Bound => Get_Bound (N, Followed_Bound_Type, Bound_High),
+                 Lower_Bound => Lower_Bound,
+                 Upper_Bound => Upper_Bound,
                  Expected_Return_Type => Get_Type (Value),
                  Check_Name  => "__CPROVER_Ada_Range_Check");
 
@@ -472,11 +477,36 @@ package body Range_Check is
                                    Upper_Bound : Irep)
                                    return Irep
    is
-      Bound_Type : constant Irep :=
+      --  The bounds and or the value may be enumeration types.
+      --  If so, they are converted to a bitvector type.
+      --  When the enumeration is declared each literal s given the
+      --  value of its position (starting from 0).
+      Bound_Type_Raw      : constant Irep :=
         Follow_Symbol_Type (Get_Type (Lower_Bound), Global_Symbol_Table);
-      Value_Expr_Type : constant Irep :=
+      Value_Expr_Type_Raw : constant Irep :=
         Follow_Symbol_Type (Get_Type (Value_Expr), Global_Symbol_Table);
 
+      Bound_Type : constant Irep :=
+        (if Kind (Bound_Type_Raw) = I_C_Enum_Type then
+              Int32_T
+         else
+            Bound_Type_Raw);
+
+      Value_Expr_Type : constant Irep :=
+        (if Kind (Value_Expr_Type_Raw) = I_C_Enum_Type then
+              Int32_T
+         else
+            Value_Expr_Type_Raw);
+
+      Resolved_Value_Expr : constant Irep :=
+        (if Kind (Value_Expr_Type_Raw) = I_C_Enum_Type then
+              Typecast_If_Necessary
+           (Expr           => Value_Expr,
+            New_Type       => Int32_T,
+            A_Symbol_Table => Global_Symbol_Table)
+         else
+            Value_Expr);
+
       type Adjusted_Value_And_Bounds_T is
         record
            Value_Expr : Irep;
@@ -494,17 +524,17 @@ package body Range_Check is
       begin
          if Greater_Width then
             return (
-             Value_Expr => Typecast_If_Necessary
-               (Value_Expr, Bound_Type, Global_Symbol_Table),
-             Upper_Bound => Upper_Bound,
-             Lower_Bound => Lower_Bound);
+                    Value_Expr => Typecast_If_Necessary
+                      (Resolved_Value_Expr, Bound_Type, Global_Symbol_Table),
+                    Upper_Bound => Upper_Bound,
+                    Lower_Bound => Lower_Bound);
          else
             return (
-             Value_Expr => Value_Expr,
-             Upper_Bound => Typecast_If_Necessary
-               (Upper_Bound, Value_Expr_Type, Global_Symbol_Table),
-             Lower_Bound => Typecast_If_Necessary
-               (Lower_Bound, Value_Expr_Type, Global_Symbol_Table));
+                    Value_Expr => Resolved_Value_Expr,
+                    Upper_Bound => Typecast_If_Necessary
+                      (Upper_Bound, Value_Expr_Type, Global_Symbol_Table),
+                    Lower_Bound => Typecast_If_Necessary
+                      (Lower_Bound, Value_Expr_Type, Global_Symbol_Table));
          end if;
       end Get_Adjusted_Value_And_Bounds;
 

gnat2goto/driver/tree_walk.adb

@@ -963,7 +963,7 @@ package body Tree_Walk is
         Intern (Unique_Name (Unique_Defining_Entity (U)));
       Unit_Symbol : Symbol;
    begin
-      --  Insert all all specifications of all withed units including the
+      --  Insert specifications of all withed units including the
       --  specification of the given compilation unit into the symbol table.
       Do_Withed_Units_Specs;
 
@@ -1209,12 +1209,14 @@ package body Tree_Walk is
       Enum_Body : constant Irep := Make_C_Enum_Members;
       Enum_Type_Symbol : constant Irep := Make_Symbol_Type
         (Identifier => Unique_Name (Defining_Identifier (Parent (N))));
-      Member : Node_Id := First (Literals (N));
+      First_Member : constant Node_Id := First (Literals (N));
+      Member : Node_Id := First_Member;
+      Last_Member : Node_Id := First_Member;
    begin
       loop
          declare
             Val_String : constant String :=
-              UI_Image (Enumeration_Rep (Member));
+              UI_Image (Enumeration_Pos (Member));
             Val_Name : constant String := Unique_Name (Member);
             Base_Name : constant String := Get_Name_String (Chars (Member));
             Member_Size : constant Int := UI_To_Int (Esize (Etype (Member)));
@@ -1225,7 +1227,7 @@ package body Tree_Walk is
             Member_Symbol_Init : constant Irep := Make_Constant_Expr
               (I_Type => Make_Signedbv_Type (Integer (Member_Size)),
                Value => Convert_Uint_To_Hex
-                 (Enumeration_Rep (Member), Member_Size),
+                 (Enumeration_Pos (Member), Member_Size),
                Source_Location => Get_Source_Location (Member));
             Typecast_Expr : constant Irep := Make_Op_Typecast
               (Op0 => Member_Symbol_Init,
@@ -1239,11 +1241,19 @@ package body Tree_Walk is
                                      Value_Expr     => Typecast_Expr,
                                      A_Symbol_Table => Global_Symbol_Table);
          end;
+         Last_Member := Member;
          Next (Member);
          exit when not Present (Member);
       end loop;
+
       return Make_C_Enum_Type
-        (I_Subtype => Make_Signedbv_Type (32), -- FIXME why 32?
+        (I_Subtype =>
+           Make_Bounded_Signedbv_Type
+             (Width       => 32, -- FIXME why 32?
+              Lower_Bound => Store_Symbol_Bound
+                (Bound_Type_Symbol (Do_Defining_Identifier (First_Member))),
+              Upper_Bound => Store_Symbol_Bound
+                (Bound_Type_Symbol (Do_Defining_Identifier (Last_Member)))),
          I_Body => Enum_Body);
    end Do_Enumeration_Definition;
 
@@ -4266,7 +4276,7 @@ package body Tree_Walk is
          Set_Bound_Value (Upper_Bound, Upper_Bound_Value, Ok);
          if not Ok then
             return Report_Unhandled_Node_Type
-              (Lower_Bound,
+              (Upper_Bound,
                "Do_Range_Constraint",
                "unsupported upper range kind");
          end if;