summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
|
* Fix Sink.FindOrCreateProcedure so that it takes an IMethodDefinition instead ↵Gravatar mikebarnett2011-03-06
| | | | of an IMethodReference so it is guaranteed to know if the method is static or not and also to be able to access its parameters as IParameterDefinitions which is needed to know if they are out params or not.
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 10:44:05 +0000