Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add simplified may-unverified analysis and instrumentation. | 2015-11-20 | |
| | |||
* | Add support for identifying unnecessary assumes. | 2015-11-16 | |
| | |||
* | fix for deterministicExtractLoops for nested loops | 2015-10-27 | |
| | |||
* | Bug fix for deterministExtractLoops for Shaobo's example | 2015-10-26 | |
| | |||
* | fix for /deterministicExtractLoops sed in SymDiff | 2015-07-19 | |
| | |||
* | Normalise line endings using a .gitattributes file. Unfortunately | 2015-06-28 | |
| | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. | ||
* | Fix issue with computation of statement checksums for lambda expressions. | 2015-06-12 | |
| | |||
* | Make caching of verification results more fine-grained for changes that ↵ | 2015-05-17 | |
| | | | | affect preconditions. | ||
* | 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 | |
| |