Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add simplified may-unverified analysis and instrumentation. | Valentin Wüstholz | 2015-11-20 |
| | |||
* | Add support for identifying unnecessary assumes. | Valentin Wüstholz | 2015-11-16 |
| | |||
* | fix for deterministicExtractLoops for nested loops | Shuvendu Lahiri | 2015-10-27 |
| | |||
* | Bug fix for deterministExtractLoops for Shaobo's example | Shuvendu Lahiri | 2015-10-26 |
| | |||
* | fix for /deterministicExtractLoops sed in SymDiff | Shuvendu Lahiri | 2015-07-19 |
| | |||
* | Normalise line endings using a .gitattributes file. Unfortunately | Dan Liew | 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. | Valentin Wüstholz | 2015-06-12 |
| | |||
* | Make caching of verification results more fine-grained for changes that ↵ | Valentin Wüstholz | 2015-05-17 |
| | | | | affect preconditions. | ||
* | Protect the Args field of NAryExpr when it is immutable. | Dan Liew | 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. | wuestholz | 2015-01-26 |
| | |||
* | Minor change | wuestholz | 2015-01-26 |
| | |||
* | Merge | Ally Donaldson | 2015-01-13 |
|\ | |||
| * | Merging changes from wuestholz/BoogieInvariantFixesIIII | wuestholz | 2015-01-13 |
| |\ | |||
* | | | Removed unnecessary stage-related attributes from candidate annotations. | Ally Donaldson | 2015-01-10 |
| | | | |||
| | * | Made invariant of class 'QKeyValue' robust by: | wuestholz | 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'. | 0biha | 2015-01-08 |
| | | |||
| * | Made 2 invariants of class 'DeclWithFormals' robust by changing the design | 0biha | 2015-01-07 |
| | | | | | | | | (replaced public fields by private fields + getters/setters) | ||
| * | Rewrote 'globalVariablesCache' invariant fix of class 'Program' | 0biha | 2015-01-08 |
| | | |||
| * | Made invariant of class 'Constant' robust by making list 'Parents' read-only | 0biha | 2015-01-05 |
| | | |||
| * | Made invariant of class 'AtomicRE' robust by changing the design | 0biha | 2015-01-05 |
| | | | | | | | | (replaced public field by private field + getter/setter) | ||
| * | Made invariant of class 'Program' robust by making the GlobalVariables cache ↵ | 0biha | 2014-12-27 |
| | | | | | | | | read-only. | ||
| * | Made invariants of classes 'Requires' and 'Ensures' robust by making ↵ | 0biha | 2014-12-27 |
|/ | | | | 'IPotentialErrorNode' generic. | ||
* | Merging changes from 0biha/BoogieInvariantFixesII | wuestholz | 2014-12-27 |
|\ | |||
| * | Made invariant of class 'ProcedureSummaryEntry' robust by changing the design | 0biha | 2014-12-23 |
| | | | | | | | | (replaced public field by private field + getter/setter). | ||
| * | Made invariant of class 'Ensures' robust by changing the design (replaced ↵ | 0biha | 2014-12-19 |
| | | | | | | | | public field by private field + getter/setter). | ||
* | | Merge | 0biha | 2014-12-16 |
|\| | |||
| * | Fixed a precondition. | wuestholz | 2014-12-16 |
| | | |||
* | | Made 2 invariants of class 'Sequential' robust by changing the design ↵ | 0biha | 2014-12-15 |
| | | | | | | | | (replaced public fields by private fields + getters/setters). | ||
* | | Made invariant of class 'Choice' robust by changing the design (replaced ↵ | 0biha | 2014-12-15 |
| | | | | | | | | public field by private field + getter/setter). | ||
* | | Made 2 invariants of class 'TypepedIdent' robust by changing the design ↵ | 0biha | 2014-12-15 |
| | | | | | | | | (replaced public fields by private fields + getters/setters). | ||
* | | Made invariant of class 'Requires' robust by changing the design (replaced ↵ | 0biha | 2014-12-15 |
| | | | | | | | | public field by private field + getter/setter). | ||
* | | Made invariant of class 'Variable' robust by changing the design (replaced ↵ | 0biha | 2014-12-09 |
| | | | | | | | | public field by private field + getter/setter). | ||
* | | Made 2 invariants of class 'TypeSynonymDecl' robust by changing the design ↵ | 0biha | 2014-12-09 |
| | | | | | | | | (replaced public fields by private fields + getters/setters). | ||
* | | Made expression invariant of class 'Axiom' robust by changing the design ↵ | 0biha | 2014-12-09 |
| | | | | | | | | (replaced public field by getter/setter). | ||
* | | Made invariant of class 'Program' robust by | 0biha | 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 ↵ | 0biha | 2014-12-09 |
|/ | | | | getter/setter instead of public field). | ||
* | Optimized the VC generation for assumption variables. | wuestholz | 2014-12-07 |
| | |||
* | Worked on the verification result caching (extracted functions). | wuestholz | 2014-11-25 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-11-23 |
| | |||
* | Fixed issue in the verification result caching. | wuestholz | 2014-11-10 |
| | |||
* | Did some refactoring. | wuestholz | 2014-10-18 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-10-17 |
| | |||
* | Did some refactoring. | wuestholz | 2014-10-16 |
| | |||
* | Fix issue in computation of checksums for indented statements. | wuestholz | 2014-10-15 |
| | |||
* | Fix typos in the name of a property and method used for handling | Dan Liew | 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 | akashlal | 2014-09-27 |
|\ | |||
* | | Better fix for the duplicator, thanks to wuestholz | akashlal | 2014-09-27 |
| | | |||
| * | Fixed issue reported by Akash Lal. | wuestholz | 2014-09-26 |
|/ | |||
* | The setter is better this way | akashlal | 2014-09-25 |
| | |||
* | Lets have a setter for TopLevelDeclarations as well | akashlal | 2014-09-25 |
| |