Fix UKNI range issue, and add symbols earlier to the symbol table

Author: NlightNFotis

gnat2goto/driver/tree_walk.adb

@@ -743,7 +743,9 @@ package body Tree_Walk is
 
       Result_Type : constant Irep := New_Irep (I_Bounded_Signedbv_Type);
    begin
-      if not (Kind (Resolved_Underlying) in Class_Bitvector_Type) then
+      if not (Kind (Resolved_Underlying) in Class_Bitvector_Type or
+              Kind (Resolved_Underlying) = I_C_Enum_Type)
+      then
          return Report_Unhandled_Node_Type (Range_Expr,
                                             "Do_Base_Range_Constraint",
                                         "range expression not bitvector type");
@@ -754,6 +756,9 @@ package body Tree_Walk is
               Store_Nat_Bound (Bound_Type_Nat (Intval (Lower_Bound)));
          when N_Attribute_Reference => Lower_Bound_Value :=
               Store_Symbol_Bound (Get_Array_Attr_Bound_Symbol (Lower_Bound));
+         when N_Identifier =>
+            Lower_Bound_Value :=
+               Store_Symbol_Bound (Bound_Type_Symbol (Lower_Bound));
          when others =>
             Report_Unhandled_Node_Empty (Lower_Bound,
                                          "Do_Base_Range_Constraint",
@@ -765,13 +770,21 @@ package body Tree_Walk is
               Store_Nat_Bound (Bound_Type_Nat (Intval (Upper_Bound)));
          when N_Attribute_Reference => Upper_Bound_Value :=
               Store_Symbol_Bound (Get_Array_Attr_Bound_Symbol (Upper_Bound));
+         when N_Identifier =>
+            Upper_Bound_Value :=
+               Store_Symbol_Bound (Bound_Type_Symbol (Upper_Bound));
          when others =>
             Report_Unhandled_Node_Empty (Upper_Bound,
                                          "Do_Base_Range_Constraint",
                                          "unsupported upper range kind");
       end case;
 
-      Set_Width (Result_Type, Get_Width (Resolved_Underlying));
+      if Kind (Resolved_Underlying) = I_C_Enum_Type then
+         Set_Width (Result_Type,
+          Get_Width (Get_Subtype (Resolved_Underlying)));
+      else
+         Set_Width (Result_Type, Get_Width (Resolved_Underlying));
+      end if;
       Set_Lower_Bound (Result_Type, Lower_Bound_Value);
       Set_Upper_Bound (Result_Type, Upper_Bound_Value);
       return Result_Type;
@@ -792,23 +805,44 @@ package body Tree_Walk is
 
       procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id);
 
+      function Handle_Enum_Symbol_Members (Mem : Irep) return Irep;
+      function Handle_Enum_Symbol_Members (Mem : Irep) return Irep is
+         Followed_Type_Symbol : constant Irep :=
+            Follow_Symbol_Type (Get_Type (Mem), Global_Symbol_Table);
+      begin
+         if Kind (Followed_Type_Symbol) = I_C_Enum_Type then
+            declare
+               Val : constant Irep := Global_Symbol_Table
+                 (Intern
+                    (Get_Identifier
+                     (Mem)))
+                 .Value;
+            begin
+               return Val;
+            end;
+         else
+            return Mem;
+         end if;
+      end Handle_Enum_Symbol_Members;
+
       ----------------------
       -- Handle_Parameter --
       ----------------------
 
       procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id) is
          Is_Out        : constant Boolean := Out_Present (Parent (Formal));
          Actual_Irep   : Irep;
-
+         Expression    : constant Irep := Do_Expression (Actual);
       begin
          if Is_Out and then
-           not (Kind (Get_Type (Do_Expression (Actual))) in Class_Type)
+           not (Kind (Get_Type (Expression)) in Class_Type)
          then
             Report_Unhandled_Node_Empty (Actual, "Handle_Parameter",
                                          "Kind of actual not in class type");
             return;
          end if;
-         Actual_Irep := Wrap_Argument (Do_Expression (Actual), Is_Out);
+         Actual_Irep := Wrap_Argument (
+          Handle_Enum_Symbol_Members (Expression), Is_Out);
          Append_Argument (Args, Actual_Irep);
       end Handle_Parameter;
 
@@ -2882,6 +2916,24 @@ package body Tree_Walk is
 
       --  Begin processing for Do_Object_Declaration_Full_Declaration
 
+      procedure Register_Identifier_In_Symbol_Table (N : Irep; Val : Irep)
+        with Pre => Kind (N) = I_Symbol_Expr;
+      procedure Register_Identifier_In_Symbol_Table (N : Irep; Val : Irep) is
+         Identifier_Name : constant Symbol_Id :=
+            Intern (Get_Identifier (N));
+         Identifier_Symbol : Symbol;
+      begin
+         Identifier_Symbol.Name       := Identifier_Name;
+         Identifier_Symbol.BaseName   := Identifier_Name;
+         Identifier_Symbol.PrettyName := Identifier_Name;
+         Identifier_Symbol.SymType    := Get_Type (N);
+         Identifier_Symbol.Mode       := Intern ("C");
+         Identifier_Symbol.Value      := Val;
+         Global_Symbol_Table.Insert (Identifier_Name, Identifier_Symbol);
+      end Register_Identifier_In_Symbol_Table;
+
+      Is_In_Symtab : constant Boolean :=
+        Global_Symbol_Table.Contains (Intern (Get_Identifier (Id)));
    begin
       Set_Source_Location (Decl, (Sloc (N)));
       Set_Symbol (Decl, Id);
@@ -2907,6 +2959,11 @@ package body Tree_Walk is
                                              Rhs => Init_Expr,
                                              Source_Location => Sloc (N)));
       end if;
+
+      if not Is_In_Symtab then
+         Register_Identifier_In_Symbol_Table (Id, Init_Expr);
+      end if;
+
    end Do_Object_Declaration_Full;
 
    -------------------------

testsuite/gnat2goto/tests/range_second/range_second.adb

@@ -0,0 +1,20 @@
+procedure Range_Second is
+  type Indicator_Type is (
+    CALIBRATION_MODE,
+    MEASUREMENT_MODE,
+    CALIBRATION_PASS,
+    CALIBRATION_FAIL,
+    MEASUREMENT_NOT_PROVEN,
+    MEASUREMENT_PRESENT);
+
+  subtype Result_Indicator_Type is Indicator_Type range CALIBRATION_PASS .. MEASUREMENT_NOT_PROVEN;
+
+  procedure Testable (Result : Result_Indicator_Type) is
+  begin
+    null;
+  end Testable;
+
+begin
+  Testable (CALIBRATION_PASS);
+  Testable (MEASUREMENT_PRESENT);
+end Range_Second;

testsuite/gnat2goto/tests/range_second/range_third.adb

@@ -0,0 +1,14 @@
+procedure Range_Second is
+  type An_Int is range 1..1000;
+  subtype Another_Int is An_Int range 5..100;
+
+  procedure Testable (Result : An_Int) is
+    test_val : Another_Int := Result;
+  begin
+    null;
+  end Testable;
+
+begin
+  Testable (50);
+  Testable (200);
+end Range_Second;

testsuite/gnat2goto/tests/range_second/test.opt

@@ -0,0 +1,2 @@
+ALL XFAIL Doesn't crash anymore but cbmc does not perform range assertion checks 
+

testsuite/gnat2goto/tests/range_second/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()