Skip to content

v0.1.20

Pre-release
Pre-release
Compare
Choose a tag to compare
@danieldietsch danieldietsch released this 02 Aug 14:59
· 14271 commits to dev since this release
v0.1.20
1f2f176

Features

Change of default settings

  • logic for auxiliary solver becomes ALL
  • do not bring TransFormulas in CNF
  • ICFG does partial skolemization by default

Misc

  • support for computation of danger invariants in InvariantSynthesis plugin
  • optimization for auxiliary bitvector equality method
  • added entry and exit functions to violation witnesses (closes #113)
  • improve assertion order modulation in strategies that use them by counting already analyzed path programs and saving/logging trace hashes for debugging (closes #204)
  • new abstract interpretation domain SMTTheoryDomain - a domain based on predicate transformer and SMT solver calls.

Solver update

  • Now using MathSat5 nightly build 84cb666a6c83 (Jul 12 2017)

Bugfixes

  • various bugfixes, e.g. in TermVariableRenamer and LassoRankerStarter, renaming of variables to constants in some SMT operations,
  • fix backtranslation bug: if a procedure without implementation is called, replace the call/return with an fcall and avoid return statement shifting workaround; for C programs without explicit return, remove assertion (closes #205)
  • add support for expressions containing variables with array type in BoogiePreprocessor backtranslator and fix a bug where struct types where not treated as intended
  • fix bug in IcfgTransformer that lead to new return transitions being created before the corresponding call transition was created (closes #207)
  • fix IndexOutOfBounds exception in backtranslation (closes #209)
  • fix not considering AutomataScriptInterpreterOverallResult in overall result message (closes #6)
  • bugfix SSD quantifier elimination
  • fix Overapprox annotation being unmergeable (closes #189)
  • fix bug that lead to different .csv files during testing by using AbstractCegarLoop.Result in CodeCheck instead of redefining own enum (closes #200)

Plumbing

  • new data structure for an equivalence relation with a ternary membership status (equal, not equal, unknown)
  • use actual hierachical prestate in AbstractInterpretation soundness check instead of stateafterleaving
  • use monteverdi nexus oss repository proxy to prevent build breakage due to high load on eclipse p2 repositories
  • introduced IRankedLetter interface: every letter in a TreeAutomaton's alphabet now needs to have an explicit rank;
  • moved helper files for TreeAutomizer from modelcheckerutils/hornutil to its own library Library-TreeAutomizer
  • add new auxiliary method (distinct) to SmtUtils

Known Issues

  • README and Website usage instructions outdated (see #135)
  • Startup with generated binary ./Ultimate stalls if no X display is available
Assets 5
Loading