Skip to content

v0.1.18

Pre-release
Pre-release
Compare
Choose a tag to compare
@danieldietsch danieldietsch released this 23 Jun 08:24
· 15293 commits to dev since this release
v0.1.18
22cb65e

Features

  • reappropriate CFGConsoleOut plugin: now prints IIcfg to console

Bugfixes

C to Boogie Translation

  • fixed error "Type missmatch on in-parameters" during C to Boogie translation by using a boogie visitor to decide similarity between function declaration and function definition (does not yet support where-clauses) (closes #186)
  • fixed an error in CACSL2BoogieBacktranslator that resulted in old-var creation were no oldvars should have been (closes #187)
  • fix merge bug in CLocation (wrong merging if one or both of the nodes is null)
  • introduce workaround that adds bvadd for all integer datatypes

Kojak

  • fix multiple assertion errors

Misc

  • fixed various bugs in loop acceleration FastUPR
  • fix TransformedIcfgBuilder: do not convert summaries to internal transitions if summaries have implementations (drop them instead)
  • fixed bug were Util.checkSat() would call pop on dead solvers
  • BoogiePreprocessor now crashes and displays a helpful error message if there is no Boogie model present (closes #193)
  • ReqAnalyzer parser error messages are now shown as expected and not only on stderr
  • removed special handling of true/false state in NondeterministicInterpolantAutomaton. This was probably also a bug in RefineBuchi in mode EagerNondeterminism because the old states were ignored.
  • do not blame SMT solver if Ultimate killed solver because of general timeout
  • bugfix live variables
  • bugfix: cyclomatic complexity, use balls instead off SCCs
  • bugfix: pass old abstraction
  • bugfix: support empty automaton
  • bugfix: mathsat settings
  • bugfix: use PredicateFactoryResultChecking instead of PredicateFactoryRefinement
  • various bugfixes in TreeAutomizer
  • timeout handling in trace checker

Plumbing

Testing

  • moved summaries and logs to library-ultimatetest
  • add method boolean createLogs() to AbstractRegressionTestSuite (overwrite and return true if you want logs for local execution of regression test cases)
  • updated regression test settings for float tests
  • allow more error path names for regression tests that use error paths

Abstract Interpretation

  • introduce useHierachicalPre() in IAbstractDomain that decides whether hierachical pre states or states before leaving are used with a post operator
  • VPDomain overrides useHierachicalPre() (closes #178)

ReqAnalyzer

  • remerge various improvements to Library-srParse (parsing of .req files): Can now handle Boogie expressions instead of only atomic propositions
  • allow specifying IDs for requirements
  • add new requirements pattern

Automata library

  • automata difference: check for simple nondeterminism before useless computations

Misc

  • do not unlet term
  • show warning if simplification was expensive
  • rename BenchmarkResult to StatisticsResult
  • local simplification for store and select
  • Improve performance of "Reachbility Hoare Triple Checks"

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