Remove support for specifying ASVAT models via a pragma Import.

tjj2017 · tjj2017 · commit 6ec3ce7b0ca4 · 2020-05-26T16:42:37.000+01:00
In the CI tests there are many eaxmples of pragma Import with convention
Ada which are not ASVAT models.  It might be possible to resolve such
instances but since Annotate ASVAT is now the preferred way to specify
ASVAT models, it seemed better remove support for specifying via Import.

Also this branch included code to check whether an Intrinsic program had
a body known to gnat2goto.  If this check was to comprehensive it should
also check if an Imported subprogram with convention Ada has body known
to gnat2goto.  After some consideration, it was decided that this
should not be checked by gnat2goto but at the link phase. So the
Intrinsic check has been removed.

Gnat2goto still checks and reports an unsupported node if a called
subprogram is not in the symbol table.
diff --git a/gnat2goto/driver/asvat-modelling.adb b/gnat2goto/driver/asvat-modelling.adb
@@ -1,9 +1,9 @@
 with Ada.Characters.Handling; use Ada.Characters.Handling;
 with Namet;                   use Namet;
-with Stringt;                 use Stringt;
 with Nlists;                  use Nlists;
 with Einfo;                   use Einfo;
 with Aspects;                 use Aspects;
+with Sem_Util;                use Sem_Util;
 with Ireps;                   use Ireps;
 with Follow;                  use Follow;
 with Range_Check;             use Range_Check;
@@ -42,128 +42,14 @@ package body ASVAT.Modelling is
       return Result;
    end Find_Model;
 
-   -------------------------
-   -- Get_Annotation_Name --
-   -------------------------
-
-   function Get_Annotation_Name (N : Node_Id) return String is
-     (Get_Name_String
-        (Chars (Expression
-                (First (Pragma_Argument_Associations (N))))));
-
-   ---------------------------
-   -- Get_Import_Convention --
-   ---------------------------
-
-   function Get_Import_Convention (N : Node_Id) return String is
-      --  The gnat front end insists thet the parameters for
-      --  pragma Import are given in the specified order even
-      --  if named association is used:
-      --  1. Convention,
-      --  2. Enity,
-      --  3. Optional External_Name,
-      --  4. Optional Link_Name.
-      --  The first 2 parameters are mandatory and
-      --  for ASVAT models the External_Name is required.
-      --
-      --  The Convention parameter will always be present as
-      --  the first parameter.
-      Conv_Assoc : constant Node_Id :=
-        First (Pragma_Argument_Associations (N));
-      Conv_Name  : constant Name_Id := Chars (Conv_Assoc);
-      Convention : constant String  := Get_Name_String
-        (Chars (Expression (Conv_Assoc)));
-   begin
-      --  Double check the named parameter if named association is used.
-      pragma Assert (Conv_Name = No_Name or else
-                     Get_Name_String (Conv_Name) = "convention");
-      return Convention;
-   end Get_Import_Convention;
-
-   ------------------------------
-   -- Get_Import_External_Name --
-   ------------------------------
-
-   function Get_Import_External_Name (N : Node_Id) return String is
-      --  The gnat front end insists thet the parameters for
-      --  pragma Import are given in the specified order even
-      --  if named association is used:
-      --  1. Convention,
-      --  2. Enity,
-      --  3. Optional External_Name,
-      --  4. Optional Link_Name.
-      --  The first 2 parameters are mandatory and
-      --  for ASVAT models the External_Name is required.
-      --
-      --  The External_Name parameter, if present, will be
-      --  the third parameter.
-      External_Assoc : constant Node_Id := Next
-        (Next
-           (First (Pragma_Argument_Associations (N))));
-   begin
-      if Present (External_Assoc) then
-         declare
-            External_Name : constant Name_Id := Chars (External_Assoc);
-            External_Name_Id : constant String_Id :=
-              Strval (Expression (External_Assoc));
-            External_Name_Id_Length : constant Natural :=
-              Natural (String_Length (External_Name_Id));
-         begin
-            --  Double check the named parameter if named association is used.
-            pragma Assert (External_Name = No_Name or else
-                             Get_Name_String
-                               (External_Name) = "external_name");
-            String_To_Name_Buffer (External_Name_Id);
-            return To_Lower (Name_Buffer (1 .. External_Name_Id_Length));
-         end;
-      else
-         return "";
-      end if;
-   end Get_Import_External_Name;
-
-   --------------------------
-   -- Get_Import_Link_Name --
-   --------------------------
-
-   function Get_Import_Link_Name (N : Node_Id) return String is
-      --  The gnat front end insists thet the parameters for
-      --  pragma Import are given in the specified order even
-      --  if named association is used:
-      --  1. Convention,
-      --  2. Enity,
-      --  3. Optional External_Name,
-      --  4. Optional Link_Name.
-      --  The first 2 parameters are mandatory and
-      --  for ASVAT models the External_Name is required
-      --  and for imported non-visible objects, Link_Name is required.
-      --  The Link_Name parameter, if present, will be
-      --  the Fourth parameter.
-      External_Assoc : constant Node_Id := Next
-        (Next
-           (First (Pragma_Argument_Associations (N))));
-      Link_Assoc     : constant Node_Id :=
-        (if Present (External_Assoc) then Next (External_Assoc)
-         else External_Assoc);
-   begin
-      if Present (Link_Assoc) then
-         declare
-            Link_Name    : constant Name_Id := Chars (Link_Assoc);
-            Link_Name_Id : constant String_Id :=
-              Strval (Expression (Link_Assoc));
-            Link_Name_Id_Length : constant Natural :=
-              Natural (String_Length (Link_Name_Id));
-         begin
-            --  Double check the named parameter if named association is used.
-            pragma Assert (Link_Name = No_Name or else
-                             Get_Name_String
-                               (Link_Name) = "link_name");
-            String_To_Name_Buffer (Link_Name_Id);
-            return To_Lower (Name_Buffer (1 .. Link_Name_Id_Length));
-         end;
-      else
-         return "";
-      end if;
-   end Get_Import_Link_Name;
+--     -------------------------
+--     -- Get_Annotation_Name --
+--     -------------------------
+--
+--     function Get_Annotation_Name (N : Node_Id) return String is
+--       (Get_Name_String
+--          (Chars (Expression
+--                  (First (Pragma_Argument_Associations (N))))));
 
    -------------------------
    -- Get_Model_From_Anno --
