Commit 4043ad2c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

hoa: diagnose unsupported Headers

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Test it.
parent 8004dca1
......@@ -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
......
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment