Remove XFAIL test.opt files for passing tests #108 #327

spanners · 2020-01-14T18:27:50Z

tests/attrib_size_object/test.out
tests/attrib_size_object/test.opt
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
tests/record_extension/test.opt
tests/record_extension/test.out
tests/representation_clause_component_size_change/test.opt
tests/representation_clause_component_size_change/test.out
tests/size_attribute_clause/test.opt
tests/size_attribute_clause/test.out
tests/size_integer_and_objects/test.opt
tests/size_integer_and_objects/test.out
Remove test.opt file and add the test.out output for each passing test

martin-cs

Looks good apart from the gotcha that I didn't warn you about.

@chrisr-diffblue and @tjj2017 : your thoughts on unsupported features in "passing" test cases?

martin-cs · 2020-01-15T22:05:13Z

testsuite/gnat2goto/tests/attrib_size_object/test.out

@@ -0,0 +1,15 @@
+Standard_Output from gnat2goto object_size:
+----------At: Process_Declaration----------
+----------size clause not applied by the front-end----------


Although the tests pass, this still has an unsupported feature so I don't think it should pass.

martin-cs · 2020-01-15T22:06:26Z

testsuite/gnat2goto/tests/record_extension/test.out

@@ -0,0 +1,14 @@
+Standard_Output from gnat2goto record_init:
+----------At: Do_Derived_Type_Definition----------
+----------record extension unsupported----------


Again, I don't think we should have unsupported features in the expected test results.

martin-cs · 2020-01-15T22:06:48Z

testsuite/gnat2goto/tests/representation_clause_component_size_change/test.out

@@ -0,0 +1,15 @@
+Standard_Output from gnat2goto test:
+----------At: Process_Declaration----------
+----------Having component sizes be different from the size of their underlying type is currently not supported----------


martin-cs · 2020-01-15T22:07:25Z

testsuite/gnat2goto/tests/size_attribute_clause/test.out

@@ -0,0 +1,70 @@
+Standard_Output from gnat2goto check_size:
+----------At: Process_Declaration----------
+----------size clause not applied by the front-end----------


Another one.

martin-cs · 2020-01-15T22:10:53Z

testsuite/gnat2goto/tests/size_integer_and_objects/test.out

-| Include the exact command that you entered.                              |
-| Also include sources listed below.                                       |
-+==========================================================================+
+Standard_Output from gnat2goto check_size:


I think it is good to update this and remove the crash but I would prefer not having unsupported features in the golden, expected results.

Looks like this test.out still contains the "unsupported feature" report (below)?

Oops - missed that one. Should be fixed now by 2d836e0

chrisr-diffblue · 2020-01-17T13:59:56Z

@martin-cs - From a purist point of view, I'd agree that having no "missing feature" reports in the expected output of regression tests is probably the way to go, pragmatically having tests run and xfail doesn't provide us a lot of information. One strategy that might be worth exploring is to see if it's possible to split any of these tests so that the part of the test that would pass is in one test, and the part that gives the "missing feature" report is in a separate, XFAIL'ed test. That sort of gets the best of both worlds, but I also fully expect some of the tests won't be able to be split like that.

chrisr-diffblue · 2020-01-17T14:01:35Z

Either way, it might be worth splitting the current single commit into two commits - one commit containing just the tests that cleanly pass with no missing feature reports, and one commit for however the tests with missing feature reports is handled. That would mean the commit history would contain some documentation about the handling of the two different cases.

spanners · 2020-01-20T12:37:18Z

@chrisr-diffblue

and one commit for however the tests with missing feature reports is handled

is this 'however' decided? i.e. what should I do to handle the tests with missing feature report?

martin-cs · 2020-01-20T14:51:38Z

@spanners / @chrisr-diffblue I am open to suggestions on the status of tests with unsupported features. I feel like they shouldn't just pass. Having them XFAIL is my preference I think but I can see an argument for passing but having the unsupported feature message in the expected results so that when it is fixed the test 'fails' and needs correcting.

Are there any existing tests that pass with unsupported features?

martin-cs · 2020-01-20T14:53:19Z

I also agree with the two commits approach. Let's get the 'definitely working with all features supported' cases merged ASAP.

spanners · 2020-01-20T18:45:00Z

I also agree with the two commits approach. Let's get the 'definitely working with all features supported' cases merged ASAP.

I have created commit ce32931 which has the 'definitely working with all features supported' version.

chrisr-diffblue · 2020-01-21T10:42:42Z

testsuite/gnat2goto/tests/size_integer_and_objects/test.out

+[check_size.assertion.1] line 30 assertion Integer (Var_T_1) + Integer (Var_T_2) = 70: SUCCESS
+[check_size.assertion.2] line 34 assertion Var_Size_1 + Var_Size_2 = 30: SUCCESS
+[check_size.assertion.3] line 37 assertion Var_U8 + 1 = 0: SUCCESS
+VERIFICATION SUCCESSFUL


Really minor nit pick - this file is ending without a newline. We typically make sure files do end with a newline character and Gituhub will highlight this as it has here.

But this is the test.out file... I don't believe I have control over whether the file ends with a newline character or not. Do you know how I'd fix this (if possible)?

