Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Dafny: did a little to extend the support of labeled statements in ↵ | Unknown | 2012-09-10 |
| | | | | refinements (things like multiple labels are still not thought through very well) | ||
* | Dafny: improved checking of inherited postconditions (in refinements) | Unknown | 2012-09-10 |
| | |||
* | Boogie: added /tracePOs option for printing out number of proof obligations ↵ | Unknown | 2012-09-10 |
| | | | | without also printing out the verification times | ||
* | Merge | Rustan Leino | 2012-09-10 |
|\ | |||
* | | ignore Chalice/bin | Rustan Leino | 2012-09-10 |
| | | |||
* | | Merge | Rustan Leino | 2012-09-10 |
|\ \ | |||
| * | | Find implementations of interface methods for dynamic dispatch, not just | Unknown | 2012-09-09 |
| | | | | | | | | | | | | overrides of virtual methods. | ||
* | | | DafnyExtension: addressed a class initialization order problem | Rustan Leino | 2012-09-09 |
| | | | |||
* | | | Dafny: allow 'decreases *' (that is, non-terminating recursion) on ↵ | Rustan Leino | 2012-09-09 |
| | | | | | | | | | | | | tail-recursive methods | ||
| * | | Avoid creating a dynamic dispatch table for GetHashCode and ToString: it ends | Unknown | 2012-09-09 |
| | | | | | | | | | | | | | | | up creating code that the Boogie parser gets a stack overflow while trying to parse! | ||
| * | | Moved the statement traverser's operand stack (used for explicit push/pop/dup | Unknown | 2012-09-09 |
|/ / | | | | | | | | | | | | | | | | | | | in the code model) into the sink so that the different statement traversers used for things like if-then-else statements share the same stack. Fixed a problem in the dispatch table for whole program virtual dispatch so it works for generic methods. Found input that either crashed the translator or caused it to produce bad Boogie: "fixed" it by having the translator thrown an exception so the method containing the bad code is skipped. | ||
* | | Merge | Unknown | 2012-09-07 |
|\ \ | |||
* | | | Dafny: Added detection and support for tail recursive calls (and an ↵ | Unknown | 2012-09-07 |
| | | | | | | | | | | | | optional "tailrecursion" attribute). Also, let the cloner also clone attributes. | ||
* | | | DafnyExtension: new color (violet) for buffer snapshot sent to the verifier | Unknown | 2012-09-07 |
| | | | |||
| * | | Implement support for alternative SMT solvers -- CVC3 and CVC4 | Peter Collingbourne | 2012-09-06 |
| | | | |||
| * | | Dafny: Fixed a test that would fail with Z3 4.1. | wuestholz | 2012-09-07 |
| | | | |||
* | | | Merge | Unknown | 2012-09-05 |
|\| | | |||
* | | | Dafny: fixed typo in latex mode | Unknown | 2012-09-05 |
| | | | |||
| * | | Moved point at which preprocessed output is shown. | Unknown | 2012-08-31 |
| | | | |||
| * | | Shared state is now properly abstracted in requires clauses. | Unknown | 2012-08-31 |
| | | | |||
* | | | DafnyExtension: don't duplicate names of inherited identifiers | Unknown | 2012-08-30 |
| | | | |||
* | | | Dafny: for refinements, don't consider a newly provided predicate body to be ↵ | Unknown | 2012-08-30 |
| | | | | | | | | | | | | an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be | ||
* | | | DafnyExtension: changed how "_" is displayed (now display as a keyword, not ↵ | Unknown | 2012-08-30 |
| | | | | | | | | | | | | as an identifier definition) | ||
* | | | Dafny: allow "_" as don't-care variable name | Unknown | 2012-08-30 |
| | | | |||
| | * | Dafny: allow more corecursive calls for copredicates | Rustan Leino | 2012-08-30 |
| |/ |/| | |||
| * | Merge | Unknown | 2012-08-30 |
| |\ | |/ |/| | |||
| * | Barriers now handled uniformly via bugle_barrier. | Unknown | 2012-08-30 |
| | | | | | | | | | | | | | | | | | | | | | | Improved loop invariant inference so that procedure formal parameters are treated as constants. (This involved fixing a bug where a Formal was being dualised to a LocalVariable.) Fixed problem in GPUVerifyBoogieDriver where source location information was being looked for via a file name, rather than a full path. Cleaned up some code in GPUVerifyBoogieDriver. | ||
* | | Dafny: fixed bug in checking postconditions of functions that mention the ↵ | Unknown | 2012-08-29 |
| | | | | | | | | result the function itself | ||
* | | DafnyExtension: fixed bug (omitted case: VarDeclStmt has no Update component) | Unknown | 2012-08-29 |
| | | |||
* | | Dafny: fixed contract violation in parser (for non-parsing Lhs production) | Unknown | 2012-08-29 |
|/ | |||
* | A small fix in variable definition analysis. | Unknown | 2012-08-29 |
| | |||
* | Added generation of invariants to restrict source location to sensible values. | Egor Kyshtymov | 2012-08-28 |
| | | | | | Refactored Make...Variable() and FindOrCreate...Variable() functions to take a variable name as a parameter rather than the variable itself. | ||
* | DafnyExtension: don't reverify a buffer with no changes | Rustan Leino | 2012-08-27 |
| | |||
* | Dafny: fixed contract bug in resolver | Rustan Leino | 2012-08-27 |
| | |||
* | Fix the whole-program translator so that exception handling is done | Unknown | 2012-08-23 |
| | | | | | | | | | | correctly for virtual method calls. Changed the whole-program override for VisitMethodCall so that it creates a new CodeModel expression that does not contain virtual method calls and then translate that newly built expression. Treat type equality (and inequality) specially: translate it directly to a type test instead. But do it just for the idiom: "o.GetType == typeof(T)". In that case, turn it into "is#T$T($DynamicType(o))". | ||
* | Make the modelExceptions option an integer. | Unknown | 2012-08-22 |
| | | | | | | | | | | | | | | | 0 means no modeling at all. 1 (which can be specified only if also specifying whole program translation) means that a fixpoint analysis will be done on all of the translated assemblies to compute the set of exceptions that each method can throw (even though we're using only the fact that a method throws anything at all, not the specific exceptions it can throw) so only calls to methods that can throw an exception have a branch after the call that checks to see if an exception has been thrown. Methods that are defined outside of the set of translated assemblies are assumed to *not* throw any exceptions! 2 means that every method is considered to be one that can throw an exception. | ||
* | Added group information to race error reporting. | Egor Kyshtymov | 2012-08-22 |
| | |||
* | Boogie build succeeded | CodeplexBot | 2012-08-22 |
| | |||
* | Merge | Rustan Leino | 2012-08-21 |
|\ | |||
* | | DafnyExtensions: better error handling | Rustan Leino | 2012-08-21 |
| | | |||
| * | Extra debugging output for Houdini | Unknown | 2012-08-21 |
|/ | |||
* | Dafny and Boogie: get rid of 'static' fields in parser | Rustan Leino | 2012-08-21 |
| | |||
* | Fixed problem where SOURCE variables were not being generated. | Unknown | 2012-08-20 |
| | |||
* | Added functionality for race error reporting. | Egor Kyshtymov | 2012-08-20 |
| | |||
* | DafnyExtension: fixed bad merge | Rustan Leino | 2012-08-17 |
| | |||
* | Merge | Rustan Leino | 2012-08-17 |
|\ | |||
* | | DafnyExtension: improved concurrency behavior | Unknown | 2012-08-17 |
| | | |||
| * | DafnyExtension: report out-of-time and out-of-memory errors | Rustan Leino | 2012-08-17 |
|/ | |||
* | DafnyExtension: toward some fixes | Unknown | 2012-08-17 |
| | |||
* | DafnyExtension: simplified display of type names and field names | Unknown | 2012-08-17 |
| |