@@ -224,51 +110,11 @@ package body ASVAT.Modelling is
       end if;
    end Get_Model_From_Anno;
 
-   ---------------------------
-   -- Get_Model_From_Import --
-   ---------------------------
-
-   function Get_Model_From_Import (N : Node_Id) return Model_Sorts is
-      Convention : constant String :=
-        Get_Import_Convention (N);
-
-      Is_Ada : constant Boolean := Convention = "ada";
-
-      Model_String  : constant String :=
-        (if Is_Ada then
-            Get_Import_External_Name (N)
-         else
-            "");
-      Model : constant Model_Sorts := Find_Model (Model_String);
-   begin
-      if Is_Ada then
-         if Model_String = "" then
-            Report_Unhandled_Node_Empty
-              (N, "Get_Model_From_Import",
-               "Import convention Ada must have a model sort");
-         elsif Model = Not_A_Model then
-            Report_Unhandled_Node_Empty
-              (N, "Get_Model_From_Import",
-               "Import convention Ada but '" &
-                 Model_String &
-                 "' is not an ASVAT model sort");
-         end if;
-      end if;
-      return Model;
-   end Get_Model_From_Import;
-
    --------------------
    -- Get_Model_Sort --
    --------------------
 
    function Get_Model_Sort (E : Entity_Id) return Model_Sorts is
-      Obj_Import    : constant Node_Id := Get_Pragma (E, Pragma_Import);
-      Subprog_Import : constant Node_Id :=
-        (if Ekind (E) in E_Procedure | E_Function then
-              Import_Pragma (E)
-         else
-            Obj_Import);
-
       Anno           : constant Node_Id := Find_Aspect (E, Aspect_Annotate);
 
       Anno_Model     : constant Model_Sorts :=
@@ -277,27 +123,8 @@ package body ASVAT.Modelling is
          else
             Not_A_Model);
 
-      --  The ASVAT anotation is used even if there is a pragma Import
-      --  specifying a, possibly different, model.
-      Import_Model   : constant Model_Sorts :=
-        (if Present (Obj_Import) then
-              (if Anno_Model = Not_A_Model then
-                   Get_Model_From_Import (Obj_Import)
-              else
-                 Anno_Model)
-         elsif Present (Subprog_Import) then
-              (if Anno_Model = Not_A_Model then
-                   Get_Model_From_Import (Subprog_Import)
-              else
-                 Anno_Model)
-         else
-            Not_A_Model);
-
    begin
-      return (if Anno_Model /= Not_A_Model then
-                 Anno_Model
-              else
-                 Import_Model);
+      return Anno_Model;
    end Get_Model_Sort;
 
    --------------------------
diff --git a/gnat2goto/driver/asvat-modelling.ads b/gnat2goto/driver/asvat-modelling.ads
@@ -33,35 +33,33 @@
 --  is also not visible).
 --
 --  The ASVAT models are associated with Ada subprograms (or objects, in
---  the case of Represents) by an Annotate aspect specifications or by a
---  pragma Import.
+--  the case of Represents) by an Annotate aspect specifications.
 --
 --  Generally modelling subprograms will not have a body as they represent
 --  features of the system that are not being directly analysed by ASVAT,
 --  this is the very reason that a model of their behaviour is requred.
---  If the model is associated via an Import pragma the subprogram cannot
---  have a body (An Ada rule).  If the model is associated by an Annotation
+--  When an ASVAT model is associated with an entity by an Annotation
 --  aspect specification then usually an Import => True will be included in
 --  the aspect specification.  If Import => True is not in the
 --  aspect specification the subprogram, Ada rules require the subprogram
 --  to have a body but it will be ignored by ASVAT.
 --
