Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Protect the Args field of NAryExpr when it is immutable. | 2015-02-12 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Made changing the reference throw an exception if the NAryExpr was constructed as immutable * Changed the type of NAryExpr.Args to be IList<Expr> rather than List<Expr> so that when the NAryExpr is immutable I can return ``_Args.AsReadOnly()`` (instead of ``_Args``) which returns a read only wrapper around the List<Expr> so that clients cannot change the list. I came across two problems * Making this change required changing types all over the place (from List<Expr> to IList<Expr>). I feel that changes are extensive enough that there's a good chance that out of tree clients using Boogie's libraries might break. I've waited for a code review but this didn't happen so I'm committing anyway. * I came across something that looks like bad design of the IAppliable interface which potentially breaks immutability enforcement. I've left this as a "FIXME" in this. Here's the problematic method. ``` Type Typecheck(ref List<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc); ``` It potentially allows the instance of the args to be changed which seems very suspect. | ||
* | Fixed minor issue. | 2015-01-26 | |
| | |||
* | Minor change | 2015-01-26 | |
| | |||
* | Merge | 2015-01-13 | |
|\ | |||
| * | Merging changes from wuestholz/BoogieInvariantFixesIIII | 2015-01-13 | |
| |\ | |||
* | | | Removed unnecessary stage-related attributes from candidate annotations. | 2015-01-10 | |
| | | | |||
| | * | Made invariant of class 'QKeyValue' robust by: | 2015-01-09 | |
| |/ |/| | | | | | | | | | | | | | - making field private - exposing read-only list - copying incoming list - adding methods 'AddParam', 'AddParams', and 'ClearParams' (with help from David Rohr) | ||
| * | Fixed a null reference problem in class 'Constant'. | 2015-01-08 | |
| | | |||
| * | Made 2 invariants of class 'DeclWithFormals' robust by changing the design | 2015-01-07 | |
| | | | | | | | | (replaced public fields by private fields + getters/setters) | ||
| * | Rewrote 'globalVariablesCache' invariant fix of class 'Program' | 2015-01-08 | |
| | | |||
| * | Made invariant of class 'Constant' robust by making list 'Parents' read-only | 2015-01-05 | |
| | | |||
| * | Made invariant of class 'AtomicRE' robust by changing the design | 2015-01-05 | |
| | | | | | | | | (replaced public field by private field + getter/setter) | ||
| * | Made invariant of class 'Program' robust by making the GlobalVariables cache ↵ | 2014-12-27 | |
| | | | | | | | | read-only. | ||
| * | Made invariants of classes 'Requires' and 'Ensures' robust by making ↵ | 2014-12-27 | |
|/ | | | | 'IPotentialErrorNode' generic. | ||
* | Merging changes from 0biha/BoogieInvariantFixesII | 2014-12-27 | |
|\ | |||
| * | Made invariant of class 'ProcedureSummaryEntry' robust by changing the design | 2014-12-23 | |
| | | | | | | | | (replaced public field by private field + getter/setter). | ||
| * | Made invariant of class 'Ensures' robust by changing the design (replaced ↵ | 2014-12-19 | |
| | | | | | | | | public field by private field + getter/setter). | ||
* | | Merge | 2014-12-16 | |
|\| | |||
| * | Fixed a precondition. | 2014-12-16 | |
| | | |||
* | | Made 2 invariants of class 'Sequential' robust by changing the design ↵ | 2014-12-15 | |
| | | | | | | | | (replaced public fields by private fields + getters/setters). | ||
* | | Made invariant of class 'Choice' robust by changing the design (replaced ↵ | 2014-12-15 | |
| | | | | | | | | public field by private field + getter/setter). | ||
* | | Made 2 invariants of class 'TypepedIdent' robust by changing the design ↵ | 2014-12-15 | |
| | | | | | | | | (replaced public fields by private fields + getters/setters). | ||
* | | Made invariant of class 'Requires' robust by changing the design (replaced ↵ | 2014-12-15 | |
| | | | | | | | | public field by private field + getter/setter). | ||
* | | Made invariant of class 'Variable' robust by changing the design (replaced ↵ | 2014-12-09 | |
| | | | | | | | | public field by private field + getter/setter). | ||
* | | Made 2 invariants of class 'TypeSynonymDecl' robust by changing the design ↵ | 2014-12-09 | |
| | | | | | | | | (replaced public fields by private fields + getters/setters). | ||
* | | Made expression invariant of class 'Axiom' robust by changing the design ↵ | 2014-12-09 | |
| | | | | | | | | (replaced public field by getter/setter). | ||
* | | Made invariant of class 'Program' robust by | 2014-12-09 | |
| | | | | | | | | | | | | -adding various preconditions -removing null elements in the setter -using the "ReadOnlyList" wrapper. | ||
* | | Made invariant of class 'Absy' robust by changing the design (added ↵ | 2014-12-09 | |
|/ | | | | getter/setter instead of public field). | ||
* | Optimized the VC generation for assumption variables. | 2014-12-07 | |
| | |||
* | Worked on the verification result caching (extracted functions). | 2014-11-25 | |
| | |||
* | Worked on the verification result caching. | 2014-11-23 | |
| | |||
* | Fixed issue in the verification result caching. | 2014-11-10 | |
| | |||
* | Did some refactoring. | 2014-10-18 | |
| | |||
* | Worked on the verification result caching. | 2014-10-17 | |
| | |||
* | Did some refactoring. | 2014-10-16 | |
| | |||
* | Fix issue in computation of checksums for indented statements. | 2014-10-15 | |
| | |||
* | Fix typos in the name of a property and method used for handling | 2014-10-08 | |
| | | | | | | Absy metadata. This feature is very new so it is unlikely any out of tree code (apart from my own) is using it so this change shouldn't be disruptive. | ||
* | Merge | 2014-09-27 | |
|\ | |||
* | | Better fix for the duplicator, thanks to wuestholz | 2014-09-27 | |
| | | |||
| * | Fixed issue reported by Akash Lal. | 2014-09-26 | |
|/ | |||
* | The setter is better this way | 2014-09-25 | |
| | |||
* | Lets have a setter for TopLevelDeclarations as well | 2014-09-25 | |
| | |||
* | Did more refactoring and addressed several todos. | 2014-09-23 | |
| | |||
* | Did more refactoring. | 2014-09-23 | |
| | |||
* | Did some refactoring. | 2014-09-23 | |
| | |||
* | Fixed an issue in the verification result caching (recycled errors). | 2014-09-22 | |
| | |||
* | fixed various CodeContracts issues. | 2014-09-18 | |
| | |||
* | Added the ability to attach arbitary objects to Absy nodes using an | 2014-09-03 | |
| | | | | | | | | | | | | | | | | | | | | | | integer as a key. This allows any arbitrary "metadata" to be attached at runtime. The implementation is lazy so the container is only created if the SetMetadata<T>() method is called which should keep the memory overhead very minimal. Example usage: var TheAssert = new AssertCmd(...); ... TheAssert.SetMetadata(0, new List<Expr>()); TheAssert.GetMetadata<List<Expr>>(0); foreach (var keyValue in TheAssert.NumberedMetaData) { // do something } Debug.Assert(TheAssert.NumberedMetaDataCount == 1); | ||
* | Minor refactoring | 2014-08-03 | |
| | |||
* | Fix bug where Visitors could not visit Requires or Ensures because | 2014-07-27 | |
| | | | | the StdDispatch method was missing on both Classes. |