v0.1.19

Features

Automata Library

• added union operation
• added isFinite operation

Misc

• first working prototype of EQ domain with array support (see #159, #195)
• preliminary implementation of HeapSeparator in IcfgTransformation (see #197)
• preliminary support for error automata in Ultimate Automizer (see #182)
• support for new requirements pattern InitializationPattern: Allows to specify types of variables s.t. former atomic propositions are not atomic anymore
• totalize now supports nondeterministic automata
• unsat-core-free relevance computation now also for call and return

Bugfixes

TreeAutomizer

• fix to HCHoareTripleChecker (in order to fix generalization of interpolant automata in TreeAutomizer) some cleanup

Misc

• fix backtranslation of to_fp (closes #198)
• prevent multiple windows from appearing by not using a parent for the dialog (closes #196)
• fix: fault localization should compute error pre-/postcondition
• fix srParse test cases
• fix small bug in IcfgTransformerSequence: did not add return transitions last
• fix bug in icfgtransformation mapelimination: transform both transformulas of a return transition (also, be less verbose)
• fix bug in absint: futureicfg did check for wrong call/return types
• omit problematic simplifications for store and select
• various fixes for LA Mohr and LA Werner

Plumbing

• add new preferences MAP_ELIMINATION_NO_EQUALITY and MAP_ELIMINATION_EQUALITY to IcfgTransformation
• Hoare triple checkers are more modular
• add log levels to ILogger mock
• add IncrementalImplicationChecker
• Add more logging output for assertion orders
• explain relevance information in output

Known Issues

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

v0.1.18

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

v0.1.17

Features

• added support for equality in float-real approximation
• added support for float to int conversion in float-real approximation

Bugfixes

• recompiled z3 870017e without cpu-specific instructions
• bugfix: equality of real constants with different value representations

Plumbing

• rename statistic RUNTIME_TOTAL to RUNTIME_TOTAL_MS

Known Issues

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

v0.1.16

Bugfixes

• fix exception if branch encoders have unexpected length
• fix an error in loop acceleration woelfing were orphaned returns would be added after acceleration
• fix: take into account that succInternal() succCall() succReturn() may return null

Plumbing

• updated Z3 and MathSAT to their current version (see README for the actual versions) (closes #180)

Known Issues

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

v0.1.15

Features

• AutomataScript is now case-sensitive. Operations are named similar to Java in CamelCase (see #179)
• new MathSAT setting for .epf files and IRefinementStrategy
• add interactive verification prototype via various new plugins

Bugfixes

• fix solver crash because of bvadd with three arguments by translating to response unknown and adding ULTIMATE_VIOLATES_SMT_LIB_STANDARD_AND_SOLVER_COMPLAINS to TraceCheckReasonUnknown (workaround for #185)
• fix StackOverflowException in LA Woelfing
• fix witness xml header: xmlns="http://graphml.graphdrawing.org/xmlns" is correct but incomplete; full boilerplate should be xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://graphml.graphdrawing.org/xmlns http://graphml.graphdrawing.org/xmlns/1.0/graphml.xsd" ( 2d24b14 ) (fixes #112)
• fix build problems by specifying relevant resources for executing builder (closes #167)
• fix API usage: Core should call parseAST(Files[]) for multiple input files that are paresable by the same parser (closes #172)
• fix NPE during toolchainstorage.clear(): do not store null in the storage
• fix compound domain unsoundness (disjunctive compound domain call bug) by using solver to check for inconsistent state (workaround)

Plumbing

Automata Library

• refactoring automata library: do not store alphabet in three sets, but introduce an visibly pushdown alphabet object ( e4bb2b1 )
• remove AA_Accept which is just a copy of AA_Accepts
• add NCSB-based buchi inclusion operation
• minor change in INwaSuccessorStateProvider API
• let BuchiComplementNCSB use new on-demand API
• let SetOfStates provide emtpy stack state
• let BuchiComplementFKV implement new on-demand API

Misc

• added generalized version of IPredicate and TransFormula
• make PredicateTransformer domain-independent for all post operations via IDomainSpecificOperationProvider
• add getConstants() for predicates
• remove confusing field (fixes #184)
• use SmtSortUtils throughout Ultimate (closes #152)
• try to avoid any INFO logging before the controller takes over
• add Library-InteractiveModel to ultimate common features
• extend TransformedIcfgBuilder s.t. it can also be used to add new transformulas to the icfg (not only transform existing ones)
• refactoring: support several interactive modules in PMaxSAT solver - added new interface for interactive module - former TransitivityGeneralMaxSatSolver became InteractiveMaxSatSolver which supports several modules
• various refactorings in CEGAR loops (towards error automaton, see #182)

Known Issues

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

v0.1.14

Features

write originfile to witnesses (close #166)

Known Issues

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

v0.1.13

Features

• limited support for #line directive (not yet for ACSL)

Bugfixes

• fix AssertionOrderModulation s.t. it can handle mixed iterations (with and without modulation)
• fix NullPointerException in loop acceleration (LA Woelfing)

Known Issues

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

v0.1.12

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)

v0.1.11

Features

• add support for non-standard fp.to_ieee_bv function
• dynamically switch between solvers depending on characteristics of trace formula in Wolf and Walrus strategy (also avoids MathSat when formula contains quantifier)

Bugfixes

Taipan / Abstract Interpretation

• fix soundness bug during abstract state retrieval: without summary computation, summary map cannot contain valid states
• fix getSmtIdentifier() bug: also try constants
• fix isSubsetOf assertion bug in AbsIntHoareTripleChecker

Misc

• SpaceExParser now throws an exception when multiple input files are used.

Plumbing

• new class for handling of SMT sorts
• adapt absint regression settings (use inlining of procedures without implementation)
• assert that you do not accidentally use AbsIntPredicate as backing for AbsIntPredicate and fix places where this happened

Known Issues

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

v0.1.10

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)