summaryrefslogtreecommitdiff
path: root/Source/Core/Absy.cs
Commit message (Expand)AuthorAge
* Added an attribute to set the time limit for implementations.Gravatar wuestholz2013-07-12
* Worked on the parallelization (task cancellation).Gravatar wuestholz2013-07-09
* Added support in the abstract interpreter for an attribute {:identity}, which...Gravatar Rustan Leino2013-07-05
* Did some refactoring in the execution engine.Gravatar wuestholz2013-06-14
* Worked on improving program snapshot verification.Gravatar wuestholz2013-06-10
* Worked on improving program snapshot verification.Gravatar wuestholz2013-06-05
* Added a feature for verifying several program snapshots (incl. result caching...Gravatar wuestholz2013-06-02
* Staged HoudiniGravatar allydonaldson2013-04-30
* fixed datatype bug reported by ChrisGravatar Unknown2013-03-05
* Refactored code that generates an axiom for a function, and changed the prett...Gravatar Rustan Leino2013-01-17
* Allow attributes on procedure formals, function formals, and bound variablesGravatar Unknown2013-01-07
* Removed old comments about "BASEMOVE" and other constructor calls, where the ...Gravatar Unknown2013-01-07
* Gather set of procedures with irreducible loops.Gravatar Unknown2012-11-18
* added sound loop unrollingGravatar Yannick Welsch2012-07-03
* bunch of refactoringsGravatar Unknown2012-10-03
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
* Move block predicator to VCGenerationGravatar Peter Collingbourne2012-06-18
* Trying to merge with recent changes, failing.Gravatar Ken McMillan2012-06-05
|\
| * Some changes to support expanded use of z3api.Gravatar Ken McMillan2012-06-05
* | moved class Macro to AbsyGravatar qadeer2012-06-04
* | 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an a...Gravatar Unknown2012-06-01
* | No need for extra attributes in ExtractLoopsGravatar akashlal2012-05-28
* | MergeGravatar Unknown2012-05-25
|\ \
* | | Adding an option for deterministicExtractLoops, that uses an alternate way to...Gravatar Unknown2012-05-25
| * | more refactoring in stratified inliningGravatar qadeer2012-05-24
|/ /
* | removed lazy inliningGravatar qadeer2012-04-28
* | more type checking for datatypesGravatar qadeer2012-03-18
|/
* Boogie: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* made delegate a datatypeGravatar qadeer2011-12-30
* fixed problems with datatypesGravatar qadeer2011-12-29
* MergeGravatar Rustan Leino2011-12-07
|\
| * MergeGravatar Michal Moskal2011-12-07
| |\
| * | Make set iteration order deterministicGravatar Michal Moskal2011-12-07
* | | MergeGravatar Rustan Leino2011-12-05
|\ \ \ | | |/ | |/|
* | | Boogie: Added new abstract interpretation harness, which uses native Boogie E...Gravatar Rustan Leino2011-12-05
| |/ |/|
| * Emit attribute on a requiresGravatar akashlal2011-12-04
|/
* MergeGravatar qadeer2011-11-22
|\
| * Boogie: don't resolve ignored types (that is, "extern" types that have been t...Gravatar Rustan Leino2011-11-22
* | added support for handling duplicate axiomsGravatar qadeer2011-11-22
|/
* Debugging output for stratified inlining. Emit attribute on Ensures whileGravatar Unknown2011-11-16
* moved the addition of selectors and testers to program.ResolveGravatar qadeer2011-11-11
* deleted unused codeGravatar qadeer2011-11-01
* Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* Boogie: removed unreachable or unused codeGravatar Rustan Leino2011-10-27
* Dafny: Fixed an assertion violation in the "Checked" configuration.Gravatar wuestholz2011-09-20
* Dafny: Added support for attributes on methods and constructors.Gravatar wuestholz2011-09-16
* Fixed test failures in the "Checked" configuration.Gravatar wuestholz2011-09-19
* Support for irreducible graphs (with extractLoops)Gravatar Unknown2011-08-24
* reverting irreducible handling temporarilyGravatar qadeer2011-08-21
|\
* | added code to handle irreducible graphsGravatar qadeer2011-08-20