summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
...
* Fix what looked like a serious design issue when Type checkingGravatar Dan Liew2015-02-12
| | | | | | | anything that implements the IAppliable interface. Type checking should never need to change the reference of a list of arguments (hence the removal of the ``ref`` keyword) and we need to use IList<Expr> instead of List<Expr> to allow NAryExpr to do its type checking.
* When an Expr immutable, never change Type reference if it has been set,Gravatar Dan Liew2015-02-12
| | | | even if the types are equivalent.
* 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.
* Fix performance issue in ComputeHashCode() methods of Expr classes.Gravatar Dan Liew2015-02-02
| | | | | | If constructing immutable Expr bottom up this would be very inefficient because the hashcode would be recomputed unnecessarily. Now just make ComputeHashCode() methods call GetHashCode() on Expr instead.
* Fix typechecking immutable Expr when we haveGravatar Dan Liew2015-01-31
| | | | | | | | | | | | <bool> == <bool> or <bool> != <bool> The type checker tries rewrite the Expr when it gets type checked which breaks immutability so disable doing this if the Expr is immutable.
* Made it produce slightly different passive commands for assignments to ↵Gravatar wuestholz2015-01-30
| | | | assumption variables.
* Minor change to the encoding of partially verified assertions as VCGravatar wuestholz2015-01-30
|
* Backed out changeset ed4196d6fe50Gravatar Dan Liew2015-01-29
| | | | | | Compilation does not depend NUnit.Runners so it should not be a required package. Instead users should install it manually as described in Source/UnitTests/README.md
* Make NUnit.Runners a require NuGet package again. This is anGravatar Dan Liew2015-01-29
| | | | | | attempt to unbreak the Jenkins build. I don't think doing this is ideal. The package isn't required to run tests, it's only required if you want to run them on the command line.
* Tweak the unit test documentation on Visual studio.Gravatar Dan Liew2015-01-29
|
* Try to fix the "out-of-the-box" build of Boogie under Visual Studio. It turnsGravatar Dan Liew2015-01-29
| | | | | | | | | | | | out we had the repository set up in "MSBuild-Integrated package" mode[1] (missing packages won't fetched unless the user explicitly allows it for the solution) but what we want is "Automatic package restore" (provided NuGet is setup correctly automatically fetch the missing packages). I've followed the migration guide [2] and it appears that now Visual Studio will try to automatically fetch after making this change. [1] http://docs.nuget.org/consume/package-restore [2] http://docs.nuget.org/Consume/Package-Restore/Migrating-to-Automatic-Package-Restore
* Improve documentation on testing.Gravatar Dan Liew2015-01-29
|
* Made the trace output for the caching more detailed.Gravatar wuestholz2015-01-29
|
* Add unit tests to check that ComputeHashCode() and GetHashCode() agreeGravatar Dan Liew2015-01-29
| | | | for BvExtractExpr, BvConcatExpr and OldExpr.
* Add unit tests to check that ComputeHashCode() and GetHashCode() agreeGravatar Dan Liew2015-01-29
| | | | for LiteralExpr, IdentifierExpr and NAryExpr.
* Protect the body of ForAllExpr, ExistsExpr and LambdaExpr when theyGravatar Dan Liew2015-01-29
| | | | are immutable. Add unit tests to check this.
* Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possibleGravatar Dan Liew2015-01-29
| | | | to set them as immutable (not currently enforced for these Expr types).
* Protect the NAryExpr.Fun field when the NAryExpr is immutable.Gravatar Dan Liew2015-01-29
| | | | | Add a unit test for this. We need to protect the Args field too but that is going to be much harder to enforce.
* Protect the Expr field of OldExpr if it is immutable. Add unit testGravatar Dan Liew2015-01-29
| | | | to check this is being enforced.
* Add some unit tests to check the enforcement of Expr immutability.Gravatar Dan Liew2015-01-29
| | | | | | | For IdentifierExpr and the Type field of Expr. There are lots of places where it still isn't enforced but hopefully we'll fix those in due time.
* Protect the Type field of an Expr if is Immutable. Note if the ExprGravatar Dan Liew2015-01-29
| | | | | | has never been type checked we allow the Type field to be set but once it has been set it cannot be changed to refer to a different Type.
* Protect the Name and Decl fields of IdentifierExpr when it isGravatar Dan Liew2015-01-29
| | | | | immutable by raising an exception if an attempt is made to modify it after construction.
* Prevent a BvConst being changed once constructed. The motivationGravatar Dan Liew2015-01-29
| | | | | | | for doing this is that we would like a LiteralExpr to be immutable when constructed but because the "Val" field can point to a BvConst which is an object it means that although the Val reference cannot change the BvConst could be changed.
* Add the ability to declare Expr to be immutable at construction time.Gravatar Dan Liew2015-01-29
| | | | | | | | | | | | This is currently not enforced (it really should be). So right now it only amounts to a promise by the client that the Expr will not be modified after it is constructed. We should actually enforce this by protecting various fields of the Expr classes so they can't be changed if an Expr is constructed as Immutable. The motivation for doing this is it allows the value of GetHashCode() to be cached. Expr classes now implement ComputeHashCode() to do the actuall hash code computation.
* Handle timeout in refinement loopGravatar akashlal2015-01-28
|
* Fixed minor issue.Gravatar wuestholz2015-01-26
|
* Worked on the verification result caching (statement checksums).Gravatar wuestholz2015-01-26
|
* Minor changeGravatar wuestholz2015-01-26
|
* Minor changeGravatar wuestholz2015-01-26
|
* Worked on the verification result caching (trace output).Gravatar wuestholz2015-01-26
|
* Change the return type of StandardVisitor.VisitLiteralExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | LiteralExpr to Expr. Enforcing the return type be LiteralExpr is too restrictive. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitExistsExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | ExistsExpr to Expr. Enforcing the return type be ExistsExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitForAllExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | ForAllExpr to Expr. Enforcing the return type be ForAllExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitBvExtractExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | BvExtractExpr to Expr. Enforcing the return type be BvExtractExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
* Change the return type of StandardVisitor.VisitBvConcatExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | BvConcatExpr to Expr. Enforcing the return type be BvConcatExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type.
* Worked on the verification result caching (use weights for extracted functions).Gravatar wuestholz2015-01-24
|
* Worked on the verification result caching (use native support for partially ↵Gravatar wuestholz2015-01-16
| | | | verified assertions).
* Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-23
|
* MergeGravatar Ally Donaldson2015-01-22
|\
* | Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-22
| |
| * MergeGravatar qadeer2015-01-16
| |\ | |/ |/|
| * removed "layer" attribute from the desugared programGravatar qadeer2015-01-16
| |
* | Worked on StagedHoudiniGravatar Ally Donaldson2015-01-16
| |
* | Fix related to limitations in CVC4 model parsingGravatar Ally Donaldson2015-01-14
| |
* | MergeGravatar Ally Donaldson2015-01-13
|\ \
| * \ Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
| |\ \
| * \ \ Merging changes from 0biha/BoogieInvariantFixesIIIaGravatar wuestholz2015-01-13
| |\ \ \ | | |_|/ | |/| |
* | | | Removed unnecessary stage-related attributes from candidate annotations.Gravatar Ally Donaldson2015-01-10
| | | |
| | | * Made 2 invariants of class 'VariableCollector' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field protected - exposing IEnumerables (with help from David Rohr)
| | | * Made invariant of class 'Trigger' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - adding getter/setter - copying incoming list - exposing read-only list (with help from David Rohr)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 09:49:55 +0000