summaryrefslogtreecommitdiff
path: root/BCT
Commit message (Collapse)AuthorAge
* Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵Gravatar Rustan Leino2013-03-05
| | | | Codeplex repositories.
* Find implementations of interface methods for dynamic dispatch, not justGravatar Unknown2012-09-09
| | | | overrides of virtual methods.
* Avoid creating a dynamic dispatch table for GetHashCode and ToString: it endsGravatar Unknown2012-09-09
| | | | | up creating code that the Boogie parser gets a stack overflow while trying to parse!
* Moved the statement traverser's operand stack (used for explicit push/pop/dupGravatar Unknown2012-09-09
| | | | | | | | | | in the code model) into the sink so that the different statement traversers used for things like if-then-else statements share the same stack. Fixed a problem in the dispatch table for whole program virtual dispatch so it works for generic methods. Found input that either crashed the translator or caused it to produce bad Boogie: "fixed" it by having the translator thrown an exception so the method containing the bad code is skipped.
* Fix the whole-program translator so that exception handling is doneGravatar Unknown2012-08-23
| | | | | | | | | | correctly for virtual method calls. Changed the whole-program override for VisitMethodCall so that it creates a new CodeModel expression that does not contain virtual method calls and then translate that newly built expression. Treat type equality (and inequality) specially: translate it directly to a type test instead. But do it just for the idiom: "o.GetType == typeof(T)". In that case, turn it into "is#T$T($DynamicType(o))".
* Make the modelExceptions option an integer.Gravatar Unknown2012-08-22
| | | | | | | | | | | | | | | 0 means no modeling at all. 1 (which can be specified only if also specifying whole program translation) means that a fixpoint analysis will be done on all of the translated assemblies to compute the set of exceptions that each method can throw (even though we're using only the fact that a method throws anything at all, not the specific exceptions it can throw) so only calls to methods that can throw an exception have a branch after the call that checks to see if an exception has been thrown. Methods that are defined outside of the set of translated assemblies are assumed to *not* throw any exceptions! 2 means that every method is considered to be one that can throw an exception.
* 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
| | | | | | method calls are not followed by a test to see if an exception was thrown "throw e" is translated as "assume false" "try S catch C finally F" is translated as "S; F"
* When translating an assighment, leave the source of the assignment on theGravatar Unknown2012-06-02
| | | | stack in case it is needed by an enclosing expression.
* Don't add dummy modules (resulting from a failed load) to the list of modulesGravatar Unknown2012-06-02
| | | | to be translated.
* Fix for addressof expressions.Gravatar Unknown2012-05-18
|
* Add options to control the emission of free ensures forGravatar Unknown2012-04-16
| | | | | | heap monotonicity (and allocatedness of references returned from a method) as well as the assert/assume checks that are generated for every object dereference.
* Removed expression simplifier (actually just commentedGravatar Unknown2012-04-15
| | | | | | | it out for now) and used a simpler scheme for always assigning compound bound expressions to a local. Added the ability to assert/assume that an object is non-null before dereferencing it.
* Added "free ensures" to procedures encoding the allocatednessGravatar Unknown2012-04-10
| | | | of references.
* Fix a lot of the translation of "op=" expressionsGravatar Unknown2012-04-09
| | | | (like += or *=).
* Changed the BCT solution so it uses the CodePlex version of CCI (insteadGravatar Mike Barnett2012-03-30
| | | | | | of the internal version). Fixed the expression traverser to (begin the) support target expressions as operands of binary expressions. (e.g., x++ or x += 2)
* 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
| | | | | | | | fixed BCT :value
| * 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
| | | | | | | | more work is perhaps needed to handle all cases
| * Automated merge with https://hg01.codeplex.com/boogieGravatar Mike Barnett2012-02-27
|/|
| * Adapting to new decompiler.Gravatar Mike Barnett2012-02-27
| | | | | | | | Dynamic dispatch for interface method calls.
* | adding attribute for string literalsGravatar qadeer2012-02-27
| |
* | added :first attribute to the first line directive corresponding to a source ↵Gravatar qadeer2012-02-13
|/ | | | line
* Union is now based on axiomsGravatar qadeer2012-02-07
| | | | added more inline attributes
* fixed bug in model parsingGravatar qadeer2012-02-06
| | | | converted a bunch of definitions to be inlined
* MergeGravatar qadeer2012-02-06
|\
* | added inlining support for all implementations given the attribute {:inline 1}Gravatar qadeer2012-02-06
| | | | | | | | | | removed AssertionInjector from the solution changed the representation of multicast delegates
| * 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
| | | | | | | | the "union" type that is the supertype of all the translated Boogie types.
* | 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
| | | | | | | | | | | | | | | | | | | | | (i.e., CLR's creating a heap cell and putting a value into it) from the concept of the "union" type that all Boogie types are a subtype of.
* | | added another method that just throws an exceptionGravatar qadeer2012-01-24
|/ /
* / an optimization in dynamic dispatchGravatar qadeer2012-01-23
|/ | | | a hack in event translation
* Mark the procedure translated from the module's entry pointGravatar Mike Barnett2012-01-15
| | | | with the attribute {:entrypoint}.
* Make a copy of a struct value being passed to a methodGravatar Mike Barnett2012-01-10
| | | | whether the method is generic or not.
* 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
| | | | | of the struct value. This way it can do an allocation within the copy ctor (if that is the design choice for structs, which it currently is).
* Copy structs that are passed by value as method call arguments.Gravatar Mike Barnett2012-01-04
| | | | Define body for default struct ctors.
* For now, just ignore "address of" nodes and translate the expression of whichGravatar Mike Barnett2012-01-03
| | | | the address is being taken.
* new axioms for subtypingGravatar qadeer2011-12-31
|
* modeling multiset using generalized array theoryGravatar qadeer2011-12-30
|
* made delegate a datatypeGravatar qadeer2011-12-30
| | | | added a DatatypeConstructor class
* problem fixed after CCI updateGravatar qadeer2011-12-30
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 09:12:09 +0000