| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Added the heap representation I was supposed to have started with... A ↵ |  mikebarnett | 2011-01-21 |
| | | | | | general one that generates function calls for heap reads and writes so that the actual heap representation can be decided just by changing the prelude. | ||
| * | Added a better options parsing by using functionality from MemberHelper. | mikebarnett | 2011-01-21 |
| | | | | | | | | Added a new heap representation, TwoDBoxHeap. Made method names unique (previously, overloads all shared the same procedure name). As part of that, no longer require method references to be resolved in order to generate a name. Added a regression test for TwoDBoxHeap. Added tests for method overloads for unique name generation. | ||
| * | Fix order of getting the instance and the field from the expression heap so ↵ | mikebarnett | 2011-01-21 |
| | | | | | that assignments are done correctly. | ||
| * | Put back the prelude for the split fields heap that had been there before. | mikebarnett | 2011-01-21 |
| | | |||
| * | Use the interned key of field references, now that they have one. | mikebarnett | 2011-01-21 |
| | | |||
| * | Added a test for the split fields option. | mikebarnett | 2011-01-20 |
| | | | | | Refactored some code to make it easier to work with different heap representations. | ||
| * | Moved the parts of the Prelude that depend on the heap representation into ↵ | mikebarnett | 2011-01-20 |
| | | | | | | | the appropriate Heap objects. Also added the ability to easily have access to the ASTs that result from the specific heap representation's declarations. | ||
| * | More structuring of the different heap representations. Now each heap ↵ | mikebarnett | 2011-01-19 |
| | | | | | representation is implemented as a different object. | ||
| * | Removed HeapVariable from everywhere now that it is encapsulated in the Heap ↵ | mikebarnett | 2011-01-19 |
| | | | | | component. | ||
| * | Removing resolution: there's no need to resolve field references in order to ↵ | mikebarnett | 2011-01-18 |
| | | | | | translate them. | ||
| * | The beginning of the encapsulation of the Heap representation so that we can ↵ | mikebarnett | 2011-01-17 |
| | | | | | easily have different ways of translating the heap. | ||
| * | Fix translation of "null" so that it produces a type-correct value. | mikebarnett | 2011-01-16 |
| | | |||
| * | 1. Converted assume to assert for the source info | qadeer | 2010-12-21 |
| | | | | | 2. Added tests for array translation | ||
| * | Changed attribute names in the BPL for source context assumption statements. | mikebarnett | 2010-12-21 |
| | | |||
| * | Use an explicit PdbReader instead of the more general ↵ | mikebarnett | 2010-12-21 |
| | | | | | ISourceLocationProvider so that we can get the closest source location even if the location we have doesn't correspond to an exact source location. | ||
| * | added support for array translation. | qadeer | 2010-12-20 |
| | | |||
| * | Generate "assume {:filename "foo.cs"}{:line 3} true" statements for each ↵ | mikebarnett | 2010-12-20 |
| | | | | | statement that has a source location. | ||
| * | Translate boolean types into Bpl.Type.Bool. | mikebarnett | 2010-12-20 |
| | | |||
| * | Added Alloc implementation to the Prelude | qadeer | 2010-12-15 |
| | | | | | | Fixed bug in translation of assume statement Added code for special handling of poirot specific calls | ||
| * | Added a new option for splitting fields | qadeer | 2010-12-15 |
| | | | | | Updated the regression input file | ||
| * | Fixed declaration of procedures from static methods so that they don't have ↵ | mikebarnett | 2010-12-14 |
| | | | | | | | the "this" parameter. If a method definition is marked with an attribute whose name is "AsyncAttribute", then all calls to that method have {: async } added as an attribute on the call. | ||
| * | changed the prelude to use only the int type and eliminated bunch of axioms ↵ | qadeer | 2010-12-14 |
| | | | | | not being used that were creating type checking problems at the Boogie level | ||
| * | Translate calls to static methods. | mikebarnett | 2010-12-14 |
| | | |||
| * | Add freshly-allocated object as argument to ctors. | mikebarnett | 2010-12-14 |
| | | |||
| * | Translate object creation expressions. | mikebarnett | 2010-12-14 |
| | | | | | Translate static fields into global variables. | ||
| * | Add a reference to ParserHelper.dll for the definition of IToken which was ↵ | mikebarnett | 2010-12-09 |
| | | | | | moved into that assembly. | ||
| * | Fixed field update and field dereference. | mikebarnett | 2010-12-09 |
| | | |||
| * | Adapt to new APIs in CCI. | mikebarnett | 2010-12-08 |
| | | |||
| * | General hygiene: introduced (fixed) a helper method that creates Boogie ↵ | mikebarnett | 2010-07-05 |
| | | | | | tokens. Made it an extension method that takes any object implementing IObjectWithLocations. Much easier to use within the translator. | ||
| * | Cleaned up the sink: removed the OutVars, which was state the sink needed ↵ | mikebarnett | 2010-07-05 |
| | | | | | only for assigning the local copy of a method's parameter to the out parameter of the Boogie procedure. But now that is simplified: instead of three versions of each parameter (in, local, and out), there are only two: in and out. For a parameter that is *not* by reference and is *not* an out parameter (i.e., just a plain pass-by-value parameter), the "out" version is a local variable. Otherwise it is an out parameter of the Boogie procedure. | ||
| * | Forgotten file: Sink.cs | mikebarnett | 2010-07-05 |
| | | | | | Added an override of ToString so MethodParameters show up nicer in the debugger. | ||
| * | Introduction of the Sink: a global object that is threaded through all of ↵ | mikebarnett | 2010-07-02 |
| | | | | | the traversers and which contains the information that they need to share with each other. | ||
| * | Forgotten file. | mikebarnett | 2010-06-30 |
| | | |||
| * | Simplified the translator by merging the ToplevelTraverser, ClassTraverser, ↵ | mikebarnett | 2010-06-28 |
| | | | | | and MethodTraverser into one traverser: MetadataTraverser. It will have to do a little more work to keep its state consistent (like saving any type-related state before traversing a nested type definition), but it seems worth it. | ||
| * | Added the factory pattern so that all traversers are created through factory ↵ | mikebarnett | 2010-06-16 |
| | | | | | | | | methods. This is the beginning of allowing plugins to perform methodology-specific translations. Added a CLR traverser that is meant to encode the CLR semantics. For now it just does one thing: add the assertion that a divisor should not be zero. Added an MS Test project so that we can use that for regression testing. | ||
| * | Consistently use the new code pattern for translating locations to tokens ↵ | mikebarnett | 2010-06-07 |
| | | | | | and putting the expression translation into a separate method. | ||
| * | Added forgotten file. | mikebarnett | 2010-06-06 |
| | | |||
| * | Updated the project to .NET v4.0. | mikebarnett | 2010-06-06 |
| | | | | | | | | | Added helper methods to the statement traverser. Handle ILocalDeclarationStatement, IAssertStatement, IAssumeStatement in StatementTraverser. Handle simple logical-and and logical-or expressions in ExpressionTraverser. Inject assertion that divisor is non-zero for IDivision in ExpressionTraverser. Added static variable BCT.Host so all parts of translation can access the CCI Metadata host. | ||
| * | BCT: Added prelude. Started test1 as a test of verification. | rustanleino | 2010-05-12 |
| | | |||
| * | Moved BCT project references for Boogie to the Boogie\Binaries directory. | rustanleino | 2010-04-16 |
| | | |||
| * | Upgraded solution file and project file to VS2010. | mikebarnett | 2010-04-16 |
| | | |||
| * | Updated to use new CCI API. | mikebarnett | 2010-04-16 |
| | | |||
| * | Setting up test cases for BCT | schaef | 2009-11-20 |
| | | |||
| * | Update use of CCI's API for decompiling the IL model to the Code Model. | mikebarnett | 2009-11-17 |
| | | |||
| * | Changed solution to include the CCI projects from Codeplex. (Still flaky in ↵ | mikebarnett | 2009-11-10 |
| | | | | | that it assumes the CCI sources are in a particular relative location to the BCT sources.) | ||
| * | Changed error message to have correct program name. | mikebarnett | 2009-11-10 |
| | | | | | | Deleted custom host, just use the default host. Write output file to current directory, use "foo.bpl" as the output file name for the input assembly "foo". | ||
| * | Please ignore. Just testing my account. | schaef | 2009-08-19 |
| | | |||
| * | The beginnings of a CCI Metadata (http://ccimetadata.codeplex.com) based ↵ | mikebarnett | 2009-08-09 |
| bytecode translator. | |||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |