summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Made it unnecessary to set the types on the Boogie ASTs as we create them.Gravatar mikebarnett2011-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.Gravatar mikebarnett2011-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 inGravatar qadeer2011-03-02
|
* some fixesGravatar qadeer2011-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 ↵Gravatar mikebarnett2011-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 optionGravatar qadeer2011-03-02
|
* Use the Sink's API for creating a procedure for the Invoke method of a delegate.Gravatar mikebarnett2011-03-01
|
* Fixed many bugs.Gravatar mikebarnett2011-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) failedGravatar codeplexbot2011-03-01
|
* Dafny: support for nested match expressionsGravatar rustanleino2011-03-01
|
* Updates to Answer files from recent changesGravatar rustanleino2011-03-01
|
* Boogie build succeeded, 5 test(s) failedGravatar codeplexbot2011-02-27
|
* Dafny: Non-empty Visual-Studio error messages for related split-expr locations.Gravatar rustanleino2011-02-27
| | | | Dafny: Forbid jumps from ghost code.
* Fixed dynamic dispatch so the most derived override is called for each subtype.Gravatar mikebarnett2011-02-25
|
* two bug fixesGravatar qadeer2011-02-25
|
* implemented delegates and eventsGravatar qadeer2011-02-25
|
* Added a new type, Type, that represents runtime types. The Heap interface ↵Gravatar mikebarnett2011-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) failedGravatar codeplexbot2011-02-24
|
* Changed calls to Debug.Assert to Contract.Assert.Gravatar mikebarnett2011-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 counterexampleGravatar MichalMoskal2011-02-23
|
* Don't ever put a label under a quantifier.Gravatar MichalMoskal2011-02-23
|
* Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)Gravatar MichalMoskal2011-02-23
|
* Add IEnumerable.Concat1 method.Gravatar MichalMoskal2011-02-23
|
* Add tests for -z3multipleErrors from Shuvendu.Gravatar MichalMoskal2011-02-23
|
* Fix build by adding missing project.Gravatar mikebarnett2011-02-23
|
* Boogie build succeeded, 4 test(s) failedGravatar codeplexbot2011-02-23
|
* Boogie build succeeded, 26 test(s) failedGravatar codeplexbot2011-02-23
|
* Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly ↵Gravatar MichalMoskal2011-02-23
| | | | different syntax in SMT than in Simplify
* Check for timeout/memoryoutGravatar MichalMoskal2011-02-23
|
* Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq ↵Gravatar MichalMoskal2011-02-23
| | | | thing in Simplify frontend)
* Don't try to declare bv typesGravatar MichalMoskal2011-02-23
|
* Dispose of the prover when Close() is called.Gravatar MichalMoskal2011-02-23
|
* Add workaround for cmd raceGravatar MichalMoskal2011-02-23
|
* Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!)Gravatar MichalMoskal2011-02-23
|
* Pass solverargumentsGravatar MichalMoskal2011-02-23
|
* Do typed->untyped translation for -mv variablesGravatar MichalMoskal2011-02-23
|
* Provide dummy implementation of FlushAxiomsToTheoremProver()Gravatar MichalMoskal2011-02-23
|
* Handle as-array[...] model elementsGravatar MichalMoskal2011-02-23
|
* Fixes in /useArrayTheory handlingGravatar MichalMoskal2011-02-23
|
* Parse else-> clauses in the modelGravatar MichalMoskal2011-02-23
| | | | Disable MODEL_PARTIAL in SMTLib
* Throw exceptions when push/pop interface is used but not implementedGravatar MichalMoskal2011-02-23
| | | | Complete ErrorModel tables with the final bogus else clause
* Pass :skolemid to SMTLib proverGravatar MichalMoskal2011-02-23
|
* Implement Push/Pop interface.Gravatar MichalMoskal2011-02-23
| | | | Implement ProverContext.Lookup method.
* Allow recent Z3 versions to be usedGravatar MichalMoskal2011-02-21
|
* Move model printing to ErrorModel classGravatar MichalMoskal2011-02-21
| | | | Allow construction of ErrorModel instance from Model instance
* Per SMT standard push requires an argumentGravatar MichalMoskal2011-02-21
|
* Add some ExpertLevel functionsGravatar MichalMoskal2011-02-21
|
* Set Id of Elements.Gravatar MichalMoskal2011-02-21
| | | | Add some explanation at the beginning of the file.
* Dafny: Improved scheme for splitting expressions. Also, report each split ↵Gravatar rustanleino2011-02-19
| | | | in error messages.
* Print prover errors on stdout (same as prover warnings)Gravatar MichalMoskal2011-02-18
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-01 01:45:06 +0000