summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Boogie: added /vcsLoad flag as a convenient way to set /vcsCores ↵Gravatar Unknown2012-09-28
| | | | proportionally to the machine's number of cores
* MergeGravatar Unknown2012-09-28
|\
* | Fixed bug with uniformity analysis for havoc. Allowed barrier invariants toGravatar Unknown2012-09-28
| | | | | | | | | | support a more expressive class of expressions. Refactored thread id creation functions.
| * Dafny: Removed assembly reference to 'AIFramework'.Gravatar wuestholz2012-09-28
| |
| * Fixed the build.Gravatar wuestholz2012-09-28
| |
| * Boogie: added type 'real' with overloaded arithmetic operations plus real ↵Gravatar boehmes2012-09-27
| | | | | | | | | | | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
| * Added BigDec as representation for (floating-point) decimal valuesGravatar boehmes2012-09-27
| |
| * Boogie: new syntax for integer division and modulus: use div and mod instead ↵Gravatar boehmes2012-09-27
| | | | | | | | of / and %
| * Removed AIFramework from Boogie -- use native trivial or native ↵Gravatar boehmes2012-09-27
| | | | | | | | | | | | | | interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
| * Removed abandoned Isabelle prover backendGravatar boehmes2012-09-27
|/
* Barrier invariants can now refer to local variables that are uniform.Gravatar Unknown2012-09-26
|
* MergeGravatar Unknown2012-09-24
|\
* | Fixed issue with uniformity analysis and block merging. Uniformity analysisGravatar Unknown2012-09-24
| | | | | | | | now enabled by default.
| * MergeGravatar Egor Kyshtymov2012-09-24
|/|
| * Added detailed trace functionality.Gravatar Egor Kyshtymov2012-09-24
| | | | | | | | | | Improved error reporting. Tidied up code.
* | Support for barrier invariants.Gravatar Unknown2012-09-24
| |
* | Fixed a bug with empty big blocks.Gravatar Unknown2012-09-21
| |
* | MergeGravatar Unknown2012-09-21
|\ \
* | | Added support for invariants about shared state.Gravatar Unknown2012-09-21
| | | | | | | | | | | | | | | | | | Reworked implementation of barriers. Started on support for barrier invariants.
| * | MergeGravatar Unknown2012-09-19
| |\ \ | |/ / |/| |
| * | Boogie: improved parser makefileGravatar Unknown2012-09-19
| | |
* | | When uniformity analysis is disabled, no procedures (even the kernel entryGravatar Unknown2012-09-19
| | | | | | | | | | | | | | | point) will be regarded as uniform. This simplification avoids various edge cases.
* | | MergeGravatar Unknown2012-09-18
|\| |
* | | Uniformity analysis. Patch by Peter Collingbourne.Gravatar Unknown2012-09-18
| | |
* | | Dualisation modified so that global arrays are not dualised, and group-sharedGravatar Unknown2012-09-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | arrays are turned into 2D maps with first index type bool. Thread 1 always indexes into "true", while threads 2 indexes into "samegroup" (a formula which is true iff threads 1 and 2 are in the same group). Thus if the threads are in different groups they operate on different shared arrays, but if they are in the same group they operate on the same shared array. This paves the way for implementing support for barrier invariants.
| * | MergeGravatar Nadia Polikarpova2012-09-17
| |\ \ | |/ / |/| |
| * | Allow custom operators on a lineGravatar Nadia Polikarpova2012-09-17
| | |
* | | During dualisation,Gravatar Unknown2012-09-17
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | x := y; now becomes x$1 := y$1; x$2 := y$2; instead of x$1, x$2 := y$1, y$2; This is to make way for further changes.
| * Allow several calculation operators (for the whole calculation)Gravatar Nadia Polikarpova2012-09-16
| |
| * Allowing calc as hint (without braces)Gravatar Nadia Polikarpova2012-09-16
| |
| * Renamed terms into lines (according to the proposal), fixed some contractsGravatar Nadia Polikarpova2012-09-16
| |
* | Added creation of source variable pre- and post- conditions.Gravatar Egor Kyshtymov2012-09-16
| | | | | | | | | | Changed style of error messages. Cleaned up error reporting code.
| * Error reporting for calculation stepsGravatar Nadia Polikarpova2012-09-14
| |
| * Calc statements: Renamed Steps into Terms; introduced Steps (expressions ↵Gravatar Nadia Polikarpova2012-09-14
| | | | | | | | t<i> op t<i + 1>), generated during resolution; first version of the translation
| * MergeGravatar Nadia Polikarpova2012-09-14
| |\ | |/ |/|
| * Pretty-print calc statementsGravatar Nadia Polikarpova2012-09-14
| |
| * Resolve and clone calc statements; fixed a small grammar bugGravatar Nadia Polikarpova2012-09-13
| |
| * Added calc statement to the AST and the grammar (first attempt)Gravatar Nadia Polikarpova2012-09-13
| |
* | Dafny: clone and merge attributes in refinementsGravatar Unknown2012-09-12
| |
* | Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ↵Gravatar Unknown2012-09-12
|/ | | | and axiomatize [][..0] == [] == [][0..]
* Dafny: did a little to extend the support of labeled statements in ↵Gravatar Unknown2012-09-10
| | | | refinements (things like multiple labels are still not thought through very well)
* Dafny: improved checking of inherited postconditions (in refinements)Gravatar Unknown2012-09-10
|
* Boogie: added /tracePOs option for printing out number of proof obligations ↵Gravatar Unknown2012-09-10
| | | | without also printing out the verification times
* MergeGravatar Rustan Leino2012-09-10
|\
* | Dafny: allow 'decreases *' (that is, non-terminating recursion) on ↵Gravatar Rustan Leino2012-09-09
| | | | | | | | tail-recursive methods
* | MergeGravatar Unknown2012-09-07
|\ \
* | | Dafny: Added detection and support for tail recursive calls (and an ↵Gravatar Unknown2012-09-07
| | | | | | | | | | | | optional "tailrecursion" attribute). Also, let the cloner also clone attributes.
| * | Implement support for alternative SMT solvers -- CVC3 and CVC4Gravatar Peter Collingbourne2012-09-06
| | |
* | | MergeGravatar Unknown2012-09-05
|\| |
| * | Moved point at which preprocessed output is shown.Gravatar Unknown2012-08-31
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 22:24:56 +0000