Improvements to the unit tests directory #1111

thk123 · 2017-07-10T13:53:39Z

I developed some utilities and fixed the Makefile for the unit directory. Rather than wait for that work to make its way to master, here are those improvements as they may be useful to others.

Would like some feedback on the directory structure - I wanted to keep utility code separate from the unit tests themselves. If people agree, I can add this to the coding standard.

tautschnig · 2017-07-10T14:16:50Z

unit/src/symbol-table/symbol_table_util.cpp

+/// \param name: The name of the symbol.
+/// \param type: The type of the symbol.
+/// \return The symbol that has been created.
+symbolt symbol_table_utilt::create_basic_symbol(


Wouldn't this make for a good constructor in symbolt?

I am happy to do this, but reasons why I didn't:

I thought it was a bit of an ad-hoc collection of flags that seems very useful when you want succinct tests, but not in general.

I don't understand all the flags in symbolt. I don't think this is a problem for tests, but seems more risky to introduce into the general codebase (someone might see this constructor, use it but in some unrelated part of the code, the missing flag could cause some nasty problems (not an issue with unit tests since only test isolated sections of the code).

Take a look at various *_symbolt classes defined in symbol.h - I'd see nothing wrong in adding one more, which really must be a useful one as otherwise you wouldn't have factored it out into a new function. (This would also address the namespace discussion in this PR.)

owen-mc-diffblue · 2017-07-10T14:08:56Z

unit/src/expr/require_expr.cpp

+
+/// \file
+/// Helper functions for requiring specific expressions
+/// If the expression is of the wrong type, through a CATCH exception


through -> throw

reuk

Looks good to me. Not sure about the namespace-esque usage of a class. I would prefer to use a proper namespace, as this code has confusing/misleading semantics.

reuk · 2017-07-10T14:30:03Z

unit/src/symbol-table/symbol_table_util.h

+
+#include <util/symbol.h>
+
+class symbol_table_utilt


Pretty sure this should be a namespace.

You're quite right - @peterschrammel would this be an acceptable use of a namespace?

thk123 · 2017-07-10T16:20:40Z

@tautschnig Added as an additional constructor to auxilary_symbolt as it had the flags I needed.

@reuk This "resolves" the issue of namespace vs class.

reuk · 2017-07-10T16:26:58Z

Sorry to be awkward but I think require_exprt should probably be a namespace too.

tautschnig · 2017-07-10T16:29:36Z

Sorry to be awkward but I think require_exprt should probably be a namespace too.

As much as I'd otherwise argue against namespaces: unit tests may be a good use of them to separate out code that is exclusively of use for testing purposes.

thk123 · 2017-07-10T16:30:20Z

unit/src/expr/require_expr.h

+
+#include <util/std_expr.h>
+
+class require_exprt


@peterschrammel would it be OK as suggested by @reuk for me to make this into a namespace, I know they are forbidden by coding standard but I don't really understand why.

thk123 · 2017-07-10T17:09:19Z

As discussed in #1070 rather than LIBS it should be OBJ which will mean the dependency doesn't have to be manually managed. It also will fix the rebuild issue since already depends on OBJ. Will update this PR accordingly.

thk123 · 2017-07-10T17:21:24Z

@reuk @peterschrammel @tautschnig I have added a commit swapping require_exprt to be a namespace, I can either squash it or drop it once the decision is made.

peterschrammel

Otherwise looks good to me.

peterschrammel · 2017-07-10T19:32:54Z

unit/src/expr/require_expr.h

+
+#include <util/std_expr.h>
+
+namespace require_exprt


Not sure the t suffix is useful then.

Requires a nolint or a change in the linting rules.

thk123 · 2017-07-14T09:30:55Z

@peterschrammel Changes applied and namespace change squashed.

tautschnig · 2017-07-17T21:54:12Z

@thk123 Would it be possible to rebase this one and make all CI tests pass? It seems the need for linking adjustments in unit/Makefile is starting to show in other branches/PRs as well. Thanks!

thk123 · 2017-07-18T09:49:25Z

@tautschnig I think I've modified the Makefile in such a way it should work, but I'd appreciate you having another look at it as quite different to before (left in a separate commit for ease of review: da6e6a0 I'll squash once reviewed)

tautschnig

Looks good to me!

tautschnig · 2017-07-18T10:32:58Z

@thk123 Thanks a lot for all the updates; please squash and maybe you can then poke @kroening for a merge?

Previously the order of the libraries in LIB would effect whether the unit tests compiled. Use OBJ rather than LIBS to ensure the --start-group/--end-group flags are used in linking. Previously, if a file in CProver changed, though the libraries would be rebuilt, the unit tests wouldn't be relinked against the new library, meaning you would get out of date binaries. This change ensures that the link process is rerun if any of the libraries are rebuilt. Adding dependency to cprover libs for other unit executables

Use namespace rather than class with static functions as more semantically correct.

In turns the error return state into a CATCH exception so the test will fail without cluttering tests with checks on the flag when it is just setup code for the actual test.

The auxilary function had the same flags requried for the test, so added a utility constructor that allows specifying of name and type.

thk123 · 2017-07-18T12:47:07Z

@kroening All fixed and squashed, could I get a merge as I understand from @tautschnig that the lack of Makefile changes is causing other issues.

thk123 force-pushed the feature/unit-test-utility branch from dc1c7ed to 3a0f1bd Compare July 10, 2017 13:59

tautschnig reviewed Jul 10, 2017

View reviewed changes

owen-mc-diffblue approved these changes Jul 10, 2017

View reviewed changes

reuk approved these changes Jul 10, 2017

View reviewed changes

thk123 force-pushed the feature/unit-test-utility branch 2 times, most recently from 8e627a0 to 02fe8bd Compare July 10, 2017 16:19

thk123 commented Jul 10, 2017

View reviewed changes

thk123 mentioned this pull request Jul 10, 2017

Fixing simplification of LHS #1070

Merged

thk123 force-pushed the feature/unit-test-utility branch from 02fe8bd to ddb728f Compare July 10, 2017 17:17

peterschrammel reviewed Jul 10, 2017

View reviewed changes

thk123 mentioned this pull request Jul 13, 2017

[depends: #708] Write Stack for storing pointer values #1120

Closed

thk123 force-pushed the feature/unit-test-utility branch from 020dfd7 to 423bc70 Compare July 14, 2017 09:30

tautschnig mentioned this pull request Jul 17, 2017

Array initialization with a non-array is expected to fail #131

Merged

tautschnig added the bugfix label Jul 17, 2017

thk123 force-pushed the feature/unit-test-utility branch 2 times, most recently from ee9af0f to 1520cf9 Compare July 18, 2017 09:45

tautschnig approved these changes Jul 18, 2017

View reviewed changes

thk123 added 4 commits July 18, 2017 11:51

Added utility functions for checking expressions

b5c55b3

Use namespace rather than class with static functions as more semantically correct.

Adding pretty printer to main file

0047733

Added utility class to convert strings into expressions

3185028

In turns the error return state into a CATCH exception so the test will fail without cluttering tests with checks on the flag when it is just setup code for the actual test.

Added constructor to auxilary symbol instead of a helper function

e3f8d4a

The auxilary function had the same flags requried for the test, so added a utility constructor that allows specifying of name and type.

thk123 force-pushed the feature/unit-test-utility branch from 1520cf9 to e3f8d4a Compare July 18, 2017 10:52

kroening merged commit 6fbd1cf into diffblue:master Jul 18, 2017

thk123 deleted the feature/unit-test-utility branch July 19, 2017 08:59

tautschnig mentioned this pull request Jul 20, 2017

goto-gcc removes CPROVER macros for native gcc #1108

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improvements to the unit tests directory #1111

Improvements to the unit tests directory #1111

thk123 commented Jul 10, 2017

tautschnig Jul 10, 2017

thk123 Jul 10, 2017

tautschnig Jul 10, 2017

owen-mc-diffblue Jul 10, 2017

reuk left a comment

reuk Jul 10, 2017

thk123 Jul 10, 2017

thk123 commented Jul 10, 2017

reuk commented Jul 10, 2017

tautschnig commented Jul 10, 2017

thk123 Jul 10, 2017

thk123 commented Jul 10, 2017

thk123 commented Jul 10, 2017

peterschrammel left a comment

peterschrammel Jul 10, 2017

peterschrammel Jul 10, 2017

thk123 commented Jul 14, 2017 •

edited

Loading

tautschnig commented Jul 17, 2017

thk123 commented Jul 18, 2017

tautschnig left a comment

tautschnig commented Jul 18, 2017

thk123 commented Jul 18, 2017 •

edited

Loading

Improvements to the unit tests directory #1111

Improvements to the unit tests directory #1111

Conversation

thk123 commented Jul 10, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

reuk left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Jul 10, 2017

reuk commented Jul 10, 2017

tautschnig commented Jul 10, 2017

Choose a reason for hiding this comment

thk123 commented Jul 10, 2017

thk123 commented Jul 10, 2017

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Jul 14, 2017 • edited Loading

tautschnig commented Jul 17, 2017

thk123 commented Jul 18, 2017

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig commented Jul 18, 2017

thk123 commented Jul 18, 2017 • edited Loading

thk123 commented Jul 14, 2017 •

edited

Loading

thk123 commented Jul 18, 2017 •

edited

Loading