| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
|
| |
|
|
|
|
| |
dictionaries are non-null, which is enforced by the implementation of Dictionary.
Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
|
| |
|
|
| |
Ignore duplicated else functions in models
|
| |
|
|
| |
Save and restore the value of Sink.RetVariable so that it doesn't get changed during the translation of a method body when new procedures end up getting declared during the translation.
|
| |
|
|
| |
Support for stub methods.
|
| | |
|
| |
|
|
| |
configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
|
| |
|
|
| |
and) verifiable
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
* Support for induction over more than 1 variable
* Added many of the Rippling induction benchmarks
* Fixed bug in case handling
|
| |
|
|
| |
(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.
|
| |
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
* 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)
|
| |
|
|
| |
the called ctor.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
| |
Fix a problem in two of the heaps where the AST for "type Type;" wasn't getting created.
|
| | |
|
| |
|
|
|
| |
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
|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Dafny: Forbid jumps from ghost code.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
| |
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.]
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
mikebarnett