From 4043ad2ccf30a926f48407cf5cc85c5cffc833b3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 21 Nov 2014 16:39:33 +0100
Subject: [PATCH] hoa: diagnose unsupported Headers

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Test it.
---
 src/hoaparse/hoaparse.yy   |  8 ++++++++
 src/tgbatest/hoaparse.test | 37 +++++++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index f89363aa1..fb8026399 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -287,6 +287,14 @@ header-item: "States:" INT
 	     }
            | "properties:" properties
            | HEADERNAME header-spec
+	     {
+	       char c = (*$1)[0];
+	       if (c >= 'A' && c <= 'Z')
+		 error(@$, "ignoring unsupported header \"" + *$1 + ":\"\n\t"
+		       "(but the capital indicates information that should not"
+		       " be ignored)");
+	       delete $1;
+	     }
 
 ap-names: | ap-names ap-name
 ap-name: STRING
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index b11a19a98..30da7963c 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -523,3 +523,40 @@ State: 1
 [0] 0
 --END--
 EOF
+
+
+cat >input <<EOF
+HOA: v1
+States: 2
+Start: 0
+Important: 4 very important "!"
+AP: 0
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0 {0} 1
+State: 1 0
+--END--
+EOF
+
+expecterr input <<EOF
+input:4.1-31: ignoring unsupported header "Important:"
+	(but the capital indicates information that should not be ignored)
+EOF
+
+cat >expected <<EOF
+HOA: v1
+States: 2
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete deterministic
+--BODY--
+State: 0 {0}
+[t] 1
+State: 1
+[t] 0
+--END--
+EOF
+
+diff expected input.out