summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Added user option for bounding inlining depthGravatar akashlal2010-08-20
* Don't set monomorphize with typeEncoding:m, not neccessary.Gravatar MichalMoskal2010-08-18
* Added option for displaying stratified inlining's searchGravatar akashlal2010-08-18
* Change Synonym type printing to what it was, use a workaround in TypeToString...Gravatar MichalMoskal2010-08-18
* Make /typeEncoding:m work with arraysGravatar MichalMoskal2010-08-18
* Boogie: Removed mistaken duplication of a type parameterGravatar tabarbe2010-08-16
* Added more options for stratified inliningGravatar akashlal2010-08-16
* Added methods to read a file from any Stream objectGravatar akashlal2010-08-12
* Added the option /extractLoops to extract loops as procedure calls. If eithe...Gravatar qadeer2010-08-11
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-17 15:10:19 +0000