From 5ddad92dfc81b0333990dc1956544e924a14600a Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Fri, 10 Mar 2017 12:00:35 -0500
Subject: Add tests for handling of warnings

---
 test-suite/output/RecognizePluginWarning.out | 0
 test-suite/output/RecognizePluginWarning.v   | 5 +++++
 test-suite/output/UsePluginWarning.out       | 1 +
 test-suite/output/UsePluginWarning.v         | 7 +++++++
 4 files changed, 13 insertions(+)
 create mode 100644 test-suite/output/RecognizePluginWarning.out
 create mode 100644 test-suite/output/RecognizePluginWarning.v
 create mode 100644 test-suite/output/UsePluginWarning.out
 create mode 100644 test-suite/output/UsePluginWarning.v

(limited to 'test-suite')

diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v
new file mode 100644
index 0000000000..cd667bbd00
--- /dev/null
+++ b/test-suite/output/RecognizePluginWarning.v
@@ -0,0 +1,5 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *)
+
+(* Test that mentioning a warning defined in plugins works. The failure
+mode here is that these result in a warning about unknown warnings, since the
+plugins are not known at command line parsing time. *)
diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out
new file mode 100644
index 0000000000..47409f3ec5
--- /dev/null
+++ b/test-suite/output/UsePluginWarning.out
@@ -0,0 +1 @@
+type foo = __
diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v
new file mode 100644
index 0000000000..c6e0054641
--- /dev/null
+++ b/test-suite/output/UsePluginWarning.v
@@ -0,0 +1,7 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *)
+
+Require Extraction.
+Axiom foo : Prop.
+
+Extraction foo.
+
-- 
cgit v1.2.3