summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Collapse)AuthorAge
* Rename DLLs to non-generic names by prefixing "Boogie". Project names andGravatar akashlal2016-04-15
| | | | namespaces remain the same.
* Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
|
* Fix issue with partially-verified assertions.Gravatar Valentin Wüstholz2015-11-19
|
* Add experimental support for optimization (requires Z3 build after changeset ↵Gravatar Valentin Wüstholz2015-11-18
| | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
|
* Document the new behaviour of the ``-proc:`` command line optionGravatar Dan Liew2015-10-31
| | | | in the output of Boogie's help.
* Added wild card matching for /proc flagGravatar Shaobo2015-10-31
|
* fix for deterministicExtractLoops for nested loopsGravatar Shuvendu Lahiri2015-10-27
|
* Bug fix for deterministExtractLoops for Shaobo's exampleGravatar Shuvendu Lahiri2015-10-26
|
* updateGravatar Shaz Qadeer2015-09-28
|
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2015-08-28
|\ | | | | | | | | | | | | | | | | | | Conflicts: Source/Core/CommandLineOptions.cs Source/ExecutionEngine/ExecutionEngine.cs Source/ExecutionEngine/VerificationResultCache.cs Source/VCGeneration/VC.cs Test/snapshots/runtest.snapshot Test/snapshots/runtest.snapshot.expect
* | Added /verifySnapshots:3, which prints recycled errors messages with the ↵Gravatar Rustan Leino2015-08-28
| | | | | | | | source locations of the new code.
| * fix for /deterministicExtractLoops sed in SymDiffGravatar Shuvendu Lahiri2015-07-19
| |
| * Update URL to boogie-partners to its new location on GitHub.Gravatar Dan Liew2015-06-28
| |
| * Fix issue #16 reported by @crazyktGravatar Dan Liew2015-06-28
| | | | | | | | | | | | | | | | | | | | Previously when Boogie was passed the ``-proc:<NAME>`` argument on the command line it would verify any procedure whose name contained ``<NAME>`` which doesn't seem like correct behaviour. Now Boogie only tries to verify a procedure only if its name matches ``<NAME>`` exactly. I've added several test cases to check Boogie behaves as expected.
| * 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.
| * Remove dead file.Gravatar Dan Liew2015-06-28
| |
| * fixed bug reported by ChrisGravatar qadeer2015-06-15
| |
| * adding z3name optionGravatar Ken McMillan2015-06-15
| |
| * Minor changesGravatar Valentin Wüstholz2015-06-12
| |
| * Fix issue with computation of statement checksums for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
| |
| * Fix issue in checksum computation for lambda expressions.Gravatar Valentin Wüstholz2015-06-12
| |
| * various changes for duality from dead codeplex repoGravatar U-REDMOND\kenmcmil2015-06-09
|/
* Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-08
|
* Fix minor issue.Gravatar Valentin Wüstholz2015-06-05
|
* Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-05
|
* Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
|
* Minor refactoringGravatar Valentin Wüstholz2015-05-17
|
* Make caching of verification results more fine-grained for changes that ↵Gravatar Valentin Wüstholz2015-05-17
| | | | affect preconditions.
* Add support for 'verified_under' attributes on procedure calls and invariants.Gravatar Valentin Wüstholz2015-04-29
|
* VC gen for security propertiesGravatar akashlal2015-04-05
|
* Eliminated calls to deprecated method.Gravatar wuestholz2015-02-18
|
* Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.Gravatar wuestholz2015-02-18
|
* Protect Bitvector field of BvExtractExpr when it is immutable.Gravatar Dan Liew2015-02-12
|
* Protect E0 and E1 in BvConcatExpr if Expr is immutable.Gravatar Dan Liew2015-02-12
|
* 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.
* 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.
* 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.
* Fixed minor issue.Gravatar wuestholz2015-01-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 23:45:29 +0000