summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Support for "do_not_predicate" in predication of requires and ensuresGravatar Unknown2012-12-20
|
* A simplification to predication of requires and ensures.Gravatar Unknown2012-11-29
|
* Fixes to uniformity analysis.Gravatar Unknown2012-11-29
|
* Fix for parsing error in MAXSAT computation in ↵Gravatar Unknown2012-10-08
| | | | ProverInterface::CheckAssumptions.
* Dafny: fixed mergeGravatar Rustan Leino2012-10-04
|
* MergeGravatar Rustan Leino2012-10-04
|\
* | Dafny: complete implementation of iteratorsGravatar Rustan Leino2012-10-03
| |
* | Dafny: automatically update iterator _new field upon allocationsGravatar Rustan Leino2012-10-03
| |
* | Dafny: fixed compiler bug in array allocation (reported as boogie:397957)Gravatar Rustan Leino2012-10-03
| |
* | Dafny: good error locations for yield statements; other iterator ↵Gravatar Rustan Leino2012-10-03
| | | | | | | | improvements / bug fixes
* | Dafny: more part of verifying iteratorsGravatar Rustan Leino2012-10-03
| |
| * changed the signing to ..\InterimKey.snkGravatar qadeer2012-10-03
| |
| * bunch of refactoringsGravatar Unknown2012-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 ↵Gravatar Rustan Leino2012-10-02
| | | | | | | | the formal in- and yield-parameters
* | Dafny: handle decreases clause for iteratorsGravatar Rustan Leino2012-10-02
| |
* | Dafny: incomplete snapshot of verification of iteratorsGravatar Rustan Leino2012-10-02
| |
| * Fixed GPUVerify solution.Gravatar Unknown2012-10-01
| | | | | | | | Merged recent changes to BoogieDriver into GPUVerifyBoogieDriver.
| * MergeGravatar Unknown2012-10-01
| |\
| * | Fix to abstract interpretation to match Boogie.Gravatar Unknown2012-10-01
| | |
* | | Dafny: fixed compilation issue (a datatype is now allowed to be called "d")Gravatar Rustan Leino2012-09-29
| | |
| | * MergeGravatar Nadia Polikarpova2012-09-29
| | |\
| | | * 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
| | |
* | | Dafny: compile iteratorsGravatar Rustan Leino2012-09-26
| | |
* | | 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 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
| | | |
| | | * Use expression splitting for checking calculation stepsGravatar Nadia Polikarpova2012-09-23
| | | |
| | | * Bugfix in the translation of calc statements (oops), added more resolution ↵Gravatar Nadia Polikarpova2012-09-21
| | | | | | | | | | | | | | | | and verification tests
| | | * Added tests for parsing and resolution of calc statementsGravatar Nadia Polikarpova2012-09-21
| | | |
| | | * MergeGravatar Nadia Polikarpova2012-09-21
| | | |\ | | |_|/ | |/| |
| * | | 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 Nadia Polikarpova2012-09-20
| | | | |\ | | | |_|/ | | |/| |
| | | | * Allow a single != in a calcGravatar Nadia Polikarpova2012-09-20
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 13:07:03 +0000