summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator
Commit message (Expand)AuthorAge
* Fix for addressof expressions.Gravatar Unknown2012-05-18
* Add options to control the emission of free ensures forGravatar Unknown2012-04-16
* Removed expression simplifier (actually just commentedGravatar Unknown2012-04-15
* Added "free ensures" to procedures encoding the allocatednessGravatar Unknown2012-04-10
* Fix a lot of the translation of "op=" expressionsGravatar Unknown2012-04-09
* Changed the BCT solution so it uses the CodePlex version of CCI (insteadGravatar Mike Barnett2012-03-30
* Automated merge with https://hg01.codeplex.com/boogieGravatar Mike Barnett2012-03-29
|\
* | updated Boogie strings so that they can refer to \" (and more)Gravatar qadeer2012-03-12
| * Automated merge with https://hg01.codeplex.com/boogieGravatar Mike Barnett2012-03-11
|/|
| * more work on op-assign expressions. (unfinished)Gravatar Mike Barnett2012-03-11
* | further sanitization of string in :value attributeGravatar qadeer2012-03-11
* | added breadcrumb to the beginning of each methodGravatar qadeer2012-03-09
* | value attribute "\n" to "\\n"Gravatar qadeer2012-03-01
| * Automated merge with https://hg01.codeplex.com/boogieGravatar Mike Barnett2012-02-27
|/|
| * Adapting to new decompiler.Gravatar Mike Barnett2012-02-27
* | adding attribute for string literalsGravatar qadeer2012-02-27
* | added :first attribute to the first line directive corresponding to a source ...Gravatar qadeer2012-02-13
|/
* Union is now based on axiomsGravatar qadeer2012-02-07
* fixed bug in model parsingGravatar qadeer2012-02-06
* MergeGravatar qadeer2012-02-06
|\
* | added inlining support for all implementations given the attribute {:inline 1}Gravatar qadeer2012-02-06
| * Automated merge with https://hg01.codeplex.com/boogieGravatar Mike Barnett2012-02-05
|/|
| * Separated the concepts of "boxing" (i.e., CLR boxing of a value type) fromGravatar Mike Barnett2012-02-05
* | added a dummy sourceLine attribute for delegate dispatchGravatar qadeer2012-01-31
| * Automated merge with https://hg01.codeplex.com/boogieGravatar Mike Barnett2012-01-26
| |\
| | * Separate out the concepts of boxingGravatar Mike Barnett2012-01-26
* | | added another method that just throws an exceptionGravatar qadeer2012-01-24
|/ /
* / an optimization in dynamic dispatchGravatar qadeer2012-01-23
|/
* Mark the procedure translated from the module's entry pointGravatar Mike Barnett2012-01-15
* Make a copy of a struct value being passed to a methodGravatar Mike Barnett2012-01-10
* Fix call to struct copy ctor.Gravatar Mike Barnett2012-01-10
* Fixed struct copy constructor implementation.Gravatar Mike Barnett2012-01-10
* Change the copy constructor for struct types so that it returns the copyGravatar Mike Barnett2012-01-09
* Copy structs that are passed by value as method call arguments.Gravatar Mike Barnett2012-01-04
* For now, just ignore "address of" nodes and translate the expression of whichGravatar Mike Barnett2012-01-03
* new axioms for subtypingGravatar qadeer2011-12-31
* modeling multiset using generalized array theoryGravatar qadeer2011-12-30
* made delegate a datatypeGravatar qadeer2011-12-30
* problem fixed after CCI updateGravatar qadeer2011-12-30
* fixed problems with datatypesGravatar qadeer2011-12-29
* Add instrumentation for branches.Gravatar Mike Barnett2011-12-28
* bug fix in houdini inlineDepthGravatar qadeer2011-12-06
* Refactored translator so it can be called programmatically and return theGravatar Mike Barnett2011-11-21
* BCT: Initialize Boogie's command-line options object correctly before usingGravatar Mike Barnett2011-11-21
* commented calls to GC.Collect()Gravatar qadeer2011-11-18
* Translate AddressOf expressions correctly.Gravatar Mike Barnett2011-11-16
* Load all assemblies before doing anything else so that the unification forGravatar Mike Barnett2011-11-16
* For some reason, these didn't get into the last commit.Gravatar Mike Barnett2011-11-14
* Trying to get the generics translation correct...Gravatar Mike Barnett2011-11-14
* moved the addition of selectors and testers to program.ResolveGravatar qadeer2011-11-11