summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Collapse)AuthorAge
* Updated the frame files to work with the latest Coco/R. This entails *not* ↵Gravatar mikebarnett2010-06-22
| | | | | | having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories. Lots of code changes to compensate for the new frame files.
* fixed a compiler warning about initialization of a non-null field inside the ↵Gravatar qadeer2010-06-10
| | | | LoopUnroll constructor
* changed the behavior of /loopUnroll:n so that the parameter n is applied per ↵Gravatar qadeer2010-05-26
| | | | SCC.
* Boogie:Gravatar rustanleino2010-05-15
| | | | | | | | | | * Added support for polymorphism in lambda expressions * Little clean-up here and there * Added 'then' keyword to emacs and latex modes Dafny: * Added support for fine-grained framing, using the back-tick syntax from Region Logic * Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses
* BCT: Added prelude. Started test1 as a test of verification.Gravatar rustanleino2010-05-12
|
* Dafny:Gravatar rustanleino2010-05-06
| | | | | * Recoded frame axioms to be more goal directed * Added Main test driver to Test/VSI-Benchmarks/b2.dfy
* Dafny:Gravatar rustanleino2010-05-06
| | | | | | | | * First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies) * Added "print" statement (to make running compiled programs more interesting) * Changed name of default class from $default to _default Boogie: * Included "lambda" as a keyword in emacs and latex style files
* Added another option for lazy inlining based on macro expansion. This ↵Gravatar qadeer2010-05-03
| | | | option is activated by /lazyInline:2. The original method is activated by /lazyInline:1.
* 1. Fixed lazy inlining implementation so that inlined procedures use live ↵Gravatar qadeer2010-04-30
| | | | | | variable analysis as well 2. Separeted model printing from the lazy inlining option
* 1. couple of bug fixes in interprocedural error trace generationGravatar qadeer2010-04-23
| | | | 2. added facility for giving weights to the generated quantifiers for lazy inlining; however, left the weights at default 1.
* 1. Fixed an off-by-one error in parsing array partitions in Z3 modelsGravatar qadeer2010-04-19
| | | | | 2. Added code for printing array partitions 3. Set UseAbstractInterpretation=false in case lazy inlining is being used
* First cut of lazy inlining. The option can be turned on by the flag ↵Gravatar qadeer2010-04-17
| | | | /lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.
* Dafny: Added definedness checks for all statements (previously, some were ↵Gravatar rustanleino2010-03-13
| | | | | | missing) Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
* Call program-wide lambda desugaring on axioms only. Call it on procedures in ↵Gravatar MichalMoskal2010-03-12
| | | | passive form.
* Boogie: Clone a TypedIdent to get rid of 'where' clauses during the ↵Gravatar rustanleino2010-03-12
| | | | translation of free variables of lambda expressions.
* Dafny:Gravatar rustanleino2010-03-10
| | | | | * Added "decreases" clauses to methods. * Interpret the filename stdin.dfy as an indication to read the program from standard input.
* Boogie: Added resolution and type checking for attributes on "call" and ↵Gravatar rustanleino2010-03-09
| | | | "call forall". Fixed printing of these attributes to print all attributes.
* added support for printing attributes on calls via EmitGravatar qadeer2010-03-08
|
* added attributes to CallForallCmd as wellGravatar qadeer2010-03-07
|
* added the ability to annotate calls with attributesGravatar qadeer2010-03-06
|
* Boogie:Gravatar rustanleino2010-02-20
| | | | | | | | | | | * Bug fix: Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case) * Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants. Previously, the only option was to instrument at the beginning and end of every basic block. The new option, which is now the default, is to instrument only at the beginning of loop heads. * Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized * Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1 Boogie refactoring: * Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand * Cleaned up some parsing of command-line options
* added an option /doModSetAnalysis specially for ZvonimirGravatar qadeer2010-02-20
| | | | changed liveVarsBefore from Boogie.Set to Generics.Set
* Fix up the polymorphic case for lambda; it probably still isn't quite correct.Gravatar MichalMoskal2010-02-19
|
* Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda ↵Gravatar MichalMoskal2010-02-19
| | | | expressions; they might not yet fully work for polymorphic maps.
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
|
* * Added "deprecated" comment in help message about /interprocInfer switch. ↵Gravatar rustanleino2010-02-18
| | | | | | | The functionality is currently broken. * Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
* 1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a ↵Gravatar qadeer2010-02-16
| | | | | | | linear procedure call 2. Inlining requires two fields OriginalBlocks and OriginalLocVars in Implementation. These are set just before inlining is called and now I reset them to null afterwards to help garbage collection. 3. Clear live variables right after passification again to help garbage collection.
* Implemented block coalescing invoked right after type checking.Gravatar qadeer2010-02-16
| | | | Controlled by the option /coalesceBlocks (default is to perform the optimization).
* (no commit message)Gravatar qadeer2010-02-12
|
* 1. Fixed bug in StandardVisitor.sscGravatar qadeer2010-02-09
| | | | | | 2. Hoisted the call to inlining into BoogieDriver.ssc 3. Implemented a simple dead variable elimination 4. Perform inlining only for those procedures whose verification is not skipped
* Boogie: /useArrayTheory currently implies /monomorphizeGravatar rustanleino2010-02-09
|
* Fix a bug in checking for {:inline} procedure attribute. Resolves #6993.Gravatar MichalMoskal2010-02-08
|
* Use reflection to read version string from assembly when displaying logo ↵Gravatar stobies2010-02-08
| | | | information
* Fixed the implementation of inlining to deal with inlining depth properly.Gravatar qadeer2010-01-30
|
* Added experimental feature /DoomDebug. Can be test using ↵Gravatar schaef2010-01-28
| | | | Test/doomed/doomdebug.bpl
* Implemented the command line switch /useArrayTheory. This switch should be ↵Gravatar qadeer2010-01-21
| | | | used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.
* Allow ":" in addition to "returns" in function definitions. Make the ↵Gravatar MichalMoskal2009-12-17
| | | | | | | | pretty-printer use ":" not "returns". Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions. Consequently foo(int,y:bool) is no longer allowed. Update the testsuite to match that.
* Z3 parameters to help it bail out of fruitless searches fasterGravatar mkawa2009-12-05
| | | | | print _all_ the attributes of an assert this time add simpletypes to the visitor
* print attributes in AssertCmd.EmitGravatar mkawa2009-12-02
|
* Added resolution and translation of algebraic datatypes and (in function ↵Gravatar rustanleino2009-11-20
| | | | | | bodies) match expressions. Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
* Fixed bug in inlining (procedure *definitions* had been traversed by ↵Gravatar rustanleino2009-11-19
| | | | | | StandardVisitor while visiting commands). This solves Issue #6266.
* Redesigned the encoding of Dafny generics, including the built-in types set ↵Gravatar rustanleino2009-11-06
| | | | | | | | | | | | and seq. Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43). Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed. Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy. Added a space in the pretty printing of Boogie coercion expressions.
* 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.
* 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.
* 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: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.
* Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other ↵Gravatar stobies2009-09-07
| | | | bitvector operations
* Sign assembliesGravatar stobies2009-08-17
|
* Changes needed in order to build Boogie using a freshly built Spec# compiler ↵Gravatar mikebarnett2009-08-10
| | | | and not just the LKG.
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-25 21:00:39 +0000