summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
* 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.
* minor fix to the golden fileGravatar qadeer2015-01-28
|
* added lit stuff at the top of the file and the golden outputGravatar qadeer2015-01-28
|
* Work stealing queue (PLDI '12 Vechev et al.)Gravatar Unknown2015-01-28
|
* Handle timeout in refinement loopGravatar akashlal2015-01-28
|
* MergeGravatar qadeer2015-01-27
|\
* | removed unused functions and axioms to make the verification fasterGravatar qadeer2015-01-27
| |
| * 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)
| | | * Made invariant of class 'StmtList' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private and readonly - exposing IEnumerable - adding 'AddLabel' method (with help from David Rohr)
| | | * Made invariant of class 'StmtList' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - adding private field - exposing read-only list - copying incoming list (with help from David Rohr)
| | | * 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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 06:10:32 +0000