From 4c06afa41f432ab2d7901256e351ccd430e455ce Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 20 Jul 2021 11:08:52 +0100 Subject: [PATCH 1/5] Output description in XML This unifies XML output with JSON output for results by also outputting the "description" in the XML. Fixes #3798 --- src/goto-checker/properties.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp index 5074bb3d83a..1d7d95d1b1b 100644 --- a/src/goto-checker/properties.cpp +++ b/src/goto-checker/properties.cpp @@ -109,6 +109,7 @@ xmlt xml(const irep_idt &property_id, const property_infot &property_info) xmlt xml_result("result"); xml_result.set_attribute("property", id2string(property_id)); xml_result.set_attribute("status", as_string(property_info.status)); + xml_result.set_attribute("description", as_string(property_info.description)); return xml_result; } From 0b88930f5921f1eadd7af55734263ebc406f51f9 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 20 Jul 2021 11:11:21 +0100 Subject: [PATCH 2/5] Fix regression test using XML output Fix regression test that matches on XML output, now includes description.. --- regression/cbmc/xml-interface1/test.desc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/xml-interface1/test.desc b/regression/cbmc/xml-interface1/test.desc index 8ef70fe541a..1bfcf38e7fc 100644 --- a/regression/cbmc/xml-interface1/test.desc +++ b/regression/cbmc/xml-interface1/test.desc @@ -4,8 +4,8 @@ CORE ^EXIT=10$ ^SIGNAL=0$ Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0 - - + + VERIFICATION FAILED -- From 624743d9996595225ac77d24d0910439333f233f Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 20 Jul 2021 13:57:17 +0100 Subject: [PATCH 3/5] Update XML schema to allow description in results This updates the XML schema that is used to validate XML output to now allow desciption in result output. --- doc/assets/xml_spec.xsd | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd index df05a215ea5..bd00275ac98 100644 --- a/doc/assets/xml_spec.xsd +++ b/doc/assets/xml_spec.xsd @@ -166,6 +166,7 @@ + From 6f521a49dabd44a0bbe344274b552e5087c6c552 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 20 Jul 2021 13:57:58 +0100 Subject: [PATCH 4/5] Skip tests that display unprintable characters in XML This skips two tests that use characters for operators where the character cannot be printed in XML --- regression/validate-trace-xml-schema/check.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 0b153f61854..a34056e2f82 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -61,7 +61,10 @@ # the SAT back-end only ['integer-assignments1', 'test.desc'], # this test is expected to abort, thus producing invalid XML - ['String_Abstraction17', 'test.desc'] + ['String_Abstraction17', 'test.desc'], + # these tests use characters that cannot be displayed in XML + ['ACSL', 'operators.desc'], + ['ACSL', 'quantifier-precedence.desc'] ])) # TODO maybe consider looking them up on PATH, but direct paths are From cb2457b5fac8b85fb4202ff0ad50797066d0b723 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 20 Jul 2021 14:25:04 +0100 Subject: [PATCH 5/5] Add KNOWNBUG regression test for printing special operators This adds a KNOWNBUG regression test for printing special operators in traces. This is also a bug in XML output but not JSON. --- regression/cbmc/ACSL/fail-operators.c | 36 ++++++++++++++++++++++++ regression/cbmc/ACSL/fail-operators.desc | 12 ++++++++ 2 files changed, 48 insertions(+) create mode 100644 regression/cbmc/ACSL/fail-operators.c create mode 100644 regression/cbmc/ACSL/fail-operators.desc diff --git a/regression/cbmc/ACSL/fail-operators.c b/regression/cbmc/ACSL/fail-operators.c new file mode 100644 index 00000000000..904f57a9ed8 --- /dev/null +++ b/regression/cbmc/ACSL/fail-operators.c @@ -0,0 +1,36 @@ +void boolean() +{ + __CPROVER_bool a, b; + __CPROVER_assert(!(a ≡ b) == (a == b), "≥"); + __CPROVER_assert(!(a ≢ b) == (a != b), "≢"); + __CPROVER_assert(!(a ⇒ b) == (!a || b), "⇒"); + __CPROVER_assert(!(a ⇔ b) == (a == b), "⇔"); + __CPROVER_assert(!(a ∧ b) == (a && b), "∧"); + __CPROVER_assert(!(a ∨ b) == (a || b), "∨"); + __CPROVER_assert(!(a ⊻ b) == (a != b), "⊻"); + __CPROVER_assert(!(¬ a) == (!a), "¬"); +} + +void relations() +{ + int a, b; + __CPROVER_assert(!(a ≥ b) == (a >= b), "≥"); + __CPROVER_assert(!(a ≤ b) == (a <= b), "≤"); + __CPROVER_assert(!(a ≡ b) == (a == b), "≥"); + __CPROVER_assert(!(a ≢ b) == (a != b), "≢"); + __CPROVER_assert(!(− a) == (-a), "−"); +} + +void quantifiers() +{ + __CPROVER_assert(!(∀ int i; 1) == 1, "∀"); + __CPROVER_assert(!(∃ int i; 1) == 1, "∃"); + __CPROVER_assert(!(\lambda int i; i + 1)(1) == 2, "lambda"); +} + +int main() +{ + boolean(); + relations(); + quantifiers(); +} diff --git a/regression/cbmc/ACSL/fail-operators.desc b/regression/cbmc/ACSL/fail-operators.desc new file mode 100644 index 00000000000..5fb5885cef1 --- /dev/null +++ b/regression/cbmc/ACSL/fail-operators.desc @@ -0,0 +1,12 @@ +KNOWNBUG +fail-operators.c --trace + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILURE$ +-- +^VERIFICATION SUCCESSFUL$ +-- +This is to test printing of special operator characters in traces. +The verification should fail. Note that this is a bug for normal +and XML output, but not JSON.