Merge pull request #246 from chrisr-diffblue/feature/pragma-declaration-volatile

Feature/pragma declaration volatile

Author: chrisr-diffblue

experiments/golden-results/SPARK-tetris-summary.txt

@@ -3,11 +3,6 @@ Calling function: Process_Declaration
 Error message: Package declaration
 Nkind: N_Package_Declaration
 --
-Occurs: 9 times
-Calling function: Process_Pragma_Declaration
-Error message: Unsupported pragma: Volatile
-Nkind: N_Pragma
---
 Occurs: 1 times
 Calling function: Process_Declaration
 Error message: Representation clause unsupported: component_size

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

@@ -3,11 +3,6 @@ Calling function: Process_Declaration
 Error message: Representation clause unsupported: address
 Nkind: N_Attribute_Definition_Clause
 --
-Occurs: 37 times
-Calling function: Process_Pragma_Declaration
-Error message: Unsupported pragma: Volatile
-Nkind: N_Pragma
---
 Occurs: 8 times
 Calling function: Process_Declaration
 Error message: Representation clause unsupported: component_size

gnat2goto/driver/tree_walk.adb

@@ -4761,6 +4761,28 @@ package body Tree_Walk is
    end Process_Declaration;
 
    procedure Process_Pragma_Declaration (N : Node_Id) is
+      procedure Handle_Pragma_Volatile (N : Node_Id);
+
+      procedure Handle_Pragma_Volatile (N : Node_Id) is
+         Argument_Associations : constant List_Id :=
+           Pragma_Argument_Associations (N);
+         First_Argument_Expression : constant Node_Id :=
+           Expression (First (Argument_Associations));
+         Expression_Id : constant Symbol_Id :=
+           Intern (Unique_Name (Entity (First_Argument_Expression)));
+
+         procedure Set_Volatile (Key : Symbol_Id; Element : in out Symbol);
+         procedure Set_Volatile (Key : Symbol_Id; Element : in out Symbol) is
+         begin
+            pragma Assert (Unintern (Key) = Unintern (Expression_Id));
+            Element.IsVolatile := True;
+         end Set_Volatile;
+      begin
+         pragma Assert (Global_Symbol_Table.Contains (Expression_Id));
+         Global_Symbol_Table.Update_Element (
+                          Position => Global_Symbol_Table.Find (Expression_Id),
+                          Process  => Set_Volatile'Access);
+      end Handle_Pragma_Volatile;
    begin
       case Pragma_Name (N) is
          when Name_Assert |
@@ -4819,8 +4841,7 @@ package body Tree_Walk is
             --  they may be modified by the environment. Effectively, they need
             --  to be modelled as non-deterministic input in every state. It
             --  changes the semantics wrt to thread interleavings.
-            Report_Unhandled_Node_Empty (N, "Process_Pragma_Declaration",
-                                         "Unsupported pragma: Volatile");
+            Handle_Pragma_Volatile (N);
          when Name_Attach_Handler =>
             --  The expression in the Attach_Handler pragma as evaluated at
             --  object creation time specifies an interrupt. As part of the

testsuite/gnat2goto/tests/volatile/test.out

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

testsuite/gnat2goto/tests/volatile/test.py

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

testsuite/gnat2goto/tests/volatile/volatile_type.adb

@@ -0,0 +1,16 @@
+procedure Volatile_Type is
+   Data: Integer;
+   pragma Volatile(Data);
+   Flag: Boolean;
+   pragma Volatile(Flag);
+begin
+   Data := 42;
+   Flag := True;
+
+   if not Flag then
+      Data := 0;
+   end if;
+
+   pragma Assert (Data=42);
+
+end Volatile_Type;