summaryrefslogtreecommitdiff
path: root/DafnyDriver
Commit message (Collapse)AuthorAge
* Put all sources under \Source directoryGravatar Rustan Leino2012-10-04
|
* bunch of refactoringsGravatar Unknown2012-10-03
| | | | | | | | | - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
* Dafny: Removed assembly reference to 'AIFramework'.Gravatar wuestholz2012-09-28
|
* Removed AIFramework from Boogie -- use native trivial or native ↵Gravatar boehmes2012-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: added /tracePOs option for printing out number of proof obligations ↵Gravatar Unknown2012-09-10
| | | | without also printing out the verification times
* Dafny: support opening modules into the local scopeGravatar Jason Koenig2012-07-30
|
* Dafny: added structural refinement checkGravatar Jason Koenig2012-07-29
|
* further refactoring of SI;Gravatar qadeer2012-05-29
| | | | removed the program argument to call to VerifyImplementation in Dafny
* removed lazy inliningGravatar qadeer2012-04-28
|
* Dafny: fixed build errorGravatar Rustan Leino2012-03-09
|
* Dafny: changed translation to be sensitive to refinement inheritance; this ↵Gravatar Rustan Leino2012-01-09
| | | | feature is now functional, provided the refining module does not add or change anything
* Boogie: output number of proof obligations (asserts) along with timing ↵Gravatar Rustan Leino2012-01-09
| | | | information when using the /trace option
* Dafny: make /infer:j (the new interval domain) the default abstract interpreterGravatar Rustan Leino2012-01-05
|
* Dafny: compile to .exe only if there is a Main method; otherwise, compile to ↵Gravatar Rustan Leino2011-12-19
| | | | a .dll
* Dafny: Made sure that error locations refer to the Dafny program, even if ↵Gravatar wuestholz2011-12-15
| | | | the /print option is used.
* MergeGravatar Rustan Leino2011-12-07
|\
| * Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable ↵Gravatar wuestholz2011-12-07
| | | | | | | | wellformedness checks).
* | Boogie: Added new abstract interpretation harness, which uses native Boogie ↵Gravatar Rustan Leino2011-12-05
|/ | | | | | | | Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred}
* Dafny: call C# compiler directly from inside Dafny, and optionally produce a ↵Gravatar Rustan Leino2011-11-22
| | | | .cs file with the new /spillTargetCode switch
* Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵Gravatar Rustan Leino2011-11-15
| | | | CommandLineOptions to separate the options that belong to these 3 tools.
* MergeGravatar Rustan Leino2011-09-28
|\
| * Dafny: Added a 'Checked' configuration and fixed some runtime assertion ↵Gravatar wuestholz2011-09-23
| | | | | | | | violations.
* | Dafny: generate a compiler error upon encountering an assume statementGravatar Rustan Leino2011-09-11
|/ | | | Dafny: don't compile programs unless all methods have been verified (or a forced compile is requested)
* Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵Gravatar wuestholz2011-07-15
| | | | some trailing whitespace.
* - fixed a bug in DafnyModelUtils.fs (reading set values from models)Gravatar Unknown2011-07-11
| | | | | - changed Dafny so that it returns an exit code - changed CheckDafnyProgram so that it checks Dafny exit code as well
* Added option to force Dafny compilation, even if verification fails.Gravatar Jason Koenig2011-06-30
|
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵Gravatar mikebarnett2011-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.
* Dafny: Non-empty Visual-Studio error messages for related split-expr locations.Gravatar rustanleino2011-02-27
| | | | Dafny: Forbid jumps from ghost code.
* Dafny: Improved scheme for splitting expressions. Also, report each split ↵Gravatar rustanleino2011-02-19
| | | | in error messages.
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
|
* Dafny: white-space deltas in source codeGravatar rustanleino2011-02-02
|
* Dafny: Fixed some build issues with duplicated and malformed Code Contracts.Gravatar rustanleino2011-01-13
|
* Add functions generated in lambda-expansion of function body to top-level ↵Gravatar MichalMoskal2010-12-17
| | | | program declarations.
* Factored out the ParserHelper class into a separate project and updated the ↵Gravatar wuestholz2010-12-02
| | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
* Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.slnGravatar qadeer2010-12-01
|
* forgot to check this file inGravatar qadeer2010-11-28
|
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* Dafny: a partial first crack at a Dafny model-viewer provider, including ↵Gravatar rustanleino2010-11-01
| | | | captureState mark-ups in the Boogie code generated from Dafny
* Update to VS2010.Gravatar MichalMoskal2010-10-07
|
* Dafny:Gravatar rustanleino2010-09-14
| | | | | | | | * Added internal support for multi-dimensional arrays (but not all surface syntax is there yet) * Removed unused variables from Dafny.atg Boogie and Dafny: * Improved error message for postcondition violations
* Dafny: Made line endings consistentGravatar tabarbe2010-08-04
|
* Dafny: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Fixed some infelicities in the project files.Gravatar mikebarnett2010-08-04
|
* fixed path to the binaries directory; there was an extra .."Gravatar qadeer2010-08-03
|
* Also build Boogie and Dafny projects in 32-bit configurations.Gravatar rustanleino2010-07-30
| | | | Don't insist on DafnyDriver picking up the LKG version (1.0.21125.0) of the Spec# runtime (in fact, most builders will probably have 1.0.21126.0).
* Sign both of the Dafny projects and have Dafny.exe get a version number as well.Gravatar mikebarnett2010-07-30
|
* Dafny: DafnyDriver port part 3/3: Updating sources to reference new project.Gravatar tabarbe2010-07-28
|
* Dafny: DafnyDriver port part 2/3: Adding new dependent file, removing ↵Gravatar tabarbe2010-07-28
| | | | unnecessary one.
* Dafny: DafnyDriver port part 1/3: Replacing old source files with ported versionGravatar tabarbe2010-07-28
|
* Dafny/DafnyDriver: Renaming source files in preparation for port commitGravatar tabarbe2010-07-28
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 18:54:35 +0000