summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
* Added support for stub methods. If a method definition is marked with a ↵Gravatar mikebarnett2011-03-06
| | | | | | custom attribute [Stub], then no procedure declaration is created for it. The user must make sure to provide Boogie with a file containing the procedure declaration. In addition, if the attribute has a string argument, [Stub("f")], then "f" is used as the nsame of the corresponding procedure instead of the encoded name computed from the method.
* Dafny:Gravatar rustanleino2011-03-06
| | | | | | * Support for induction over more than 1 variable * Added many of the Rippling induction benchmarks * Fixed bug in case handling
* In the Sink, keep track of any procedures defined in the initial program ↵Gravatar mikebarnett2011-03-06
| | | | (which is created by the heap when the initial Heap object is created). When the Sink is asked for a procedure corresponding to a method, if the method's encoded name matches any of the these procedures, then the matching procedure is returned.
* Changes needed to translate both contracts and method bodies. The Statement ↵Gravatar mikebarnett2011-03-05
| | | | | | | | and Expression traversers need to have a mode that controls two things: 1. Parameters occurring in contracts are translated as the corresponding in-parameter of the corresponding procedure. Parameters occurring in method bodies are translated as the corresponding out-parameter of the corresponding procedure. 2. Method calls in method bodies are translated as call commands. Method calls in contracts are translated as function calls.
* Dafny: Added heuristic for when to turn on the induction tacticGravatar rustanleino2011-03-05
|
* changes for dealing with delegatesGravatar qadeer2011-03-05
|
* Dafny:Gravatar rustanleino2011-03-04
| | | | | | * Add support for an {:induction} attribute on universal quantifiers over one bound variable. It causes the universally quantified formulas to be proved by induction. * For a user-defined function F, introduce not just F and F#limited, but also F#2 (which sits "above" F, just as F sits "above" F#limited) * In base case of SplitExpr, make use of F#2 functions (unless already inside an inlined predicate)
* Fix translation of "new" so that a procedure is generated (if needed) for ↵Gravatar mikebarnett2011-03-03
| | | | the called ctor.
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 01:27:27 +0000