Feature/pragma declaration attribute

experiments/golden-results/UKNI-Information-Barrier-summary.txt

@@ -43,11 +43,6 @@ Calling function: Process_Declaration
 Error message: Use package clause declaration
 Nkind: N_Use_Package_Clause
 --
-Occurs: 1 times
-Calling function: Process_Pragma_Declaration
-Error message: Unsupported pragma: Machine Attribute
-Nkind: N_Pragma
---
 Occurs: 5 times
 Redacted compiler error message:
 "REDACTED" not declared in "REDACTED"

gnat2goto/driver/tree_walk.adb

@@ -4762,6 +4762,9 @@ package body Tree_Walk is
 
    procedure Process_Pragma_Declaration (N : Node_Id) is
       procedure Handle_Pragma_Volatile (N : Node_Id);
+      procedure Handle_Pragma_Machine_Attribute (N : Node_Id)
+        with Pre => Nkind (N) in N_Pragma
+        and then Pragma_Name (N) = Name_Machine_Attribute;
 
       procedure Handle_Pragma_Volatile (N : Node_Id) is
          Argument_Associations : constant List_Id :=
@@ -4783,6 +4786,38 @@ package body Tree_Walk is
                           Position => Global_Symbol_Table.Find (Expression_Id),
                           Process  => Set_Volatile'Access);
       end Handle_Pragma_Volatile;
+
+      procedure Handle_Pragma_Machine_Attribute (N : Node_Id) is
+         Argument_Associations : constant List_Id :=
+           Pragma_Argument_Associations (N);
+
+         --  first is the identifier to be given the attribute
+         First_Argument : constant Node_Id := First (Argument_Associations);
+
+         --  second is the attribute as string
+         Second_Argument : constant Node_Id := Next (First_Argument);
+         Attr_String_Id : constant String_Id :=
+           Strval (Expression (Second_Argument));
+         Attr_Length : constant Integer :=
+           Integer (String_Length (Attr_String_Id));
+      begin
+         String_To_Name_Buffer (Attr_String_Id);
+         declare
+            Attr_String : String
+              renames Name_Buffer (1 .. Attr_Length);
+         begin
+            if Attr_String = "signal" then
+            --  CBMC would not acknowledge this one anyway -> Ignored
+               null;
+            else
+               Report_Unhandled_Node_Empty
+                 (N, "Process_Pragma_Declaration",
+                  "Unsupported pragma: Machine Attribute "
+                  & Attr_String);
+            end if;
+         end;
+      end Handle_Pragma_Machine_Attribute;
+
    begin
       case Pragma_Name (N) is
          when Name_Assert |
@@ -4948,8 +4983,7 @@ package body Tree_Walk is
             Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
                                "Known but unsupported pragma: Linker Options");
          when Name_Machine_Attribute =>
-            Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
-                                      "Unsupported pragma: Machine Attribute");
+            Handle_Pragma_Machine_Attribute (N);
          when Name_Check =>
             Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
                                          "Unsupported pragma: Check");

testsuite/gnat2goto/tests/pragma_machine_attribute/pragma_machine_attribute.adb

@@ -0,0 +1,23 @@
+procedure Pragma_Machine_Attribute is
+
+   procedure Timer_Interrupt;
+   pragma Machine_Attribute (Timer_Interrupt, "signal");
+
+   Seconds_Count : Integer := 0;
+   Interval : Integer := 1;
+   Timeout : Boolean := False;
+
+   procedure Timer_Interrupt is
+   begin
+      Seconds_Count := Seconds_Count + 1;
+      if Seconds_Count = Interval then
+         Timeout := True;
+      end if;
+   end Timer_Interrupt;
+
+begin
+   Timer_Interrupt;
+
+   pragma Assert (Timeout and Interval = Seconds_Count);
+
+end Pragma_Machine_Attribute;

testsuite/gnat2goto/tests/pragma_machine_attribute/test.out

@@ -0,0 +1,2 @@
+[1] file pragma_machine_attribute.adb line 21 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/pragma_machine_attribute/test.py

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