Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Change the copy constructor for struct types so that it returns the copy | 2012-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. | 2012-01-04 | |
| | | | | Define body for default struct ctors. | ||
* | For now, just ignore "address of" nodes and translate the expression of which | 2012-01-03 | |
| | | | | the address is being taken. | ||
* | new axioms for subtyping | 2011-12-31 | |
| | |||
* | modeling multiset using generalized array theory | 2011-12-30 | |
| | |||
* | made delegate a datatype | 2011-12-30 | |
| | | | | added a DatatypeConstructor class | ||
* | problem fixed after CCI update | 2011-12-30 | |
| | |||
* | fixed problems with datatypes | 2011-12-29 | |
| | | | | | removed stale contracts in stratified inlining added test to datatypes | ||
* | Merge | 2011-12-28 | |
|\ | |||
* | | deleted some commented code | 2011-12-28 | |
| | | |||
| * | Add instrumentation for branches. | 2011-12-28 | |
|/ | |||
* | refactored AssertionInjector so that it works directly on bpl files as well | 2011-12-26 | |
| | |||
* | bug fix in houdini inlineDepth | 2011-12-06 | |
| | |||
* | Fixed bug when getting last source context in a method body. | 2011-12-06 | |
| | |||
* | Refactored translator so it can be called programmatically and return the | 2011-11-21 | |
| | | | | translated program in memory without writing it to disk. | ||
* | BCT: Initialize Boogie's command-line options object correctly before using | 2011-11-21 | |
| | | | | Boogie. | ||
* | commented calls to GC.Collect() | 2011-11-18 | |
| | |||
* | Translate AddressOf expressions correctly. | 2011-11-16 | |
| | | | | Fixes for problems when translating generic type parameters. | ||
* | Load all assemblies before doing anything else so that the unification for | 2011-11-16 | |
| | | | | | | | | | | the Core Assembly identity can happen correctly. Cache things in the sink based on the mangled name rather than the interned key: this prevents clashes in the Boogie program, but might mask some errors due to different types/members with the same full name (minus the assembly name of course). Translate generic parameters as Ref instead of Box if they are constrained to be a reference or struct (since we translate structs as Ref). [Experimental] | ||
* | For some reason, these didn't get into the last commit. | 2011-11-14 | |
| | |||
* | Trying to get the generics translation correct... | 2011-11-14 | |
| | |||
* | moved the addition of selectors and testers to program.Resolve | 2011-11-11 | |
| | |||
* | Many, many bug fixes related to generics and some other random problems. | 2011-11-10 | |
| | |||
* | change in model parsing with datatype values | 2011-11-07 | |
| | |||
* | Don't wipe out existing attributes when adding {:extern} | 2011-11-01 | |
| | |||
* | Major changes to the translator traversers because they now are based on the | 2011-10-31 | |
| | | | | | | | | new traversers. (The old ones have been marked as obsolete.) All types are now encoded as "datatypes" in Boogie. So non-generic types are nullary functions and generic types just have at least one type argument. Lots of other fixes: string encoding of names is now done by negating Boogie's regular expression for identifiers, etc. | ||
* | Fixed the generation of names for datatype functions to use the API for | 2011-10-31 | |
| | | | | | | getting SMT-approved names. Fixed a bug in VisitDistinctOp where a bad axiom was being generated when no grouping had more than one occurrence. | ||
* | Don't let /s be specified for stub files. (But keep the old code in case we | 2011-10-23 | |
| | | | | go back to it.) | ||
* | Fixed two bugs related to structs: now a struct that is declared without an | 2011-09-01 | |
| | | | | | | | | | | initial value is getting allocated. Also, deferring ctor calls within a struct ctor do *not* result in an attempt to allocate a new struct and assign it to "this". Restart the temporary variable counter on entry to each method. (This makes the regressions less noisy because a change in the number of temporaries created for one method will not change the names of the temporaries in other methods.) | ||
* | more string mangling | 2011-08-31 | |
| | |||
* | delegates/events implemented as multisets rather than linked lists | 2011-08-30 | |
| | |||
* | Merge | 2011-08-26 | |
|\ | |||
* | | a small bug in GeneralHeap translation | 2011-08-26 | |
| | | |||
| * | (phone)data on results of analyses on market apps | 2011-08-26 | |
| | | |||
* | | Merge | 2011-08-26 | |
|\| | |||
* | | some more string munging | 2011-08-26 | |
| | | |||
| * | (bct) removed ad-hoc string replacements, the problem is actually the encoding | 2011-08-25 | |
| | | |||
* | | fixed a bug: do not include the invoke procedure for thread delegates in the ↵ | 2011-08-25 | |
| | | | | | | | | set of initially declared procedures. The principle is that any procedure whose body will be created dynamically, its header should also be created dynamically | ||
* | | fixed bug | 2011-08-23 | |
|/ | |||
* | (phone bct) boolean binding of control enabledness ignored (for now) | 2011-08-22 | |
| | | | | tracking Page virtual overrides | ||
* | (phone bct) minor bugfixes found playing around with apps | 2011-08-19 | |
| | |||
* | continuned phone bct docs | 2011-08-19 | |
| | |||
* | fix in event translation for whole program analysis | 2011-08-17 | |
| | |||
* | Merge | 2011-08-17 | |
|\ | |||
* | | added RealModulus | 2011-08-17 | |
| | | |||
| * | (phone) documentation | 2011-08-17 | |
|/ | |||
* | (bct) skeleton of plugin infrastructure. for now the code is essentially the ↵ | 2011-08-16 | |
| | | | | | | same I will open a plugin branch to make more deeper changes until everything is stable | ||
* | (phone) fixed problem with unknown type anonymous controls | 2011-08-16 | |
| | |||
* | Merge | 2011-08-16 | |
|\ | |||
* | | saving navigation bad smells report | 2011-08-16 | |
| | |