Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | fixed bug | 2013-09-09 | |
| | |||
* | fixed the problem with codexprs | 2013-09-07 | |
| | | | | now positive/negative context is detected and appropriate translation is done | ||
* | When a codeexpr is used at the top-level in an assume statement, we use the ↵ | 2013-09-04 | |
| | | | | alternative existential semantics. | ||
* | Avoid another potential data race. | 2013-07-23 | |
| | |||
* | Resolved some issues with data races. | 2013-07-23 | |
| | |||
* | Did some refactoring. | 2013-07-23 | |
| | |||
* | Minor fix | 2013-07-23 | |
| | |||
* | Did some refactoring. | 2013-07-23 | |
| | |||
* | Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in ↵ | 2013-07-22 | |
| | | | | code (as opposed to contracts). | ||
* | All ...Seq classes now gone | 2013-07-22 | |
| | |||
* | ExprSeq: farewell | 2013-07-22 | |
| | |||
* | RESeq: farewell | 2013-07-22 | |
| | |||
* | BlockSeq: farewell | 2013-07-22 | |
| | |||
* | CmdSeq: farewell | 2013-07-22 | |
| | |||
* | Started to remove ...Seq classes | 2013-07-22 | |
| | |||
* | More refactoring | 2013-07-22 | |
| | |||
* | More refactoring | 2013-07-22 | |
| | |||
* | More refactoring towards replacing PureCollections.Sequence with List | 2013-07-22 | |
| | |||
* | Merge | 2013-07-22 | |
|\ | |||
* | | Refactoring of TypeVariableSeq | 2013-07-22 | |
| | | |||
* | | Changed Has method of PureSequence to Contains to make refactoring easier. | 2013-07-22 | |
| | | |||
| * | merge | 2013-07-22 | |
| |\ | |/ |/| | |||
* | | Refactoring of VariableSeq and TypeSeq | 2013-07-22 | |
| | | |||
* | | Requires/EnsuresSeq replaced by List<Requires/Ensures> | 2013-07-22 | |
| | | |||
| * | Merge | 2013-07-15 | |
|/| | |||
* | | Worked on the parallelization. | 2013-07-11 | |
| | | |||
* | | Worked on the parallelization. | 2013-07-10 | |
| | | |||
* | | Worked on the parallelization. | 2013-07-08 | |
| | | |||
| * | merge | 2013-07-06 | |
| |\ | |/ |/| | |||
* | | Fixes for duality under corral | 2013-06-14 | |
| | | |||
| * | CVC4 Parser | 2013-06-12 | |
|/ | |||
* | removed call forall and * args to calls | 2013-02-23 | |
| | |||
* | Removed old comments about "BASEMOVE" and other constructor calls, where the ↵ | 2013-01-07 | |
| | | | | conversion from Spec# into C# moved a constructor call | ||
* | Boogie: added type 'real' with overloaded arithmetic operations plus real ↵ | 2012-09-27 | |
| | | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested) | ||
* | Removed AIFramework from Boogie -- use native trivial or native ↵ | 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. | ||
* | Boogie: Get rid of {:inline} attributes on axioms | 2011-10-27 | |
| | |||
* | Boogie: Get rid of {:ignore} feature on axioms | 2011-10-27 | |
| | |||
* | Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵ | 2011-10-27 | |
| | | | | as if the old /bv:z were used | ||
* | Name the constant used in @MV_state function applications - otherwise we get ↵ | 2011-09-26 | |
| | | | | invalid Z3 files | ||
* | Boogie: use (WEIGHT 0) with the select-of-store axioms | 2011-06-29 | |
| | |||
* | Dafny: compile quantifiers | 2011-03-26 | |
| | | | | | | Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges | ||
* | Re-enabled quantifier checking in the Checked configuration. | 2011-03-16 | |
| | |||
* | new algorithm for dead code detection (vc:doomed) | 2011-03-15 | |
| | |||
* | Turn off quantifier checking in the runtime checking. | 2011-03-14 | |
| | |||
* | Replaced all dictionaries that mapped to bool (i.e., were being used to ↵ | 2011-03-10 | |
| | | | | implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null. | ||
* | Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵ | 2011-03-10 | |
| | | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked. | ||
* | Added a new solution configuration, Checked, that builds the Checked ↵ | 2011-03-07 | |
| | | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration. | ||
* | Fix some more contracts. | 2011-03-07 | |
| | |||
* | Fix contracts so runtime checking can be turned on. | 2011-03-07 | |
| | |||
* | Add VCExprNAry.UniformArguments property to return arguments of nested ↵ | 2011-02-15 | |
| | | | | And/Or nodes. |