summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Boogie: handle absolute paths on *nix correctlyGravatar Peter Collingbourne2012-05-02
* Get Boogie and GPUVerify to compile and run with MonoGravatar Peter Collingbourne2012-05-02
* added counterexample generation based on labels back to stratified inliningGravatar qadeer2012-05-01
* UseLabels=false when stratified inline is onGravatar qadeer2012-04-29
* removed proccopybounding codeGravatar qadeer2012-04-28
* removed lazy inliningGravatar qadeer2012-04-28
* unsat core for houdiniGravatar qadeer2012-04-27
* Added functionality to "skip" procedures. Some cleanup.Gravatar akashlal2012-04-12
* Fixed bug with triply nested maps and polymorphism (reported as Item # 10218).Gravatar Unknown2012-04-04
* added nonUniformUnfolding optionGravatar qadeer2012-04-03
* deleted the option UseUnsatCoreForInliningGravatar qadeer2012-04-02
* Emit of invariants now prints out the invariant attributes alsoGravatar qadeer2012-03-26
* added attributes to loop invariantsGravatar qadeer2012-03-23
* more type checking for datatypesGravatar qadeer2012-03-18
* Boogie: Simplified (and liberalized) parsing of string literals as attribute ...Gravatar Unknown2012-03-12
* updated Boogie strings so that they can refer to \" (and more)Gravatar qadeer2012-03-12
* make the call to ProcessDataTypeConstructors in the right placeGravatar qadeer2012-03-11
* Boogie: map the given filename stdin.bpl to standard inputGravatar Unknown2012-03-09
* various refactorings related to houdiniGravatar qadeer2012-03-02
* verbose mode for stratified inlining.Gravatar Unknown2012-02-29
* bug fixes related to using ControlFlowFunction instead of labelsGravatar qadeer2012-02-23
* using model instead of labelsGravatar Unknown2012-02-23
* verbose modeGravatar akashlal2012-02-19
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
* Boogie: output number of proof obligations (asserts) along with timing inform...Gravatar Rustan Leino2012-01-09
* made delegate a datatypeGravatar qadeer2011-12-30
* fixed problems with datatypesGravatar qadeer2011-12-29
* fixed a completeness problem in houdini with inliningGravatar qadeer2011-12-18
* Fixed the Boogie build.Gravatar wuestholz2011-12-16
* Dafny: Made sure that error locations refer to the Dafny program, even if the...Gravatar wuestholz2011-12-15
* Boogie: Changed Expr.Not to keep swap arguments rather change direction of op...Gravatar Rustan Leino2011-12-12
* MergeGravatar Rustan Leino2011-12-07
|\
| * MergeGravatar Michal Moskal2011-12-07
| |\
| * | Fix atg file and add comment about Set/*Variable*/Gravatar Michal Moskal2011-12-07
| * | Make set iteration order deterministicGravatar Michal Moskal2011-12-07
* | | MergeGravatar Rustan Leino2011-12-05
|\ \ \ | | |/ | |/|
* | | Boogie: Added new abstract interpretation harness, which uses native Boogie E...Gravatar Rustan Leino2011-12-05
| |/ |/|
| * Emit attribute on a requiresGravatar akashlal2011-12-04
|/
* Added option of turning off model generation in SI. Can be very expensive som...Gravatar akashlal2011-11-26
* fixed bug in the inlineDepth option for houdiniGravatar qadeer2011-11-23
* MergeGravatar qadeer2011-11-22
|\
| * Boogie: don't resolve ignored types (that is, "extern" types that have been t...Gravatar Rustan Leino2011-11-22
* | added support for handling duplicate axiomsGravatar qadeer2011-11-22
|/
* Added lazy summary computation to stratified inlining (not finished yet)Gravatar akashlal2011-11-20
* commented calls to GC.Collect()Gravatar qadeer2011-11-18
* changed the semantics of requires and ensures for inlined proceduresGravatar qadeer2011-11-17
* Boogie: fixed build error (incorrect type in Contract.Result)Gravatar Rustan Leino2011-11-16
* MergeGravatar akashlal2011-11-16
|\
| * Debugging output for stratified inlining. Emit attribute on Ensures whileGravatar Unknown2011-11-16
* | Boogie (and Dafny, with effects also on SscBoogie): I refactored CommandLine...Gravatar Rustan Leino2011-11-15
|/