Skip to content
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.

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

Fix regression tests #611

Open
28 of 49 tasks
schuessf opened this issue Jan 10, 2023 · 0 comments
Open
28 of 49 tasks

Fix regression tests #611

schuessf opened this issue Jan 10, 2023 · 0 comments
Assignees

Comments

@schuessf
Copy link
Contributor

schuessf commented Jan 10, 2023

On the Nightly build 405 we had 320 failed regression tests. To improve our workflow we should avoid failures of regression tests in the future.

Issues with test-suites/verdicts:

Tests that succeed locally, but fail in Jenkins-Build:

Issues with AutomataLibraryRegressionTestSuite:

Issues with ReqCheckerRegressionTestSuite:

Other Issues:

  • PdrAutomizer: SIMPLIFY_QUICK does not support simplification with respect to context, should we use another simplification technique?
  • PdrAutomizer: UnsupportedOperationException: Solver returned unknown
  • recursive-CallABAB_incorrect.bpl (abstract interpretation): Looks like an actual unsoundness.
  • overflow.c: We currently do not add any in-range-assumptions for parameters. This can be unsound, if we are in library mode (i.e. the entry-method is not declared). Should we adapt this or is the library mode not important enough for us? An easy fix would be to always assume that the arguments are in range, but not sure, if this is desired.
  • Enum03-Unsafe.c: ClassCastException: class CEnum cannot be cast to class CPrimitive in TypeSizes.extractIntegerValue
  • Some Float tests with MathSAT (e.g. this): SMTLIBException: The CNF conversion does not support quantifiers
  • ctrans-float-round.c: unknown symbol: roundNearestTiesToAway (with two strategies); Problem with MathSAT?
  • float22_simplified.c, ctrans-float-union.c: Sort Array not declared
  • ctrans-float-union.c: The translation of unions is unsound.
  • SubwordAccess.c: Looks like an actual unsoundness, how should we proceed with that?
  • Bug_ProcedureDNF.c (LTL): Assertion error in "old" map elimination
  • Some tests of ChcRegressionTestSuite fail because of issues in TreeAutomizer or because external solvers (like Z3) time out.
  • LTLAutomizer: AssertionError: No corresponding entry node for exit node with procedure main
  • UpAndDownGlobalReals.bpl: AssertionError in SMTInterpol (Interpolator$MixedLAInterpolator::convert)
  • builtin_ffs.c (with bitvector settings): IllegalArgumentException: incompatible types LONG INT
  • structFlexibleArray01.c: NumberFormatException: For input string: "18446744073708317049"
  • flexible_array.c: Unsoundness with bitvector translation

Unsupported features:

  • SyntaxSupportMixedIntReal2.bpl: PolynomialRelation does not support mixed sorts. The problem is that we do not really support ranking functions for real variables, since most constants and variables created in the termination analysis have the sort int. Therefore we often create terms with inconsistent sorts.
  • multipleCallSuccessors-01.bpl: State has more than one call successor
  • C2BoogieRegressionTestSuite: All the failing tests are currently unsupported cases, do we want to keep those as regression tests?
  • Some tests of the RegressionTestSuite (e.g this) also fail, because we don't support a specific feature.
  • ConstArray.bpl: SMTLIBException: Const is only supported for infinite index sort (with three settings)
  • InParamRenaming.c: Issue with renaming parameters that are used in ACSL
  • NonterminatingForLoopSafe.c: Some settings don't support non-linear arithmetic, we could however just simplify this example, the intention would remain the same.

Tests fail with unknown/timeout:

  • Several SMT tests are too hard for the underlying solver and should not run in regression tests.
  • Most of the other tests (e.g. from RegressionTestSuite) simply always fail, because we say unknown or have a timeout (at least for some of the settings/toolchains). We should try to fix them and otherwise find a way to ignore these failures in the test result.
schuessf added a commit that referenced this issue Jan 13, 2023
schuessf added a commit that referenced this issue Jan 16, 2023
schuessf added a commit that referenced this issue Feb 6, 2023
Heizmann pushed a commit that referenced this issue Feb 8, 2023
schuessf added a commit that referenced this issue Feb 16, 2023
schuessf added a commit that referenced this issue Feb 21, 2023
Heizmann added a commit that referenced this issue Feb 22, 2023
A Boogie file is either safe or unsafe.

This reverts commit 86f7848.
schuessf added a commit that referenced this issue Feb 23, 2023
This makes the test pass for all settings, since it removes non-linear arithmetic.
schuessf added a commit that referenced this issue Feb 23, 2023
schuessf added a commit that referenced this issue Feb 27, 2023
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

No branches or pull requests

4 participants