| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | bunch of refactorings |  Unknown | 2012-10-03 |
| | | | | | | | | | | - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs | ||
| * | Fixed GPUVerify solution. |  Unknown | 2012-10-01 |
| | | | | | Merged recent changes to BoogieDriver into GPUVerifyBoogieDriver. | ||
| * | Merge | Unknown | 2012-10-01 |
| |\ | |||
| * | | Fix to abstract interpretation to match Boogie. | Unknown | 2012-10-01 |
| | | | |||
| | * | Chalice: Two new test-cases for recently fixed problems. |  stefanheule | 2012-10-01 |
| | | | |||
| | * | Chalice: Disallow unfolding expressions in postconditions. | stefanheule | 2012-10-01 |
| | | | |||
| | * | Chalice: Fix bug in detecting permissions in postconditions. | stefanheule | 2012-10-01 |
| | | | |||
| | * | Chalice: Let the trigger for the function postcondition axiom be more ↵ | stefanheule | 2012-10-01 |
| | | | | | | | | | permissive. | ||
| | * | Updated the 'PrepareBoogieZip.bat' script. | wuestholz | 2012-10-01 |
| | | | |||
| | * | Merge | stefanheule | 2012-09-30 |
| | |\ | |||
| | * | | Chalice: Use new 'mod' and 'div' operators of Boogie for division and modulo. | stefanheule | 2012-09-30 |
| | | | | |||
| | * | | Chalice: Remove superfluous comment. | stefanheule | 2012-09-30 |
| | | | | |||
| | * | | Chalice: Clean up /percentageSupport command line option to adapt to the ↵ | stefanheule | 2012-09-30 |
| | | | | | | | | | | | | | usage of reals for permissions. | ||
| | * | | Chalice: Activate the test-case tests/permission-model/scaling.chalice that ↵ | stefanheule | 2012-09-30 |
| | | | | | | | | | | | | | was previously disabled due to performance problems. | ||
| | * | | Chalice: Fix some problems related to the use of reals in Boogie. | stefanheule | 2012-09-30 |
| | | | | |||
| | * | | Chalice: Further changes to make permissions use the Boogie type real. | stefanheule | 2012-09-29 |
| | | | | |||
| | * | | Chalice: Make permissions use the Boogie type real. | stefanheule | 2012-09-29 |
| | | | | |||
| | * | | Chalice: Extend the Boogie AST with real literals. | stefanheule | 2012-09-29 |
| | | | | |||
| | | * | Merge |  Nadia Polikarpova | 2012-09-29 |
| | | |\ | |||
| | * | | | Chalice (Adapt to real support in Boogie): Axiomatization of division is no ↵ | stefanheule | 2012-09-29 |
| | | |/ | |/| | | | | | | | longer needed (and in fact, results in a Boogie parse error). | ||
| | * | | Boogie: updated syntax highlighting ("real") |  Unknown | 2012-09-28 |
| | | | | |||
| | * | | Dafny: removed div/mod axioms, since Boogie now interprets div/mod | Unknown | 2012-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 ↵ | Unknown | 2012-09-28 |
| |/ / | | | | | | | proportionally to the machine's number of cores | ||
| * | | Merge |  Unknown | 2012-09-28 |
| |\ \ | |||
| * | | | Fixed bug with uniformity analysis for havoc. Allowed barrier invariants to | Unknown | 2012-09-28 |
| | | | | | | | | | | | | | | | | support a more expressive class of expressions. Refactored thread id creation functions. | ||
| | * | | Boogie build succeeded, 2 test(s) failed | CodeplexBot | 2012-09-28 |
| | | | | |||
| | * | | Dafny: Removed assembly reference to 'AIFramework'. | wuestholz | 2012-09-28 |
| | | | | |||
| | * | | Fixed the build. | wuestholz | 2012-09-28 |
| | | | | |||
| | * | | Chalice: Add a test-case for a recently fixed issue. | stefanheule | 2012-09-28 |
| | | | | |||
| | * | | Boogie build failed | CodeplexBot | 2012-09-28 |
| | | | | |||
| | * | | Merge | Unknown | 2012-09-27 |
| | |\ \ | |||
| | * \ \ | Merge | Unknown | 2012-09-27 |
| | |\ \ \ | |||
| | * | | | | Boogie and Dafny: adjustments to the test suite expected output (and a ↵ | Unknown | 2012-09-27 |
| | | | | | | | | | | | | | | | | | | | | | temporary hack in FloydCycleDetect.dfy to be corrected shortly) | ||
| | | | * | | Merge |  Unknown | 2012-09-27 |
| | | | |\ \ | | | |/ / | | |/| | | |||
| | | | * | | Chalice: changed quantifier triggering to use #limited#trigger versions of ↵ | Unknown | 2012-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. | ||
| | | * | | Merge | Unknown | 2012-09-27 |
| | | |\ \ | |_|/ / |/| | | | |||
| | | * | | DafnyExtension: make it usable also in Visual Studio 2012 | Unknown | 2012-09-27 |
| | | | | | |||
| | * | | | Boogie: added type 'real' with overloaded arithmetic operations plus real ↵ | boehmes | 2012-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 values | boehmes | 2012-09-27 |
| | | | | | |||
| | * | | | Boogie: new syntax for integer division and modulus: use div and mod instead ↵ | boehmes | 2012-09-27 |
| | | | | | | | | | | | | | | | | | of / and % | ||
| | * | | | Removed AIFramework from Boogie -- use native trivial or native ↵ | boehmes | 2012-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 backend | boehmes | 2012-09-27 |
| |/ / / | |||
| * / / | Barrier invariants can now refer to local variables that are uniform. | Unknown | 2012-09-26 |
| |/ / | |||
| | * | Merge | Nadia Polikarpova | 2012-09-25 |
| | |\ | |/ |/| | |||
| * | | Merge | Unknown | 2012-09-24 |
| |\ \ | |||
| * | | | Fixed issue with uniformity analysis and block merging. Uniformity analysis | Unknown | 2012-09-24 |
| | | | | | | | | | | | | | now enabled by default. | ||
| | * | | Merge | stefanheule | 2012-09-24 |
| | |\ \ | |||
| | * | | | Chalice: New regression test-case. | stefanheule | 2012-09-24 |
| | | | | | |||
| | * | | | Chalice: Fix type-checker incompleteness. | stefanheule | 2012-09-24 |
| | | | | | |||
| | * | | | Chalice: Add new regression test case. | stefanheule | 2012-09-24 |
| | | | | | |||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |