From db2ffc59541b0baee40ae43b3a1b0508699944e3 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 9 May 2019 14:34:34 +0100 Subject: [PATCH 1/3] Handle pragma machine attribute Case by case based on what the attribute is. Attribute signal would probably be ignored by CBMC anyway. And so do we here. --- gnat2goto/driver/tree_walk.adb | 38 ++++++++++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb index 3c4f7b4eb..b0fa679db 100644 --- a/gnat2goto/driver/tree_walk.adb +++ b/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"); From 720991bb921b8e0d70c4e948a7d943925ba73445 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 9 May 2019 14:35:01 +0100 Subject: [PATCH 2/3] Add test for attribute signal Just to check that gnat2goto will not produce the unsupported feature report. --- .../pragma_machine_attribute.adb | 23 +++++++++++++++++++ .../tests/pragma_machine_attribute/test.out | 2 ++ .../tests/pragma_machine_attribute/test.py | 3 +++ 3 files changed, 28 insertions(+) create mode 100644 testsuite/gnat2goto/tests/pragma_machine_attribute/pragma_machine_attribute.adb create mode 100644 testsuite/gnat2goto/tests/pragma_machine_attribute/test.out create mode 100644 testsuite/gnat2goto/tests/pragma_machine_attribute/test.py diff --git a/testsuite/gnat2goto/tests/pragma_machine_attribute/pragma_machine_attribute.adb b/testsuite/gnat2goto/tests/pragma_machine_attribute/pragma_machine_attribute.adb new file mode 100644 index 000000000..ca60c272c --- /dev/null +++ b/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; diff --git a/testsuite/gnat2goto/tests/pragma_machine_attribute/test.out b/testsuite/gnat2goto/tests/pragma_machine_attribute/test.out new file mode 100644 index 000000000..d714a7d89 --- /dev/null +++ b/testsuite/gnat2goto/tests/pragma_machine_attribute/test.out @@ -0,0 +1,2 @@ +[1] file pragma_machine_attribute.adb line 21 assertion: SUCCESS +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/pragma_machine_attribute/test.py b/testsuite/gnat2goto/tests/pragma_machine_attribute/test.py new file mode 100644 index 000000000..0017741b4 --- /dev/null +++ b/testsuite/gnat2goto/tests/pragma_machine_attribute/test.py @@ -0,0 +1,3 @@ +from test_support import * + +prove() From f558622204ddf6c6aaba1b176daf52326dd08f03 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 9 May 2019 14:35:15 +0100 Subject: [PATCH 3/3] Update golden results --- .../golden-results/UKNI-Information-Barrier-summary.txt | 5 ----- 1 file changed, 5 deletions(-) diff --git a/experiments/golden-results/UKNI-Information-Barrier-summary.txt b/experiments/golden-results/UKNI-Information-Barrier-summary.txt index 1872a1cd7..b2ea6bd2f 100644 --- a/experiments/golden-results/UKNI-Information-Barrier-summary.txt +++ b/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"