Skip to content

Conversation

allredj
Copy link
Contributor

@allredj allredj commented Jul 1, 2019

Some StringBuilder tests were marked as FUTURE and caused by https://github.com/diffblue/test-gen/issues/434.
This seems now fixed, so I moved the tests to the main StringBuilder.append tests and enabled them, but I added a --max-nondet-string-length 1000 option. Not sure whether these tests should always pass without the option.
@romainbrenguier do you think we can remove it (the tests don't fail locally without the option, but I'm worried they might at a later time)?

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@allredj allredj self-assigned this Jul 1, 2019
String s = sb.toString();
assert(s.equals("fg"));
}
public static void nondet(String stringArg, int intArg)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see where intArg is used

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not. Removed.

String s = sb.toString();
assert(s.equals("fg"));
}
public static void nondet(String stringArg, int intArg)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ the name suggest there should also be a det test

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The tests for deterministic inputs are in the StringBuilderAppend[01] folders.

@allredj allredj force-pushed the clean-up/enable-string-test branch from c8ec34b to 62ceb1b Compare July 2, 2019 09:58
--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.1"
^EXIT=10$
^SIGNAL=0$
\[.*assertion\.1\] .* line 9 .* FAILURE
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about the other two assertions?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm testing per-property, so the other assertions are checked in the two other desc files. Is that what you mean?

Copy link
Contributor Author

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 62ceb1b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/117650646

@allredj allredj merged commit b41cc10 into diffblue:develop Jul 2, 2019
@allredj allredj deleted the clean-up/enable-string-test branch July 2, 2019 14:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants