summaryrefslogtreecommitdiff
path: root/Source/Core/Absy.cs
Commit message (Collapse)AuthorAge
* Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
|
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
|
* fix for deterministicExtractLoops for nested loopsGravatar Shuvendu Lahiri2015-10-27
|
* Bug fix for deterministExtractLoops for Shaobo's exampleGravatar Shuvendu Lahiri2015-10-26
|
* fix for /deterministicExtractLoops sed in SymDiffGravatar Shuvendu Lahiri2015-07-19
|
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-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.Gravatar Valentin Wüstholz2015-06-12
|
* Make caching of verification results more fine-grained for changes that ↵Gravatar Valentin Wüstholz2015-05-17
| | | | affect preconditions.
* Protect the Args field of NAryExpr when it is immutable.Gravatar Dan Liew2015-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.Gravatar wuestholz2015-01-26
|
* Minor changeGravatar wuestholz2015-01-26
|
* MergeGravatar Ally Donaldson2015-01-13
|\
| * Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
| |\
* | | Removed unnecessary stage-related attributes from candidate annotations.Gravatar Ally Donaldson2015-01-10
| | |
| | * Made invariant of class 'QKeyValue' robust by:Gravatar wuestholz2015-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'.Gravatar 0biha2015-01-08
| |
| * Made 2 invariants of class 'DeclWithFormals' robust by changing the designGravatar 0biha2015-01-07
| | | | | | | | (replaced public fields by private fields + getters/setters)
| * Rewrote 'globalVariablesCache' invariant fix of class 'Program'Gravatar 0biha2015-01-08
| |
| * Made invariant of class 'Constant' robust by making list 'Parents' read-onlyGravatar 0biha2015-01-05
| |
| * Made invariant of class 'AtomicRE' robust by changing the designGravatar 0biha2015-01-05
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made invariant of class 'Program' robust by making the GlobalVariables cache ↵Gravatar 0biha2014-12-27
| | | | | | | | read-only.
| * Made invariants of classes 'Requires' and 'Ensures' robust by making ↵Gravatar 0biha2014-12-27
|/ | | | 'IPotentialErrorNode' generic.
* Merging changes from 0biha/BoogieInvariantFixesIIGravatar wuestholz2014-12-27
|\
| * Made invariant of class 'ProcedureSummaryEntry' robust by changing the designGravatar 0biha2014-12-23
| | | | | | | | (replaced public field by private field + getter/setter).
| * Made invariant of class 'Ensures' robust by changing the design (replaced ↵Gravatar 0biha2014-12-19
| | | | | | | | public field by private field + getter/setter).
* | MergeGravatar 0biha2014-12-16
|\|
| * Fixed a precondition.Gravatar wuestholz2014-12-16
| |
* | Made 2 invariants of class 'Sequential' robust by changing the design ↵Gravatar 0biha2014-12-15
| | | | | | | | (replaced public fields by private fields + getters/setters).
* | Made invariant of class 'Choice' robust by changing the design (replaced ↵Gravatar 0biha2014-12-15
| | | | | | | | public field by private field + getter/setter).
* | Made 2 invariants of class 'TypepedIdent' robust by changing the design ↵Gravatar 0biha2014-12-15
| | | | | | | | (replaced public fields by private fields + getters/setters).
* | Made invariant of class 'Requires' robust by changing the design (replaced ↵Gravatar 0biha2014-12-15
| | | | | | | | public field by private field + getter/setter).
* | Made invariant of class 'Variable' robust by changing the design (replaced ↵Gravatar 0biha2014-12-09
| | | | | | | | public field by private field + getter/setter).
* | Made 2 invariants of class 'TypeSynonymDecl' robust by changing the design ↵Gravatar 0biha2014-12-09
| | | | | | | | (replaced public fields by private fields + getters/setters).
* | Made expression invariant of class 'Axiom' robust by changing the design ↵Gravatar 0biha2014-12-09
| | | | | | | | (replaced public field by getter/setter).
* | Made invariant of class 'Program' robust byGravatar 0biha2014-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 ↵Gravatar 0biha2014-12-09
|/ | | | getter/setter instead of public field).
* Optimized the VC generation for assumption variables.Gravatar wuestholz2014-12-07
|
* Worked on the verification result caching (extracted functions).Gravatar wuestholz2014-11-25
|
* Worked on the verification result caching.Gravatar wuestholz2014-11-23
|
* Fixed issue in the verification result caching.Gravatar wuestholz2014-11-10
|
* Did some refactoring.Gravatar wuestholz2014-10-18
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-17
|
* Did some refactoring.Gravatar wuestholz2014-10-16
|
* Fix issue in computation of checksums for indented statements.Gravatar wuestholz2014-10-15
|
* Fix typos in the name of a property and method used for handlingGravatar Dan Liew2014-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.
* MergeGravatar akashlal2014-09-27
|\
* | Better fix for the duplicator, thanks to wuestholzGravatar akashlal2014-09-27
| |
| * Fixed issue reported by Akash Lal.Gravatar wuestholz2014-09-26
|/
* The setter is better this wayGravatar akashlal2014-09-25
|
* Lets have a setter for TopLevelDeclarations as wellGravatar akashlal2014-09-25
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 16:38:50 +0000