Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Made it unnecessary to set the types on the Boogie ASTs as we create them. | 2011-03-03 | |
| | | | | | | Added support for string literals. Translating structs no longer crashes the translator, but on the other hand, they are just skipped and not translated... Added a helper method to make sure that generated identifiers are Boogie-legal. | ||
* | Create a static constructor only for types that don't already define one. | 2011-03-02 | |
| | | | | Fix a problem in two of the heaps where the AST for "type Type;" wasn't getting created. | ||
* | put the call to CreateStaticConstructor back in | 2011-03-02 | |
| | |||
* | some fixes | 2011-03-02 | |
| | | | | | 1. introduced ProcedureInfo for packaging up relevant information about a Procedure 2. removed the call to the code that generates the static class constructor. this is temporarily broken; have to discuss with mike | ||
* | Fix null-equivalent initialization of fields so that instance fields are ↵ | 2011-03-02 | |
| | | | | initialized in instance constructors and static fields are initialized in static constructors. Added wrinkle is that compiler generates a static constructor only if it needs to, so if there isn't one, we create one. | ||
* | fixes for splitFields option | 2011-03-02 | |
| | |||
* | Use the Sink's API for creating a procedure for the Invoke method of a delegate. | 2011-03-01 | |
| | |||
* | Fixed many bugs. | 2011-03-01 | |
| | | | | | | Ctors now initialize all fields to default (null-equivalent) values. Generate procedures for interface methods. Translate enums just by ignoring them and using the integers that they really are. | ||
* | Boogie build succeeded, 4 test(s) failed | 2011-03-01 | |
| | |||
* | Dafny: support for nested match expressions | 2011-03-01 | |
| | |||
* | Updates to Answer files from recent changes | 2011-03-01 | |
| | |||
* | Boogie build succeeded, 5 test(s) failed | 2011-02-27 | |
| | |||
* | Dafny: Non-empty Visual-Studio error messages for related split-expr locations. | 2011-02-27 | |
| | | | | Dafny: Forbid jumps from ghost code. | ||
* | Fixed dynamic dispatch so the most derived override is called for each subtype. | 2011-02-25 | |
| | |||
* | two bug fixes | 2011-02-25 | |
| | |||
* | implemented delegates and events | 2011-02-25 | |
| | |||
* | Added a new type, Type, that represents runtime types. The Heap interface ↵ | 2011-02-24 | |
| | | | | | | now provides a way to declare a new user-defined type and to represent the expressions "typeof(T)" or "o.Type" in the BPL program using a new function $DynamicType. Added a method to the Sink so that any of the translation visitors can find or declare a new type. When an object is allocated, an assumption is generated that gives its dynamic type. Fixed the dynamic dispatch inlining so that the $DynamicType of the object is used to decide which override to call. | ||
* | Boogie build succeeded, 4 test(s) failed | 2011-02-24 | |
| | |||
* | Changed calls to Debug.Assert to Contract.Assert. | 2011-02-24 | |
| | | | | | Suppress source contexts for empty statements. Added a "whole program" option. When that is specified, then virtual calls are translated into a series of if-statements that test the dynamic type of the receiver and call the appropriate method. This is done only for subtypes that are defined in the CUA (Code Under Analysis -- which currently consists of just the one assembly being translated). [Note: currently the dynamic type is not implemented. That is next.] | ||
* | Mimic Z3 logic for figuring out the blocking clause for the next counterexample | 2011-02-23 | |
| | |||
* | Don't ever put a label under a quantifier. | 2011-02-23 | |
| | |||
* | Add MULTI_TRACES prover option (equivalent of /z3multipleErrors) | 2011-02-23 | |
| | |||
* | Add IEnumerable.Concat1 method. | 2011-02-23 | |
| | |||
* | Add tests for -z3multipleErrors from Shuvendu. | 2011-02-23 | |
| | |||
* | Fix build by adding missing project. | 2011-02-23 | |
| | |||
* | Boogie build succeeded, 4 test(s) failed | 2011-02-23 | |
| | |||
* | Boogie build succeeded, 26 test(s) failed | 2011-02-23 | |
| | |||
* | Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly ↵ | 2011-02-23 | |
| | | | | different syntax in SMT than in Simplify | ||
* | Check for timeout/memoryout | 2011-02-23 | |
| | |||
* | Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq ↵ | 2011-02-23 | |
| | | | | thing in Simplify frontend) | ||
* | Don't try to declare bv types | 2011-02-23 | |
| | |||
* | Dispose of the prover when Close() is called. | 2011-02-23 | |
| | |||
* | Add workaround for cmd race | 2011-02-23 | |
| | |||
* | Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!) | 2011-02-23 | |
| | |||
* | Pass solverarguments | 2011-02-23 | |
| | |||
* | Do typed->untyped translation for -mv variables | 2011-02-23 | |
| | |||
* | Provide dummy implementation of FlushAxiomsToTheoremProver() | 2011-02-23 | |
| | |||
* | Handle as-array[...] model elements | 2011-02-23 | |
| | |||
* | Fixes in /useArrayTheory handling | 2011-02-23 | |
| | |||
* | Parse else-> clauses in the model | 2011-02-23 | |
| | | | | Disable MODEL_PARTIAL in SMTLib | ||
* | Throw exceptions when push/pop interface is used but not implemented | 2011-02-23 | |
| | | | | Complete ErrorModel tables with the final bogus else clause | ||
* | Pass :skolemid to SMTLib prover | 2011-02-23 | |
| | |||
* | Implement Push/Pop interface. | 2011-02-23 | |
| | | | | Implement ProverContext.Lookup method. | ||
* | Allow recent Z3 versions to be used | 2011-02-21 | |
| | |||
* | Move model printing to ErrorModel class | 2011-02-21 | |
| | | | | Allow construction of ErrorModel instance from Model instance | ||
* | Per SMT standard push requires an argument | 2011-02-21 | |
| | |||
* | Add some ExpertLevel functions | 2011-02-21 | |
| | |||
* | Set Id of Elements. | 2011-02-21 | |
| | | | | Add some explanation at the beginning of the file. | ||
* | Dafny: Improved scheme for splitting expressions. Also, report each split ↵ | 2011-02-19 | |
| | | | | in error messages. | ||
* | Print prover errors on stdout (same as prover warnings) | 2011-02-18 | |
| |