summaryrefslogtreecommitdiff
path: root/BCT
Commit message (Expand)AuthorAge
* 1. Converted assume to assert for the source infoGravatar qadeer2010-12-21
* Changed attribute names in the BPL for source context assumption statements.Gravatar mikebarnett2010-12-21
* Use an explicit PdbReader instead of the more general ISourceLocationProvider...Gravatar mikebarnett2010-12-21
* added support for array translation.Gravatar qadeer2010-12-20
* Generate "assume {:filename "foo.cs"}{:line 3} true" statements for each stat...Gravatar mikebarnett2010-12-20
* Translate boolean types into Bpl.Type.Bool.Gravatar mikebarnett2010-12-20
* Added Alloc implementation to the PreludeGravatar qadeer2010-12-15
* Added a new option for splitting fieldsGravatar qadeer2010-12-15
* Fixed declaration of procedures from static methods so that they don't have t...Gravatar mikebarnett2010-12-14
* changed the prelude to use only the int type and eliminated bunch of axioms n...Gravatar qadeer2010-12-14
* Translate calls to static methods.Gravatar mikebarnett2010-12-14
* Add freshly-allocated object as argument to ctors.Gravatar mikebarnett2010-12-14
* Translate object creation expressions.Gravatar mikebarnett2010-12-14
* Add a reference to ParserHelper.dll for the definition of IToken which was mo...Gravatar mikebarnett2010-12-09
* Fixed field update and field dereference.Gravatar mikebarnett2010-12-09
* Adapt to new APIs in CCI.Gravatar mikebarnett2010-12-08
* General hygiene: introduced (fixed) a helper method that creates Boogie token...Gravatar mikebarnett2010-07-05
* Cleaned up the sink: removed the OutVars, which was state the sink needed onl...Gravatar mikebarnett2010-07-05
* Forgotten file: Sink.csGravatar mikebarnett2010-07-05
* Introduction of the Sink: a global object that is threaded through all of the...Gravatar mikebarnett2010-07-02
* Forgotten file.Gravatar mikebarnett2010-06-30
* Simplified the translator by merging the ToplevelTraverser, ClassTraverser, a...Gravatar mikebarnett2010-06-28
* Added the factory pattern so that all traversers are created through factory ...Gravatar mikebarnett2010-06-16
* Consistently use the new code pattern for translating locations to tokens and...Gravatar mikebarnett2010-06-07
* Added forgotten file.Gravatar mikebarnett2010-06-06
* Updated the project to .NET v4.0.Gravatar mikebarnett2010-06-06
* BCT: Added prelude. Started test1 as a test of verification.Gravatar rustanleino2010-05-12
* Forgotten to turn the echo off.Gravatar mikebarnett2010-04-19
* Updated list of tests to just include test0.Gravatar mikebarnett2010-04-19
* New, simpler way of running regressions.Gravatar mikebarnett2010-04-19
* Moved BCT project references for Boogie to the Boogie\Binaries directory.Gravatar rustanleino2010-04-16
* Upgraded solution file and project file to VS2010.Gravatar mikebarnett2010-04-16
* Updated to use new CCI API.Gravatar mikebarnett2010-04-16
* Setting up test cases for BCTGravatar schaef2009-11-20
* Update use of CCI's API for decompiling the IL model to the Code Model.Gravatar mikebarnett2009-11-17
* Changed solution to include the CCI projects from Codeplex. (Still flaky in t...Gravatar mikebarnett2009-11-10
* Changed error message to have correct program name.Gravatar mikebarnett2009-11-10
* Please ignore. Just testing my account.Gravatar schaef2009-08-19
* The beginnings of a CCI Metadata (http://ccimetadata.codeplex.com) based byte...Gravatar mikebarnett2009-08-09