summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Boogie: Added boolean code expressions (sans well-formedness checks on the in...Gravatar rustanleino2010-08-10
* Remove -z3DebugTraces and -z3Mam options (no longer working). Rename the -z3b...Gravatar MichalMoskal2010-08-06
* Boogie: added /z3bv option that overrides the current setting of Z3 options f...Gravatar stobies2010-08-06
* Remove support for Z3 V1 and clean up parameter processing code for Z3Gravatar stobies2010-08-06
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
* Boogie: VCGeneration port part 3/3: Updating sources to reference new project...Gravatar tabarbe2010-07-28
* Also traverse bodies of function definitions when performing lambda expansion.Gravatar sboehme2010-07-23
* Boogie: Added interprocedural live variable analysis. Flag to turn it on: "/l...Gravatar akashlal2010-07-19
* /stratifiedInline:n eagerly inlines n times before calling the stratified inl...Gravatar akashlal2010-07-10
* Boogie: Added stratified inlining. It is enabled using the flag /stratifiedIn...Gravatar akashlal2010-07-07
* Boogie: Added an additional parameter 'defines' to the method 'BoogiePL.Parse...Gravatar wuestholz2010-07-06
* Unified the .frame files so that both Boogie and Dafny use exactly the same o...Gravatar mikebarnett2010-06-25
* Updated the frame files to work with the latest Coco/R. This entails *not* ha...Gravatar mikebarnett2010-06-22
* fixed a compiler warning about initialization of a non-null field inside the ...Gravatar qadeer2010-06-10
* changed the behavior of /loopUnroll:n so that the parameter n is applied per ...Gravatar qadeer2010-05-26
* Boogie:Gravatar rustanleino2010-05-15
* BCT: Added prelude. Started test1 as a test of verification.Gravatar rustanleino2010-05-12
* Dafny:Gravatar rustanleino2010-05-06
* Dafny:Gravatar rustanleino2010-05-06
* Added another option for lazy inlining based on macro expansion. This option...Gravatar qadeer2010-05-03
* 1. Fixed lazy inlining implementation so that inlined procedures use live var...Gravatar qadeer2010-04-30
* 1. couple of bug fixes in interprocedural error trace generationGravatar qadeer2010-04-23
* 1. Fixed an off-by-one error in parsing array partitions in Z3 modelsGravatar qadeer2010-04-19
* First cut of lazy inlining. The option can be turned on by the flag /lazyInl...Gravatar qadeer2010-04-17
* Dafny: Added definedness checks for all statements (previously, some were mi...Gravatar rustanleino2010-03-13
* Call program-wide lambda desugaring on axioms only. Call it on procedures in ...Gravatar MichalMoskal2010-03-12
* Boogie: Clone a TypedIdent to get rid of 'where' clauses during the translati...Gravatar rustanleino2010-03-12
* Dafny:Gravatar rustanleino2010-03-10
* Boogie: Added resolution and type checking for attributes on "call" and "call...Gravatar rustanleino2010-03-09
* 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
* added an option /doModSetAnalysis specially for ZvonimirGravatar qadeer2010-02-20
* 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 expressions;...Gravatar MichalMoskal2010-02-19
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
* * Added "deprecated" comment in help message about /interprocInfer switch. T...Gravatar rustanleino2010-02-18
* 1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a linea...Gravatar qadeer2010-02-16
* Implemented block coalescing invoked right after type checking.Gravatar qadeer2010-02-16
* (no commit message)Gravatar qadeer2010-02-12
* 1. Fixed bug in StandardVisitor.sscGravatar qadeer2010-02-09
* 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 info...Gravatar stobies2010-02-08
* Fixed the implementation of inlining to deal with inlining depth properly.Gravatar qadeer2010-01-30
* Added experimental feature /DoomDebug. Can be test using Test/doomed/doomdebu...Gravatar schaef2010-01-28
* Implemented the command line switch /useArrayTheory. This switch should be u...Gravatar qadeer2010-01-21
* Allow ":" in addition to "returns" in function definitions. Make the pretty-p...Gravatar MichalMoskal2009-12-17
* Z3 parameters to help it bail out of fruitless searches fasterGravatar mkawa2009-12-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 07:51:35 +0000