Add support to ignore refine pragmas

Author: Petr Bauch

gnat2goto/driver/tree_walk.adb

@@ -407,7 +407,7 @@ package body Tree_Walk is
 
    procedure Declare_Itype (Ty : Entity_Id) is
    begin
-      if Is_Itype (Ty) then
+      if Present (Ty) and then Is_Itype (Ty) then
          declare
             Ty_Name : constant Symbol_Id := Intern (Unique_Name (Ty));
             Ty_Symbol : Symbol;
@@ -2128,6 +2128,8 @@ package body Tree_Walk is
       --  Handle pragmas that suppress some checks by explicitly ignoring them
       procedure Do_Pragma_Suppress
         (N_Orig : Node_Id);
+      procedure Do_Pragma_Refine
+        (N_Orig : Node_Id);
 
       procedure Do_Pragma_Assert_or_Assume
         (N_Orig : Node_Id; Block : Irep)
@@ -2227,6 +2229,54 @@ package body Tree_Walk is
 
       end Do_Pragma_Suppress;
 
+      procedure Do_Pragma_Refine
+        (N_Orig : Node_Id)
+      is
+         --  To be set by iterator:
+         Components : List_Id;
+         Component_Expression : Node_Id;
+         CEE : List_Id;
+         Scope_Size : Nat;
+
+         ----------------
+         -- Handle_Arg --
+         ----------------
+
+         procedure Handle_Arg
+           (Arg_Pos : Positive; Arg_Name : Name_Id; Expr : Node_Id);
+
+         procedure Handle_Arg
+           (Arg_Pos : Positive; Arg_Name : Name_Id; Expr : Node_Id) is
+         begin
+
+            if Arg_Name = No_Name and then
+              Arg_Pos = 1 and then
+              Nkind (Expr) = N_Aggregate
+            then
+               Components := Component_Associations (Expr);
+               Component_Expression := Expression (First (Components));
+               CEE := Expressions (Component_Expression);
+               Scope_Size := List_Length (CEE);
+            else
+               Report_Unhandled_Node_Empty (N, "Do_Pragma_Suppress",
+                                            "Unknown arg name");
+            end if;
+         end Handle_Arg;
+
+         procedure Iterate_Args is new
+           Iterate_Pragma_Parameters (Handle_Arg => Handle_Arg);
+
+      begin
+         Iterate_Args (N_Orig);
+         if Scope_Size > 1
+         then
+            null; -- Intentionally ignoring this request to suppress all checks
+         else
+            null; -- Intentionally ignoring supressing some checks
+         end if;
+
+      end Do_Pragma_Refine;
+
       N_Orig : Node_Id;
 
    begin
@@ -2241,8 +2291,11 @@ package body Tree_Walk is
          when Name_Annotate =>
             --  Ignore here. Rather look for those when we process a node.
             null;
+         when Name_Refined_State | Name_Refined_Global |
+              Name_Refined_Depends =>
+            Do_Pragma_Refine (N_Orig);
          when Name_SPARK_Mode | Name_Global | Name_Postcondition |
-              Name_Refined_State | Name_Refined_Global | Name_Precondition =>
+              Name_Precondition =>
             --  These pragmas are currently unimplemented
             Report_Unhandled_Node_Empty (N, "Do_Pragma",
                                          "Unsupported pragma");