Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix for parsing error in MAXSAT computation in ↵ | 2012-10-08 | |
| | | | | ProverInterface::CheckAssumptions. | ||
* | Boogie build failed | 2012-10-05 | |
| | |||
* | deleted unnecessary files | 2012-10-04 | |
| | |||
* | Dafny: fixed merge | 2012-10-04 | |
| | |||
* | Merge | 2012-10-04 | |
|\ | |||
* | | Dafny: complete implementation of iterators | 2012-10-03 | |
| | | |||
| * | Boogie build failed | 2012-10-04 | |
| | | |||
* | | Dafny: automatically update iterator _new field upon allocations | 2012-10-03 | |
| | | |||
* | | Dafny: fixed compiler bug in array allocation (reported as boogie:397957) | 2012-10-03 | |
| | | |||
* | | Dafny: good error locations for yield statements; other iterator ↵ | 2012-10-03 | |
| | | | | | | | | improvements / bug fixes | ||
* | | Dafny: more part of verifying iterators | 2012-10-03 | |
| | | |||
| * | changed the signing to ..\InterimKey.snk | 2012-10-03 | |
| | | |||
| * | bunch of refactorings | 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 | ||
* | | Dafny: changed iterator body to resolve to implicit fields rather than to ↵ | 2012-10-02 | |
| | | | | | | | | the formal in- and yield-parameters | ||
* | | Dafny: handle decreases clause for iterators | 2012-10-02 | |
| | | |||
* | | Dafny: incomplete snapshot of verification of iterators | 2012-10-02 | |
| | | |||
| * | Fixed GPUVerify solution. | 2012-10-01 | |
| | | | | | | | | Merged recent changes to BoogieDriver into GPUVerifyBoogieDriver. | ||
| * | Merge | 2012-10-01 | |
| |\ | |||
| * | | Fix to abstract interpretation to match Boogie. | 2012-10-01 | |
| | | | |||
| | * | Chalice: Two new test-cases for recently fixed problems. | 2012-10-01 | |
| | | | |||
| | * | Chalice: Disallow unfolding expressions in postconditions. | 2012-10-01 | |
| | | | |||
| | * | Chalice: Fix bug in detecting permissions in postconditions. | 2012-10-01 | |
| | | | |||
| | * | Chalice: Let the trigger for the function postcondition axiom be more ↵ | 2012-10-01 | |
| | | | | | | | | | | | | permissive. | ||
| | * | Updated the 'PrepareBoogieZip.bat' script. | 2012-10-01 | |
| | | | |||
| | * | Merge | 2012-09-30 | |
| | |\ | |||
| | * | | Chalice: Use new 'mod' and 'div' operators of Boogie for division and modulo. | 2012-09-30 | |
| | | | | |||
| | * | | Chalice: Remove superfluous comment. | 2012-09-30 | |
| | | | | |||
| | * | | Chalice: Clean up /percentageSupport command line option to adapt to the ↵ | 2012-09-30 | |
| | | | | | | | | | | | | | | | | usage of reals for permissions. | ||
| | * | | Chalice: Activate the test-case tests/permission-model/scaling.chalice that ↵ | 2012-09-30 | |
| | | | | | | | | | | | | | | | | was previously disabled due to performance problems. | ||
| | * | | Chalice: Fix some problems related to the use of reals in Boogie. | 2012-09-30 | |
| | | | | |||
* | | | | Dafny: fixed compilation issue (a datatype is now allowed to be called "d") | 2012-09-29 | |
| | | | | |||
| | * | | Chalice: Further changes to make permissions use the Boogie type real. | 2012-09-29 | |
| | | | | |||
| | * | | Chalice: Make permissions use the Boogie type real. | 2012-09-29 | |
| | | | | |||
| | * | | Chalice: Extend the Boogie AST with real literals. | 2012-09-29 | |
| | | | | |||
| | | * | Merge | 2012-09-29 | |
| | | |\ | |||
| | * | | | Chalice (Adapt to real support in Boogie): Axiomatization of division is no ↵ | 2012-09-29 | |
| | | |/ | | |/| | | | | | | | | | longer needed (and in fact, results in a Boogie parse error). | ||
| | * | | Boogie: updated syntax highlighting ("real") | 2012-09-28 | |
| | | | | |||
| | * | | Dafny: removed div/mod axioms, since Boogie now interprets div/mod | 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 ↵ | 2012-09-28 | |
| |/ / | | | | | | | | | | proportionally to the machine's number of cores | ||
| * | | Merge | 2012-09-28 | |
| |\ \ | |||
| * | | | Fixed bug with uniformity analysis for havoc. Allowed barrier invariants to | 2012-09-28 | |
| | | | | | | | | | | | | | | | | | | | | support a more expressive class of expressions. Refactored thread id creation functions. | ||
| | * | | Boogie build succeeded, 2 test(s) failed | 2012-09-28 | |
| | | | | |||
| | * | | Dafny: Removed assembly reference to 'AIFramework'. | 2012-09-28 | |
| | | | | |||
| | * | | Fixed the build. | 2012-09-28 | |
| | | | | |||
| | * | | Chalice: Add a test-case for a recently fixed issue. | 2012-09-28 | |
| | | | | |||
| | * | | Boogie build failed | 2012-09-28 | |
| | | | | |||
| | * | | Merge | 2012-09-27 | |
| | |\ \ | |||
| | * \ \ | Merge | 2012-09-27 | |
| | |\ \ \ | |||
| | * | | | | Boogie and Dafny: adjustments to the test suite expected output (and a ↵ | 2012-09-27 | |
| | | | | | | | | | | | | | | | | | | | | | | | | temporary hack in FloydCycleDetect.dfy to be corrected shortly) | ||
| | | | * | | Merge | 2012-09-27 | |
| | | | |\ \ | | | | |/ / | | | |/| | |