summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Added a short description of new flags added to Boogie.Gravatar akashlal2010-08-23
* Fixed external references to other projects in the solution.Gravatar mikebarnett2010-08-23
* Boogie: Adding required source file, deleting no-longer-necessarry oneGravatar tabarbe2010-08-20
* Boogie: Committing changed source filesGravatar tabarbe2010-08-20
* Boogie: Renaming core sources in preparation for port commitGravatar tabarbe2010-08-20
* Boogie: Renaming core sources in preparation for port commitGravatar tabarbe2010-08-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 15:20:27 +0000