summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Move block predicator to VCGenerationGravatar Peter Collingbourne2012-06-18
* GPUVerify: implement is-a-constant analysisGravatar Peter Collingbourne2012-06-15
* Merging againGravatar Ken McMillan2012-06-07
|\
| * Trying to merge with recent changes, failing.Gravatar Ken McMillan2012-06-05
| |\
| | * Some changes to support expanded use of z3api.Gravatar Ken McMillan2012-06-05
* | | Boogie: add /printCFG command line option, which prints each implementation's...Gravatar Peter Collingbourne2012-06-06
|/ /
* | moved class Macro to AbsyGravatar qadeer2012-06-04
* | MergeGravatar qadeer2012-06-01
|\ \
* | | changed behavior of InlinedEnsures so that free ensures is skipped unless an ...Gravatar qadeer2012-06-01
| * | 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an a...Gravatar Unknown2012-06-01
|/ /
* | No need for extra attributes in ExtractLoopsGravatar akashlal2012-05-28
* | Better interface for adding skipped calls, andGravatar akashlal2012-05-26
* | MergeGravatar Unknown2012-05-25
|\ \
* | | Adding an option for deterministicExtractLoops, that uses an alternate way to...Gravatar Unknown2012-05-25
| * | MergeGravatar qadeer2012-05-24
| |\ \ | |/ / |/| |
| * | more refactoring in stratified inliningGravatar qadeer2012-05-24
* | | Boogie: document /typeEncoding:mGravatar Peter Collingbourne2012-05-22
|/ /
* | 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
| |\