summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
| | | * MergeGravatar Nadia Polikarpova2012-09-29
| | | |\
| | * | | Chalice (Adapt to real support in Boogie): Axiomatization of division is no ↵Gravatar stefanheule2012-09-29
| | | |/ | | |/| | | | | | | | | longer needed (and in fact, results in a Boogie parse error).
| | * | Boogie: updated syntax highlighting ("real")Gravatar Unknown2012-09-28
| | | |
| | * | Dafny: removed div/mod axioms, since Boogie now interprets div/modGravatar Unknown2012-09-28
| | | | | | | | | | | | | | | | | | | | Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support
| | * | 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.
| | * | Boogie build succeeded, 2 test(s) failedGravatar CodeplexBot2012-09-28
| | | |
| | * | Dafny: Removed assembly reference to 'AIFramework'.Gravatar wuestholz2012-09-28
| | | |
| | * | Fixed the build.Gravatar wuestholz2012-09-28
| | | |
| | * | Chalice: Add a test-case for a recently fixed issue.Gravatar stefanheule2012-09-28
| | | |
| | * | Boogie build failedGravatar CodeplexBot2012-09-28
| | | |
| | * | MergeGravatar Unknown2012-09-27
| | |\ \
| | * \ \ MergeGravatar Unknown2012-09-27
| | |\ \ \
| | * | | | Boogie and Dafny: adjustments to the test suite expected output (and a ↵Gravatar Unknown2012-09-27
| | | | | | | | | | | | | | | | | | | | | | | | temporary hack in FloydCycleDetect.dfy to be corrected shortly)
| | | | * | MergeGravatar Unknown2012-09-27
| | | | |\ \ | | | | |/ / | | | |/| |
| | | | * | Chalice: changed quantifier triggering to use #limited#trigger versions of ↵Gravatar Unknown2012-09-27
| | |_|/ / | |/| | | | | | | | | | | | | functions, instead of their "heap fragment" versions from the framing axiom. It's not totally clear why this works better, but it seems to avoid the excessive triggering Yannis' examples showed.
| | | * | MergeGravatar Unknown2012-09-27
| | | |\ \ | | |_|/ / | |/| | |
| | | * | DafnyExtension: make it usable also in Visual Studio 2012Gravatar Unknown2012-09-27
| | | | |
| | * | | 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
| |/ /
* | | Dafny: compile iteratorsGravatar Rustan Leino2012-09-26
| | |
* | | Dafny: added test cases for resolving iteratorsGravatar Rustan Leino2012-09-25
| | |
* | | Dafny: changed iterators to become special cases of classesGravatar Rustan Leino2012-09-25
| | |
* | | Dafny: added iterators; for now, only parsing and resolving (and printing ↵Gravatar Rustan Leino2012-09-25
| | | | | | | | | | | | and refining), no compilation or verification
| | * MergeGravatar Nadia Polikarpova2012-09-25
| | |\ | | |/ | |/|
| * | MergeGravatar Unknown2012-09-24
| |\ \
| * | | Fixed issue with uniformity analysis and block merging. Uniformity analysisGravatar Unknown2012-09-24
| | | | | | | | | | | | | | | | now enabled by default.
| | * | MergeGravatar stefanheule2012-09-24
| | |\ \
| | * | | Chalice: New regression test-case.Gravatar stefanheule2012-09-24
| | | | |
| | * | | Chalice: Fix type-checker incompleteness.Gravatar stefanheule2012-09-24
| | | | |
| | * | | Chalice: Add new regression test case.Gravatar stefanheule2012-09-24
| | | | |
| | * | | Chalice: Improve code to generate triggers for framing axiom.Gravatar stefanheule2012-09-24
| | | | |
| | * | | Chalice: Fix triggers for framing axiom of known-folded locations.Gravatar stefanheule2012-09-24
| | | | |
| | | * | MergeGravatar Egor Kyshtymov2012-09-24
| | |/| | | |/| | |
| | | * | Added detailed trace functionality.Gravatar Egor Kyshtymov2012-09-24
| | | | | | | | | | | | | | | | | | | | | | | | | Improved error reporting. Tidied up code.
| * | | | MergeGravatar Unknown2012-09-24
| |\ \ \ \
| * | | | | Support for barrier invariants.Gravatar Unknown2012-09-24
| | | | | |
| | * | | | MergeGravatar Unknown2012-09-24
| | |\ \ \ \
| | * | | | | added output for a test caseGravatar Unknown2012-09-24
| | | | | | |
| | | | | | * Use expression splitting for checking calculation stepsGravatar Nadia Polikarpova2012-09-23
| | | | | | |
| | | * | | | DafnyExtension: adding some missing keywords (for imports)Gravatar Unknown2012-09-21
| | |/ / / / | |/| | | |
| | | * | | Chalice: Fix soundness issue about when it is sound to keep knowledge about ↵Gravatar stefanheule2012-09-21
| | | | | | | | | | | | | | | | | | | | | | | | predicate permission masks.
| | | | | * Bugfix in the translation of calc statements (oops), added more resolution ↵Gravatar Nadia Polikarpova2012-09-21
| | | | | | | | | | | | | | | | | | | | | | | | and verification tests
| | | * | | Chalice: Alternative approach to frame known-folded locations; use ↵Gravatar stefanheule2012-09-21
| | | | | | | | | | | | | | | | | | | | | | | | quantification instead of explicit enumeration of locations.
| | | | | * Added tests for parsing and resolution of calc statementsGravatar Nadia Polikarpova2012-09-21
| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 10:56:48 +0000