| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Merging complete. Everything looks good *crosses fingers* |  Checkmate50 | 2016-06-06 |
| | | |||
| * | Fix performance issue in ComputeHashCode() methods of Expr classes. |  Dan Liew | 2015-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. | ||
| * | Protect the body of ForAllExpr, ExistsExpr and LambdaExpr when they | Dan Liew | 2015-01-29 |
| | | | | | are immutable. Add unit tests to check this. | ||
| * | Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possible | Dan Liew | 2015-01-29 |
| | | | | | to set them as immutable (not currently enforced for these Expr types). | ||
| * | Add the ability to declare Expr to be immutable at construction time. | Dan Liew | 2015-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. |  wuestholz | 2015-01-26 |
| | | |||
| * | Minor change | wuestholz | 2015-01-26 |
| | | |||
| * | Merging changes from wuestholz/BoogieInvariantFixesIIII | wuestholz | 2015-01-13 |
| |\ | |||
| | * | Made invariant of class 'Trigger' robust by: | wuestholz | 2015-01-09 |
| | | | | | | | | | | | | | | | | | - making field private - adding getter/setter - copying incoming list - exposing read-only list (with help from David Rohr) | ||
| | * | 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) | ||
| * | | Tiny change ('Trigger' class) | 0biha | 2015-01-08 |
| | | | |||
| * | | Tiny fix (made field 'tr' of class 'Trigger' private) | 0biha | 2015-01-08 |
| | | | |||
| * | | Made invariant of class 'Trigger' robust by | 0biha | 2015-01-01 |
| |/ | | | | | | -replacing public field by private field + getter -using read-only wrappers (to avoid leaking) -cloning the tr list in the setter and constructor (to avoid capturing) | ||
| * | Minor refactoring | wuestholz | 2014-11-05 |
| | | |||
| * | Merge |  Dan Rosén | 2014-08-01 |
| |\ | |||
| * | | Add alpha equivalence check for Expr, and use it when lambda lifting | Dan Rosén | 2014-08-01 |
| | | | |||
| | * | Fix bug in BinderExpr where is was possible for A.Equals(B) to return | Dan Liew | 2014-07-29 |
| | | | | | | | | | true but A.GetHashCode() == B.GetHashCode() return false. | ||
| | * | Fix bug in BinderExpr where Equals() was not corrected implemented. | Dan Liew | 2014-07-28 |
| |/ | | | | | | | | | | | | | | | | | BinderExpr was doing: object.Equals(this.TypeParameters, other.TypeParameters) && object.Equals(this.Dummies, other.Dummies) Both of these are wrong because these are of type List<> and so - object.Equals(this.TypeParamters, other.TypeParameters) will call this.TypeParameters.Equals(other.TypeParamters) (assuming they aren't references to the same list) - object.Equals(this.Dummies, other.TypeParameters) will call this.TypeParameters.Equals(other.Dummies) (assuming they aren't references to the same list) so this is becomes a reference comparision on Lists<>. This is wrong because Equals() has been overloaded to implement structural equality. This affects the classes ForallExpr, LambdaExpr and ExistsExpr. | ||
| * | Add some pretty-printing, on by default. Turn off with the flag "/pretty:0" | Dan Rosén | 2014-06-24 |
| | | | | | | | When running boogie form the command line, this should be on by default. On the other hand, the TokenTextWriter constructors and PrintBplFile now have an argument for this, but by default it is off. | ||
| * | checkpoint | qadeer | 2014-05-03 |
| | | |||
| * | disabled quantifier merging, except when no triggers are provided (as ↵ |  Unknown | 2014-03-03 |
| | | | | | discussed with Rustan) | ||
| * | Changed all lambda-expression rewriting to be done as a pre-processing step ↵ | Rustan Leino | 2014-02-28 |
| | | | | | | | before real verification. Fixed treatment of lambda-expression attributes. | ||
| * | (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions ↵ | Rustan Leino | 2014-02-24 |
| | | | | | | | of its methods now demand the return value to equal the given node. Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor. | ||
| * | Fixed errors in the use of Code Contracts | Rustan Leino | 2014-02-10 |
| | | |||
| * | more bug fixes | qadeer | 2013-12-24 |
| | | | | | updates to DeviceCache.bpl to make it verify | ||
| * | Fixed another :never_pattern bug related to nested quantifiers | Rustan Leino | 2013-12-16 |
| | | |||
| * | Fixed bug in never_pattern functionality. In the new design, never_pattern ↵ | Rustan Leino | 2013-12-16 |
| | | | | | does not assemble any nopats from nested quantifiers/lambdas. | ||
| * | All ...Seq classes now gone | Ally Donaldson | 2013-07-22 |
| | | |||
| * | ExprSeq: farewell | Ally Donaldson | 2013-07-22 |
| | | |||
| * | Started to remove ...Seq classes | Ally Donaldson | 2013-07-22 |
| | | |||
| * | More refactoring | Ally Donaldson | 2013-07-22 |
| | | |||
| * | More refactoring towards replacing PureCollections.Sequence with List | Ally Donaldson | 2013-07-22 |
| | | |||
| * | Refactoring of TypeVariableSeq | Ally Donaldson | 2013-07-22 |
| | | |||
| * | Changed Has method of PureSequence to Contains to make refactoring easier. | Ally Donaldson | 2013-07-22 |
| | | |||
| * | Allow attributes on procedure formals, function formals, and bound variables |  Unknown | 2013-01-07 |
| | | |||
| * | Removed old comments about "BASEMOVE" and other constructor calls, where the ↵ | Unknown | 2013-01-07 |
| | | | | | conversion from Spec# into C# moved a constructor call | ||
| * | Removed AIFramework from Boogie -- use native trivial or native ↵ | boehmes | 2012-09-27 |
| | | | | | | | | interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped. | ||
| * | Make set iteration order deterministic |  Michal Moskal | 2011-12-07 |
| | | | | | Make the set class generic | ||
| * | changed the semantics of requires and ensures for inlined procedures |  qadeer | 2011-11-17 |
| | | |||
| * | Fix a bug in cloning of nested lambda expressions in AI engine | MichalMoskal | 2011-02-11 |
| | | |||
| * | Boogie: Commented out all occurences of repeated inherited contracts - makes ↵ | tabarbe | 2010-08-27 |
| | | | | | fewer error messages when compiling with runtime checking on. | ||
| * | Boogie: Committing changed source files | tabarbe | 2010-08-20 |
| | | |||
| * | Boogie: Renaming core sources in preparation for port commit | tabarbe | 2010-08-20 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |