Skip to content

v0.1.10

Pre-release
Pre-release
Compare
Choose a tag to compare
@danieldietsch danieldietsch released this 05 Apr 06:52
· 16205 commits to dev since this release
v0.1.10
3561117

Features

C translation

  • add support for "division by zero"-check for Float types (closes #137)
  • add support for Float types on heap (pointers, globals)
  • add support for __builtin_bswap32 and __builtin_bswap64 via overapproximation

Automata library

  • added option to unify objects in AutomataScriptParser
    The states and letters in automata are not unified when parsed from a file. That means there are a lot of String duplicates, which wastes memory and can become a bottleneck for very large automata. Currently only nested word automata can be unified. Tests have shown that there is no impact in runtime for small automata. The setting is not the default for now.
  • NwaApproximateXsimulation gets flag to ignore successors
    With this optinal flag (default true) set to false, successors are not considered. What remains is optional separation of accepting and non-accepting states and states with different symbols.

Taipan / Abstract Interpretation

  • new HoareTripleChecker based on abstract interpretation post operator (closes #109)
  • use PathProgram instead of NWAPathProgramTransitionProvider in Taipan's path program analysis (closes #82)

Statistics

  • count number of variables in abstract states
  • more/better runtime information for some minimization operations
  • add solver statistics inside statistics method
  • only compute minimization statistics if result is available

Misc

  • when using --help with CLI, print core and controller options even if no toolchain is supplied
  • improved RewriteNotEquals option of BlockEncoding
  • ICFG transformation ModuloNeighborTransformation is now exact (no overapproximation)
  • PathProgram now constructs its own symbol table that only contains symbols present in the path program

Bugfixes

Taipan / Abstract Interpretation

  • fix isSubsetOf in Octagon domain by handling different variable orders (permutated matrices) correctly
  • fix merge bug in octagon domain by correctly considering isBottom()
  • fix isSubsetOf in AbstractMultiState by considering isBottom() correctly
  • fix toLogString bug
  • fix AbsIntPredicate in automata problem by ensuring that BasicPredicate equals() function is symmetric for all subclasses; this also implies that only the hashcode of a BasicPredicate defines equality (closes #141)
  • fix bug in call handling of AbsIntHoareTripleChecker
  • fix bug that prevented using compound domain with just one domain
  • fix bug that produced nullpointer exception instead of timeout in certain situations
  • fix non-terminating loop in getInnermostArrayValueSort()
  • fix statistics generation during fixpoint computation

C translation

  • fix decimal form conversion in multi-assignments (closes #140)
  • bugfix: indicate need for floating types
  • bugfixes: order of parameters, bitlength, no indices for fp
  • bugfix: support integer and floating in SingleBitprecise
  • bugfix: pointer array does not represent primitives
  • bugfix for code that puts unions on heap

Automata library

  • add timeout check to FullMultipebbleGameAutomaton
  • add extensive timeout checks to NestedWordAutomatonReachableStates
  • do not report duplicate statistics in old simulation
  • fix: FullMultipebble simulation readout wrong in certain combination
    If the asymmetric preprocessing is used instead the symmetric postprocessing, the simulation was not correctly obtained. Those pairs for which (p, q) was an initial pair but (q, p) was not, the method claimed that p ~ q.
  • bugfix: missing spoiler winning sink selfloop

Misc

  • log ignored exceptions in TraceAbstractionRefinementEngine
  • fix term to transformula conversion in SBE
  • only rewrite equalities of ints and reals (<, <=, >, >= are not defined on arrays, bitvectors and floats need more work)
  • use Exception instead of assert in pathinvariants (without -ea we obtained wrong results)
  • escape illegal sequences in backtranslation
  • bugfixes in backtranslation of quantified formulas
  • fix: sort enum alphabetically, otherwise CSV concatenation does not work

Plumbing

Taipan / Abstract Interpretation

  • throw all unknown exceptions in Taipan instead of supressing them
  • use IcfgEdge and getLabel() in multiple places in abstract interpretation
  • remove dependency on BoogieSymboltable and remove ISymbolTableAdapter workaround

Testing

  • add regression tests for Taipan
  • add regression tests for tree automaton operations
  • add regression tests for Ultimate's handling of floats on the heap
  • print assertion status (-ea or not) in IncrementalLogWithVMParameters
  • new TestResultDecider SomeVerificationResultTestResultDecider succeeds if there is any verification result

Misc

  • add toNnf to SmtUtils (analogously to toDnf) and add NNF to IcfgTransformer (analogously to DNF)
  • add additional assert to BasicCegarLoop (automaton states should have identical types)
  • add auto-generated visitors and transformers to Boogie AST
  • add infrastructure for asserts in auto-generated AST code
  • add asserts to Boogie AST that check identifier Strings for validity
  • add OS_IS_WINDOWS to CoreUtils
  • use windows detection to avoid using cvc4 on windows in Taipan
  • new data structure LinkedHashRelation
  • support for dumping interprocedural path programs as Boogie code
  • add support for pretty-printing ASTType
  • added new shrinker to automatondeltadebugger
  • added IPartition to replace UnionFind in automaton minimization
  • remove floating point rounding mode
  • all random automata library operations get a seed
  • moved Rers2016 benchmarks to new benchmark repository ultimate-pa/ultimate-benchmarks.

Known Issues

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

Assets 5
Loading