I think the diffing against the test.out expected output is flexible on the newline front, so you should be able to manually add the newline. Most of us here have our editors set to always add a newline at the end. Of course, if adding a newline causes the test matching to complain, then please consider me corrected :-)

chrisr-diffblue

Looks good - many thanks for doing what is a rather tedious task. Much appreciated!

spanners · 2020-01-21T11:25:26Z

I have no idea why the build is failing - I can't reproduce the diffs on my local machine when running the gnat2goto python testsuite.py command

chrisr-diffblue · 2020-01-21T11:27:12Z

Do you have an up-to-date CBMC submodule checked out and rebuilt? There were some changes that went into CBMC in December that change the sort order of the assertion messages.

chrisr-diffblue · 2020-01-21T17:39:55Z

@spanners - I just remebered that this sorting order may be affected by UNIX Locale settings - I think CI is running with LC_ALL=posix, so could you try running your local tests with LC_ALL=posix and see if that changes the results?

chrisr-diffblue · 2020-01-21T18:13:05Z

Actually, we've just found a small bug in CBMC and how it sorts it's output. We'll get that fixed and update the submodule, and we'll ping you once thats in.

chrisr-diffblue · 2020-01-22T13:47:51Z

Once #330 is merged, hopefully the ordering issues will go away from the regression tests :-) Note that that PR includes a bump of the CBMC submodule, so after updating/rebasing your source tree you will need to ensure the submodule has updated, and then rebuild CBMC.

thk123 · 2020-01-22T14:31:35Z

@spanners #330 is now merged which should fix your ordering problem on CI.

thk123 · 2020-01-23T09:11:17Z

testsuite/gnat2goto/tests/address_clause/test.out

@@ -18,6 +18,6 @@ N_Attribute_Definition_Clause "address" (Node_Id=2295) (source,analyzed)
 Entity = N_Defining_Identifier "var_addr_2" (Entity_Id=2282)
 Check_Address_Alignment = True

-[address_clause.assertion.2] line 12 assertion Var_Addr_1 + Var_Addr_2 = 3: SUCCESS


I'm confused why this change is showing up, when the exact same change is made in #330: https://github.com/diffblue/gnat2goto/pull/330/files#diff-b450147fb1fc8092f271746d6b36256e but I suppose it doesn't matter

I think it is simply that it is based on an old commit of master. If you rebase first, your commit will be a little smaller, but I don't mind either way

Yeah, I think this should be rebased so that the PR is against the newest commit of master - though possibly in Spanners defence, I did have a PR recently (in a different Github repo) where even though I'd rebased my code, force pushed it to the PR, etc - the PR was still showing the old version. In that instance, I changed the commit message slightly and then did another force push, and that seemed to be enough to get the PR showing the right thing. So @spanners - if you could double check you've done a fetch/rebase, and try pushing again, it would be good to have this PR showing the proper diff.

#327 (comment) I think I've rebased now! Thanks for your patience.

* 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

chrisr-diffblue

Looks good - many thanks for pushing this through.

chrisr-diffblue · 2020-01-23T17:10:25Z

@martin-cs I think this is now just waiting for your re-review, when you get a moment.

martin-cs

Looks good to me!

spanners requested a review from martin-cs January 15, 2020 16:42

martin-cs requested changes Jan 15, 2020

View reviewed changes

spanners requested a review from martin-cs January 20, 2020 18:48

chrisr-diffblue reviewed Jan 21, 2020

View reviewed changes

chrisr-diffblue approved these changes Jan 21, 2020

View reviewed changes

spanners requested review from chrisr-diffblue and martin-cs and removed request for martin-cs January 22, 2020 16:38

thk123 reviewed Jan 23, 2020

View reviewed changes

chrisr-diffblue approved these changes Jan 23, 2020

View reviewed changes

chrisr-diffblue assigned martin-cs Jan 23, 2020

martin-cs approved these changes Jan 28, 2020

View reviewed changes

martin-cs merged commit 5b6ecf8 into diffblue:master Jan 28, 2020

chrisr-diffblue mentioned this pull request Jan 30, 2020

Declare implicit array types #335

Merged

Remove XFAIL test.opt files for passing tests #108 #327

Remove XFAIL test.opt files for passing tests #108 #327

Uh oh!

Conversation

spanners commented Jan 14, 2020

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue commented Jan 17, 2020

Uh oh!

chrisr-diffblue commented Jan 17, 2020

Uh oh!

spanners commented Jan 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

martin-cs commented Jan 20, 2020

Uh oh!

martin-cs commented Jan 20, 2020

Uh oh!

spanners commented Jan 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

spanners commented Jan 21, 2020

Uh oh!

chrisr-diffblue commented Jan 21, 2020

Uh oh!

chrisr-diffblue commented Jan 21, 2020

Uh oh!

chrisr-diffblue commented Jan 21, 2020

Uh oh!

chrisr-diffblue commented Jan 22, 2020

Uh oh!

thk123 commented Jan 22, 2020

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue commented Jan 23, 2020

spanners commented Jan 20, 2020 •

edited

Loading

spanners commented Jan 20, 2020 •

edited

Loading