Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Dafny: fixed typo in latex mode | 2012-09-05 | |
| | |||
* | DafnyExtension: don't duplicate names of inherited identifiers | 2012-08-30 | |
| | |||
* | Dafny: for refinements, don't consider a newly provided predicate body to be ↵ | 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 ↵ | 2012-08-30 | |
| | | | | as an identifier definition) | ||
* | Dafny: allow "_" as don't-care variable name | 2012-08-30 | |
| | |||
* | Dafny: fixed bug in checking postconditions of functions that mention the ↵ | 2012-08-29 | |
| | | | | result the function itself | ||
* | DafnyExtension: fixed bug (omitted case: VarDeclStmt has no Update component) | 2012-08-29 | |
| | |||
* | Dafny: fixed contract violation in parser (for non-parsing Lhs production) | 2012-08-29 | |
| | |||
* | A small fix in variable definition analysis. | 2012-08-29 | |
| | |||
* | Added generation of invariants to restrict source location to sensible values. | 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 | 2012-08-27 | |
| | |||
* | Dafny: fixed contract bug in resolver | 2012-08-27 | |
| | |||
* | Fix the whole-program translator so that exception handling is done | 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. | 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. | 2012-08-22 | |
| | |||
* | Boogie build succeeded | 2012-08-22 | |
| | |||
* | Merge | 2012-08-21 | |
|\ | |||
* | | DafnyExtensions: better error handling | 2012-08-21 | |
| | | |||
| * | Extra debugging output for Houdini | 2012-08-21 | |
|/ | |||
* | Dafny and Boogie: get rid of 'static' fields in parser | 2012-08-21 | |
| | |||
* | Fixed problem where SOURCE variables were not being generated. | 2012-08-20 | |
| | |||
* | Added functionality for race error reporting. | 2012-08-20 | |
| | |||
* | DafnyExtension: fixed bad merge | 2012-08-17 | |
| | |||
* | Merge | 2012-08-17 | |
|\ | |||
* | | DafnyExtension: improved concurrency behavior | 2012-08-17 | |
| | | |||
| * | DafnyExtension: report out-of-time and out-of-memory errors | 2012-08-17 | |
|/ | |||
* | DafnyExtension: toward some fixes | 2012-08-17 | |
| | |||
* | DafnyExtension: simplified display of type names and field names | 2012-08-17 | |
| | |||
* | DafnyExtension: various improvements | 2012-08-16 | |
| | |||
* | Fixed bug where source location attributes are not being attached to a CHECK | 2012-08-16 | |
| | | | | call, and refactored code to avoid the duplication which caused this error. | ||
* | DafnyExtension: improvements | 2012-08-15 | |
| | |||
* | DafnyExtension: do verification in a non-UI thread | 2012-08-15 | |
| | |||
* | DafnyExtension: fixed more missing cases for hover texts | 2012-08-15 | |
| | |||
* | Dafny: fixed some bugs in the newly added DafnyExtension code | 2012-08-15 | |
| | |||
* | Merge | 2012-08-15 | |
|\ | |||
* | | Dafny: added Statement.SubExpressions getter | 2012-08-15 | |
| | | | | | | | | DafnyExtension: added hover text for identifiers | ||
* | | Dafny: added Statement.SubExpressions getter | 2012-08-15 | |
| | | | | | | | | DafnyExtension: added hover text for identifiers | ||
* | | Dafny: removed the defunct "havoc" keyword from various source-code highlighters | 2012-08-15 | |
| | | |||
| * | Boogie build succeeded | 2012-08-15 | |
| | | |||
* | | Merge | 2012-08-14 | |
|\| | |||
* | | Dafny emacs mode: changed a menu name (Does anyone ever use this menu anyhow?) | 2012-08-14 | |
| | | |||
* | | Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension ↵ | 2012-08-14 | |
| | | | | | | | | crashing after certain deletes) | ||
| * | Also updated test15 | 2012-08-14 | |
| | | |||
| * | Update test suite for commit 8a59fbb7ee34. | 2012-08-14 | |
| | | |||
| * | Added GPUVerifyBoogieDriver project. | 2012-08-14 | |
| | | | | | | | | Contributed by Egor Kyshtymov. | ||
| * | Separated race checking into logging and checking calls. This simplifies | 2012-08-14 | |
| | | | | | | | | error reporting. | ||
| * | Removed some dud code for handling nested maps, which we no longer support. | 2012-08-13 | |
| | | |||
| * | Some more code cleanup related to removal of the "divided" option. | 2012-08-13 | |
| | | |||
| * | Removed code related to "divided" option. | 2012-08-13 | |
|/ | |||
* | Merge | 2012-08-13 | |
|\ |