summaryrefslogtreecommitdiff
path: root/BCT
Commit message (Expand)AuthorAge
* Fix a bug when static fields are used in as operands for ++ or --.Gravatar Unknown2012-07-31
* Add an option to model exceptional control flow or not. When it is false:Gravatar Unknown2012-07-31
* When translating an assighment, leave the source of the assignment on theGravatar Unknown2012-06-02
* Don't add dummy modules (resulting from a failed load) to the list of modulesGravatar Unknown2012-06-02
* 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
* | added another projectGravatar qadeer2012-01-30
| * 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
* MergeGravatar qadeer2011-12-28
|\
* | deleted some commented codeGravatar qadeer2011-12-28
| * Add instrumentation for branches.Gravatar Mike Barnett2011-12-28
|/
* refactored AssertionInjector so that it works directly on bpl files as wellGravatar qadeer2011-12-26
* bug fix in houdini inlineDepthGravatar qadeer2011-12-06