Skip to content

v0.1.12

Pre-release
Pre-release
Compare
Choose a tag to compare
@danieldietsch danieldietsch released this 08 May 12:21
· 15899 commits to dev since this release
v0.1.12
44fa4f4

Features

Taipan / Abstract Interpretation

  • Octagons now support arbitrarily ordered matrices for certain methods
  • Normalized expressions are now cached (along with various other helpers like call/return variable assignments)
  • Nonrelational domains and octagons now support bottom caching
  • Nonrelational domains and octagons now support old variables (still experimental, see #155)
  • AbsIntHoareTripleChecker is now used as a chain of Caching/SD/AbsInt/SMT HTCs
  • AbsInt now has its own predicate unifier that skips predicate simplification and uses AbsIntPredicates (CNF)
  • AbsInt now supports a simple weakening algorithm for path programs that retains inductive predicates, but removes variables (see #80)
  • new strategy LazyTaipan: use absint if all else fails
  • Taipan strategies now start with NON_INCREMENTALLY as assertion order
  • Taipan now uses full timeout for fixpoint computation instead of 20% of the remaining time

Website

  • updated automata library website
  • updated lasso ranker website

Misc

  • new SimplificationTechnique NONE
  • support backtranslation of array types also for ICFG mode
  • add option for simple partial skolemization of terms in ICFG builder
  • add statistics for error localization
  • use CVC4 in refinement engine with --rewrite-divk in order to support div and mod in AUFLIA
  • support HoenickeLindenmannOriginal also for floats
  • support acceleration of loops containing assertions (LA Woelfing)

Bugfixes

Taipan / Abstract Interpretation

  • fix statistics output: reduction value (is now 100 - remaining size)
  • fix: compound is bottom if any state is bottom, not if all states are bottom
  • fix bottom state bug in octagon domain: octstate should retain bottom flag during add/remove (closes #156)
  • fix: release incremental htc before checking subset inclusion
  • fix subset bug in abstract multi state: change ordinal order in SubsetResult and use max of individual states instead of min
  • fix release HTC lock even if timeout occurs
  • fix do not trigger assertion if isSubsetOf is none due to overapprox
  • fix nullpointer exception in IntervalDomainValue
  • fix bug in Octagon patch() method

Test framework

  • fix: if one test summary write fails, do not stop writing other summaries (also, print some error information)
  • fix: remove dependency to swt mistakenly added by someone, thus forcing JUnit-Plugin tests to start a GUI (closes #164)

Loop acceleration

  • Fix outVars for loop acceleration (LA Woelfing)
  • Fix some bugs in loop acceleration (LA Woelfing)

Misc

  • fix bug in BoogieNormalFormTransformer: rewriteNotEquals did also rewrite bools
  • fix complement operation of tree automata, added test for EmptinessCheck

Plumbing

Test framework

  • refactoring: unified creation of UltimateTestCase in all test suites
  • refactoring: introduce superclass BasetestLogfile for all ITestLogfile implementations
  • refactoring: move timeout information into UltimateRunDefinition
  • add IPreTestLog: A logtype that is generated before the test suite is executed
  • add new testresultdecider NoErrorAndTimeoutTestResultDecider
  • print paths in summaries always with "/"
  • provide z3 scriptor and mocks directly from UltimateMocks (fixing dependency problem in Icfgtransformertest)
  • add new prelog BenchexecRundefinitionGeneratorPreLog: writes .xml file in benchexec' benchmark format based on current test suite

Taipan / Abstract Interpretation

  • removed merge-operator from IAbstractDomain, added union and intersect methods to IAbstractState and use these instead
  • move synchronize() from IVariableProvider to AbsIntUtil
  • add factory method to AbstractMultiState and enforce AbstractMultiState to be a disjunction of normal states
  • new method IAbstractState.compact(): remove all unused variables from a state (used in AbsIntHTC, AbstractMultiState, Weakening)
  • new method OctMatrix.rearrange(): Eliminated use of BidirectionalMap, more efficient OctMatrix.copySelection()
  • refactoring: taipan strategies share new super class BaseTaipanRefinementStrategy

Automata library

  • refactoring of on-demand construction API
  • refactoring NWA
  • introduce new hierarchical predecessor-based lettersReturn method (more efficient)
  • added computation of relations for delayed simulation
  • added variable factory for SAT-based minimization

Loop acceleration

  • Use TransFormulaUtils.sequentialComposition() instead of custom implementation (LA Woelfing)

Misc

  • use nested iterator for more efficient iteration over entries of NestedMap2
  • restructure exception handling of TraceChecker
  • descend in similar subterms only once in ContainsQuantifier

Known Issues

README and Website usage instructions still outdated (see #135)

Assets 5
Loading