From 2d836e0e56c80458063a182788a155e1eaf07e5f Mon Sep 17 00:00:00 2001 From: Simon Buist Date: Tue, 14 Jan 2020 17:58:57 +0000 Subject: [PATCH] Remove XFAIL test.opt files for passing tests #108 * tests/deferred_constant_use/test.opt * tests/deferred_constant_use/test.out * tests/enum_symbols_range_constraint_assignment/test.opt * tests/enum_symbols_range_constraint_assignment/test.out * tests/packages/test.opt * tests/packages/test.out Remove test.opt file and add the test.out output for each passing test * tests/size_integer_and_objects/test.opt * tests/size_integer_and_objects/test.out Remove test.out and add newline to end of test.opt --- .../tests/deferred_constant_use/test.opt | 1 - .../tests/deferred_constant_use/test.out | 4 +--- .../test.opt | 1 - .../test.out | 1 + testsuite/gnat2goto/tests/packages/test.opt | 1 - testsuite/gnat2goto/tests/packages/test.out | 3 +++ .../tests/size_integer_and_objects/test.opt | 2 +- .../tests/size_integer_and_objects/test.out | 19 ------------------- 8 files changed, 6 insertions(+), 26 deletions(-) delete mode 100644 testsuite/gnat2goto/tests/deferred_constant_use/test.opt delete mode 100644 testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt delete mode 100644 testsuite/gnat2goto/tests/packages/test.opt create mode 100644 testsuite/gnat2goto/tests/packages/test.out delete mode 100644 testsuite/gnat2goto/tests/size_integer_and_objects/test.out diff --git a/testsuite/gnat2goto/tests/deferred_constant_use/test.opt b/testsuite/gnat2goto/tests/deferred_constant_use/test.opt deleted file mode 100644 index b585e32d0..000000000 --- a/testsuite/gnat2goto/tests/deferred_constant_use/test.opt +++ /dev/null @@ -1 +0,0 @@ -ALL XFAIL cbmc returns failed verification (calling function without body) diff --git a/testsuite/gnat2goto/tests/deferred_constant_use/test.out b/testsuite/gnat2goto/tests/deferred_constant_use/test.out index 1e3c7b901..15a034aff 100644 --- a/testsuite/gnat2goto/tests/deferred_constant_use/test.out +++ b/testsuite/gnat2goto/tests/deferred_constant_use/test.out @@ -1,4 +1,2 @@ -[assertion.1] Range Check: SUCCESS -VERIFICATION SUCCESSFUL - +[inc.assertion.1] line 4 Ada Check assertion: SUCCESS VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt deleted file mode 100644 index 2c44c9bfb..000000000 --- a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt +++ /dev/null @@ -1 +0,0 @@ -ALL XFAIL symex is crashing at the assignment because of wrong code generation. diff --git a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out index c0794a357..e9643f394 100644 --- a/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out +++ b/testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out @@ -1 +1,2 @@ +[range_constraint.assertion.1] line 15 assertion Value = CALIBRATION_FAIL: SUCCESS VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/packages/test.opt b/testsuite/gnat2goto/tests/packages/test.opt deleted file mode 100644 index b585e32d0..000000000 --- a/testsuite/gnat2goto/tests/packages/test.opt +++ /dev/null @@ -1 +0,0 @@ -ALL XFAIL cbmc returns failed verification (calling function without body) diff --git a/testsuite/gnat2goto/tests/packages/test.out b/testsuite/gnat2goto/tests/packages/test.out new file mode 100644 index 000000000..e266f597b --- /dev/null +++ b/testsuite/gnat2goto/tests/packages/test.out @@ -0,0 +1,3 @@ +[packages.assertion.1] line 6 assertion Test.Double (1) = 2: SUCCESS +[double.assertion.1] line 6 Ada Check assertion: SUCCESS +VERIFICATION SUCCESSFUL diff --git a/testsuite/gnat2goto/tests/size_integer_and_objects/test.opt b/testsuite/gnat2goto/tests/size_integer_and_objects/test.opt index eff20f6ec..9f1bb3617 100644 --- a/testsuite/gnat2goto/tests/size_integer_and_objects/test.opt +++ b/testsuite/gnat2goto/tests/size_integer_and_objects/test.opt @@ -1 +1 @@ -ALL XFAIL gnat2goto fails when Size representation clause applied to standard types and their derivations or to objects. \ No newline at end of file +ALL XFAIL gnat2goto fails when Size representation clause applied to standard types and their derivations or to objects. diff --git a/testsuite/gnat2goto/tests/size_integer_and_objects/test.out b/testsuite/gnat2goto/tests/size_integer_and_objects/test.out deleted file mode 100644 index bb8f6db13..000000000 --- a/testsuite/gnat2goto/tests/size_integer_and_objects/test.out +++ /dev/null @@ -1,19 +0,0 @@ -+===========================GNAT BUG DETECTED==============================+ -| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:4673 | -| Error detected at check_size.adb:1:11 | -| Please submit a bug report; see https://gcc.gnu.org/bugs/ . | -| Use a subject line meaningful to you and us to track the bug. | -| Include the entire contents of this bug box in the report. | -| Include the exact command that you entered. | -| Also include sources listed below. | -+==========================================================================+ - -Please include these source files with error report -Note that list may not be accurate in some cases, -so please double check that the problem can still -be reproduced with the set of files listed. -Consider also -gnatd.n switch (see debug.adb). - -check_size.adb - -compilation abandoned