---  Associating Represents to a declaration of a local variable indicates that
---  the variable represents a more global variable that is not visible in the
---  context of the local declaration.  Furthermore, if the type of the
---  non-visible variable a local type declaration can be used to represent
---  this too.
+--  Associating Represents model with a declaration of a local variable
+--  indicates that the variable represents a more global variable that is
+--  not visible in the context of the local declaration.
+--  Furthermore, if the type of the non-visible variable a
+--  local type declaration can be used to representthis too.
+--
 --  The local declaration of the variable (and its type, if the type of
 --  the non-visible variable is also not visible) must exactly match the
 --  declaration of the non-visible variable (and its type if necessary).
 --  The purpose of these declarations is to represent global variables of
 --  the subprogram which are indirectly updated by the subprogram but not
 --  directly visible to it.
 --
---  The models can be associated in one of two ways, by an ASVAT annotation or,
---  by using an Import pragma.  The ASVAT annotation is the preferred method.
+--  The ASVAT models are associated with an entity by an ASVAT annotation.
 --
---  Using the ASVAT annotation:
+--  Examples:
 --  type My_Int is range 1 .. 100;
 --
 --  X : Integer;  --  A normal, visible variable.
@@ -76,8 +74,8 @@
 --                           "Hidden_Type.My_Int"  --  Its non-visible type
 --                   );
 --
---  The name of a modelling subprogram can be any legal Ada subprogram name
---  except operator names.
+--  The name of a subprogram associated with an ASVAT model can be any legal
+--  Ada subprogram name except operator names.
 --
 --  function In_Type (N : My_Int) return Boolean
 --  with Annotate => (ASVAT, In_Type_Function),
@@ -97,45 +95,13 @@
 --       Annotate => (ASVAT, Nondet_In_Type_Vars),
 --       Import   => True;
 --
---  Using pragma Import - the convention Ada indicates it is an ASVAT model:
---  type My_Int is range 1 .. 100;
---
---  X : Integer;  --  A normal, visible variable
---
---  I : Integer;  --  Represents a variable that is not visible.
---  pragma Import (Ada, I, "Represents", "Hidden_Vars.I");
---
---  J : My_Int;   --  Represents a non-visible variable whose type is also
---                -- not visible.
---  pragma Import (Convention    => Ada,
---                 Entity        => J,
---                 External_Name => "Represents",
---                 Link_Name     => "Hidden_Vars.J:Hidden_Type.My_Int");
---  --  Notice the hidden type follows the colon. No spaces allowed.
---
---  The name of a modelling subprogram can be any legal Ada subprogram name
---  except operator names.
---
---  function In_Type (N : My_Int) return Boolean;
---  pragma Import (Ada, In_Type, "In_Type_Function");
---
---  function Nondet_Integer return Integer
---  pragma Global (null);
---  pragma Import (Ada, Non_Det_Integer, "Nondet_Function");
---
---  procedure Update
---  pragma Global ((In_Out => (I, J, X));
---  pragma Import (Ada, Update, "Nondet");
---
---  procedure Read (I : out Integer)
---  pragma Global null,
---  pragma Import (Ada, Read, "Nondet");
+--  Current limitations:
+--  Only Annotate aspect specifications are supported.
+--  Pragma Annotate is not currently supported.
 
 with Types;                   use Types;
 with Atree;                   use Atree;
 with Sinfo;                   use Sinfo;
-with Sem_Util;                use Sem_Util;
-with Snames;                  use Snames;
 
 package ASVAT.Modelling is
    type Model_Sorts is
@@ -144,30 +110,13 @@ package ASVAT.Modelling is
    subtype Valid_Model is Model_Sorts range
      Nondet_Function .. Model_Sorts'Last;
 
-   function Get_Annotation_Name (N : Node_Id) return String
-   with Pre => Nkind (N) = N_Pragma and then
-               Get_Pragma_Id (N) = Pragma_Annotate;
-
-   function Get_Import_Convention (N : Node_Id) return String
-   with Pre => Nkind (N) = N_Pragma and then
-               Get_Pragma_Id (N) = Pragma_Import;
-
-   function Get_Import_External_Name (N : Node_Id) return String
-   with Pre => Nkind (N) = N_Pragma and then
-               Get_Pragma_Id (N) = Pragma_Import;
-   --  Returns null string if the External_Name parameter is not present.
-
-   function Get_Import_Link_Name (N : Node_Id) return String
-   with Pre => Nkind (N) = N_Pragma and then
-               Get_Pragma_Id (N) = Pragma_Import;
-   --  Returns null string if the Link_Name parameter is not present.
+--     function Get_Annotation_Name (N : Node_Id) return String
+--     with Pre => Nkind (N) = N_Pragma and then
+--                 Get_Pragma_Id (N) = Pragma_Annotate;
 
    function Get_Model_From_Anno (N : Node_Id) return Model_Sorts
    with Pre => Nkind (N) = N_Aspect_Specification;
 
-   function Get_Model_From_Import (N : Node_Id) return Model_Sorts
-   with Pre => Nkind (N) = N_Pragma and then Get_Pragma_Id (N) = Pragma_Import;
-
    function Get_Model_Sort (E : Entity_Id) return Model_Sorts;
 
    function Is_Model (Model : Model_Sorts) return Boolean is
diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb
