summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Look for Boogie.exe also in Program Files (x86)Gravatar MichalMoskal2009-11-03
|
* vc:doomed does not use the console anymore to report resultsGravatar schaef2009-11-02
| | | | | | added first test cases for doomed (including the ones from smoke) minor bug fixes minor speed-ups
* Fixed PreLoopHeap counting bug.Gravatar rustanleino2009-10-31
|
* Initial version of VSI Benchmarks 1 - 8Gravatar RMonahan2009-10-30
|
* Use the new F# names for bigint typeGravatar MichalMoskal2009-10-30
|
* Update F# binaries to Oct09 CTPGravatar MichalMoskal2009-10-30
|
* Fixed problem where Dafny filenames with unusual characters in filenames had ↵Gravatar rustanleino2009-10-29
| | | | | | caused malformed Boogie and malformed VCs. In particular, the problem arose in the CEV $file_name_is declarations. Such characters are now replaced by a percent sign followed by a four-digit hexadecimal number representing the Unicode value of the character. This fixes issue #6057.
* - Sieve.chalice verifies + executes fasterGravatar jansmans2009-10-20
|
* - the "-gen" option works only if the program verifiesGravatar jansmans2009-10-16
|
* Implicitly declare as local variables undeclared variables occurring as ↵Gravatar rustanleino2009-10-16
| | | | LHS's of CALL and RECEIVE statements (as was already done for FORK statements).
* Sieve of Eratosthenes, written in Chalice.Gravatar rustanleino2009-10-15
|
* Changed how Boogie looks for Z3: first look in the directory where Boogie ↵Gravatar rustanleino2009-10-14
| | | | | | is being executed from, then look in "c:\Program Files\Microsoft Research\Z3-2.x\bin" for x := 5,4,3,2,1,0. This fixes Issue Tracker item 5446.
* Evidently, Z3 does not like QID's to start with a digit. If a Boogie ↵Gravatar rustanleino2009-10-14
| | | | | | filename starts with a digit, don't just prepend it to a QID, but prepend another character ('_') first. This fixes issue 5278 in the Issue Tracker.
* Fixed bugs in inlining, and added a test case.Gravatar rustanleino2009-10-14
| | | | This solves issue 5742, as reported in the MSR Boogie Issue Tracker on Codeplex.
* In the TypeDeclCollector, call RegisterType for the bound variables in a ↵Gravatar stobies2009-10-12
| | | | quantifier. This makes sure that we get the proper DEFTYPEs for bit vector variables, even when they are not used in operator expressions. Fixes issue #5741.
* - fixed a positioning bug in Parser.scalaGravatar jansmans2009-10-07
| | | | - CopyLessMessagePassing-with-ack2.chalice verifies (i.e. separate channel for acknowledgements)
* - extended to example to use acknowledgements (but uses sending debit)Gravatar jansmans2009-10-07
|
* - verified a program inpsired by "Copyless Message Passing" in ChaliceGravatar jansmans2009-10-07
| | | | (todo: we should really support sending debit over channel to allow sending with acknowledgements)
* Added /z3lets switch, which governs which kinds of LET expressions are sent ↵Gravatar rustanleino2009-10-04
| | | | to Z3. By default, both LET TERM and LET FORMULA expressions are used. Mode /z3lets:2 uses only LET FORMULA, which works around a current Z3 issue with LET expressions and nested quantifiers.
* - where clauses are now properly type-checkedGravatar jansmans2009-10-02
| | | | - all credits must be consumed on entry to a loop by the invariant (to avoid getting the wrong maxlock)
* Implemented -noDeadlockChecks mode. With this mode, it is possible to give ↵Gravatar rustanleino2009-10-01
| | | | some demos that use locks before explaining the global order on locks.
* Handle new Z3 'Memout' message.Gravatar stobies2009-09-30
|
* Restoring Spec# binariesGravatar stobies2009-09-30
|
* Fixed some bugs in the generation of bitvector input for Z3.Gravatar rustanleino2009-09-29
| | | | Deleted/ignored some binaries in the Binaries directory.
* Use type-erased result type to make decision about whether or not to include ↵Gravatar rustanleino2009-09-27
| | | | antecedent in select-of-store axioms (fixing an error in my previous check-in).
* Optimized the number of Z3 queries in doomed program point detection.Gravatar schaef2009-09-25
|
* Added antecedent to select-of-store axioms to make them sound even when ↵Gravatar rustanleino2009-09-24
| | | | triggers are ignored.
* Added /z3multipleErrors flag for generation of multiple counterexamples per ↵Gravatar mkawa2009-09-23
| | | | assert (switches off z3's /@ flag).
* * Boogie and Dafny: added /cev:<file> optionGravatar rustanleino2009-09-15
| | | | | * SscBoogie: changed default setting for /modifiesOnLoop (we really should move this SscBoogie-specific code to the Spec# codeplex)
* Dafny: Added axioms for division and modulo.Gravatar rustanleino2009-09-15
| | | | | Dafny: Make use of function preconditions in function well-definedness checks. Chalice: Changed old "install" to current "reorder" keyword in Emacs mode.
* Dafny:Gravatar rustanleino2009-09-14
| | | | | | | | * Added DeclType(f)==C axioms, which for each field f says which class declares it. Boogie: * Changed behavior of free loop invariants. Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures. The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior. * NOTE: I did NOT yet make the corresponding change for loop unrolling, but it is needed.
* Report prover warnings during smoke test via the VerifierCallbackGravatar stobies2009-09-07
|
* Use callback mechanism to report prover warnings; do not just write them to ↵Gravatar stobies2009-09-07
| | | | stdout/stderr
* Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other ↵Gravatar stobies2009-09-07
| | | | bitvector operations
* Full (?) support in Dafny for Counterexample Visualizer predicates.Gravatar rustanleino2009-08-19
|
* Please ignore. Just testing my account.Gravatar schaef2009-08-19
|
* Improve token-dumping in the inspector interfaceGravatar MichalMoskal2009-08-18
|
* Also sign AbsInt.dllGravatar stobies2009-08-18
|
* Added files to stamp drop builds with generated version numbersGravatar stobies2009-08-18
|
* - made the output of the Chalice-to-C# translator slightly nicerGravatar jansmans2009-08-17
|
* - Chalice-to-C# compiler now supports channelsGravatar jansmans2009-08-17
|
* Sign assembliesGravatar stobies2009-08-17
|
* Updated Answer files, in synch with my recent edits 31961.Gravatar rustanleino2009-08-16
|
* * Implemented channelsGravatar rustanleino2009-08-16
| | | | | | | | | | | | | | | | - channel declarations - send and receive statements - bounds clause for new, to accommodate channels - Added ProdConsChannel.chalice test case - Resolve and Translate (but no Compile yet) - Added Credits to global state in encoding (this caused changes to lots of source lines) * Simplified meaning of maxlock==E * Various parser improvements * Added alternative syntax for eval statements * Some renamings in error messages (e.g., install -> reorder) * Added preliminary parsing for condition variables and their wait and signal operations * Added new keywords to Chalice emacs mode
* Incorporated Counterexample Visualizer (CEV) information in the generated ↵Gravatar rustanleino2009-08-15
| | | | Boogie.
* Fixed bug where the remove-empty-blocks optimization had not updated the ↵Gravatar rustanleino2009-08-13
| | | | start block. Now it does. After the remove-empty-blocks optimization, the only possibly empty block is the start block. That is, the optimization does not change the name of the start block.
* Changes needed in order to build Boogie using a freshly built Spec# compiler ↵Gravatar mikebarnett2009-08-10
| | | | and not just the LKG.
* The beginnings of a CCI Metadata (http://ccimetadata.codeplex.com) based ↵Gravatar mikebarnett2009-08-09
| | | | bytecode translator.
* Removed Output files. These are created on a local machine when the tests ↵Gravatar rustanleino2009-08-07
| | | | are run.
* Fixed problem where nullary function with definition had caused a crash.Gravatar rustanleino2009-08-07
|
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-04 15:19:56 +0000