From 2e691665f63f8d2307346903c5ca03e85ca66de5 Mon Sep 17 00:00:00 2001
From: Trevor Jennings <TrevorJennings@bcs.org>
Date: Fri, 28 Jun 2019 19:01:30 +0100
Subject: [PATCH] Add test for enumeration out parameters

Test currently fails with gnat2goto raising:
SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from ireps.ads:1875
---
 .../gnat2goto/tests/enum_out_param/enum_out.adb    | 14 ++++++++++++++
 testsuite/gnat2goto/tests/enum_out_param/test.opt  |  1 +
 testsuite/gnat2goto/tests/enum_out_param/test.out  |  2 ++
 testsuite/gnat2goto/tests/enum_out_param/test.py   |  3 +++
 4 files changed, 20 insertions(+)
 create mode 100644 testsuite/gnat2goto/tests/enum_out_param/enum_out.adb
 create mode 100644 testsuite/gnat2goto/tests/enum_out_param/test.opt
 create mode 100644 testsuite/gnat2goto/tests/enum_out_param/test.out
 create mode 100644 testsuite/gnat2goto/tests/enum_out_param/test.py

diff --git a/testsuite/gnat2goto/tests/enum_out_param/enum_out.adb b/testsuite/gnat2goto/tests/enum_out_param/enum_out.adb
new file mode 100644
index 000000000..4fbd6bcab
--- /dev/null
+++ b/testsuite/gnat2goto/tests/enum_out_param/enum_out.adb
@@ -0,0 +1,14 @@
+procedure Enum_Out is
+   type Enum is (One, Two, Three);
+
+   procedure P_Out (E : out Enum) is
+   begin
+      E := Two;
+   end P_Out;
+
+   Var_E : Enum;
+
+begin
+   P_Out (Var_E);
+   pragma Assert (Var_E = Two);
+end Enum_Out;
diff --git a/testsuite/gnat2goto/tests/enum_out_param/test.opt b/testsuite/gnat2goto/tests/enum_out_param/test.opt
new file mode 100644
index 000000000..ec4050d23
--- /dev/null
+++ b/testsuite/gnat2goto/tests/enum_out_param/test.opt
@@ -0,0 +1 @@
+ALL XFAIL gnat2goto fails with "raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from ireps.ads:1875"
diff --git a/testsuite/gnat2goto/tests/enum_out_param/test.out b/testsuite/gnat2goto/tests/enum_out_param/test.out
new file mode 100644
index 000000000..30c1435ad
--- /dev/null
+++ b/testsuite/gnat2goto/tests/enum_out_param/test.out
@@ -0,0 +1,2 @@
+[1] file enum_out.adb line 13 assertion: SUCCESS
+VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/enum_out_param/test.py b/testsuite/gnat2goto/tests/enum_out_param/test.py
new file mode 100644
index 000000000..0017741b4
--- /dev/null
+++ b/testsuite/gnat2goto/tests/enum_out_param/test.py
@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()