Skip to content

Tests exhibiting performance problems with floating point equalities #4338

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Mar 7, 2019
Merged

Tests exhibiting performance problems with floating point equalities #4338

merged 1 commit into from
Mar 7, 2019

Conversation

@peterschrammel
Copy link
Member

@peterschrammel peterschrammel commented Mar 6, 2019

See #4337.

  • 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.

@peterschrammel peterschrammel mentioned this pull request Mar 6, 2019
Open
tautschnig
tautschnig approved these changes Mar 6, 2019
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

This is failing CI as explained below, but otherwise ready to be merged.

regression/cbmc/Float-equality1/main.c Outdated
double x = a, y = b, z = c;
assert(!(z > x + y) );
#else
assert(!(c > a + b) );
Copy link
Collaborator

@tautschnig tautschnig Mar 6, 2019

Choose a reason for hiding this comment

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

This test isn't clang-format clean. (Opening { on new line, no space before ) (twice).)

regression/cbmc/Float-equality1/test_no_equality.desc Outdated
@@ -0,0 +1,9 @@
CORE
Copy link
Collaborator

@tautschnig tautschnig Mar 6, 2019

Choose a reason for hiding this comment

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

The SMT-backend is broken, and this test again shows this. Add broken-smt-backend. Preferably also to the KNOWNBUG test.

@peterschrammel peterschrammel force-pushed the floating-point-timeout branch from 9c7170f to b3c9ade Compare March 7, 2019 08:40
allredj
allredj reviewed Mar 7, 2019
View reviewed changes
Copy link
Contributor

@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: b3c9ade).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103505025

@tautschnig tautschnig merged commit 616a4b3 into diffblue:develop Mar 7, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnig tautschnig tautschnig approved these changes

+1 more reviewer

@allredj allredj allredj left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@peterschrammel peterschrammel

Labels

Tests

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@peterschrammel @tautschnig @allredj