summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
* Boogie:Gravatar rustanleino2010-10-12
* Get rid of some CCI dependencies in DriverGravatar MichalMoskal2010-10-07
* Update to VS2010.Gravatar MichalMoskal2010-10-07
* Boogie:Gravatar rustanleino2010-09-23
* Some simplifications to coverage reporting for StratifiedInlining.Gravatar akashlal2010-09-19
* added an optimization to extract loops so that only loop targets are treated ...Gravatar qadeer2010-09-10
* Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal tha...Gravatar akashlal2010-09-05
* Delete unreachable Blocks of an Impl before calling ExtractLoops().Gravatar akashlal2010-09-05
* Fix for extractLoopsGravatar akashlal2010-09-04
* more fixes to ExtractLoopsGravatar qadeer2010-09-03
* Added a fix to extract loops code so that it returns a more comprehensive map...Gravatar qadeer2010-09-03
* Changed the interface of Parse so that it can consume a program from a StreamGravatar akashlal2010-09-03
* fixed bug in extract loops by ensuring that loop extraction is done in nestin...Gravatar qadeer2010-09-01
* Added a way of recovering counterexample paths after loop extraction. Stable,...Gravatar akashlal2010-09-01
* Added a new class LoopProcedure to represent the procedures representing extr...Gravatar qadeer2010-09-01
* Dafny: added a command-line option to change the prelude fileGravatar sboehme2010-08-30
* created a new build target called z3apidebug.Gravatar qadeer2010-08-29
* Boogie: Commented out all occurences of repeated inherited contracts - makes ...Gravatar tabarbe2010-08-27
* Boogie: Removed some errors with code contracts (commenting out doubly-inheri...Gravatar tabarbe2010-08-27
* Boogie: Changed the cce classes into one separate project, which every other ...Gravatar tabarbe2010-08-27
* Boogie: Basetypes port 3/3: Committing changed referencesGravatar tabarbe2010-08-27
* Boogie: Graph port 3/3: Committing changed references; also, adding back cce ...Gravatar tabarbe2010-08-27
* Boogie: AIFramework port part 3/3: Committing reference changes, edit to Core...Gravatar tabarbe2010-08-26
* 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