index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
new files for fixedpoint engine backend
Unknown
2013-05-07
*
merging changes for fixedpoint engine backend
Ken McMillan
2013-05-07
|
\
*
|
Adding fixedpoint engine backend
Ken McMillan
2013-05-07
|
*
havocs and updates to globals added only if they are non-null
Unknown
2013-05-06
|
*
Merge
Unknown
2013-05-06
|
|
\
|
*
|
fixed bug (reported by Akash) in treatment of linear parameters to calls
Unknown
2013-05-06
|
|
*
AbsHoudini: Each function can specify its own abstract domain. Also added
akashlal
2013-05-05
|
|
/
|
*
In the typecheck method of HavocCmd, added calls to typecheck the havoced vars
Unknown
2013-05-04
|
*
Merge
Unknown
2013-05-04
|
|
\
|
*
|
fixed bug reported by Akash
Unknown
2013-05-04
|
|
*
Print "\n" after a YieldCmd
akashlal
2013-05-03
|
|
*
Some code refactoring
akashlal
2013-05-03
|
|
/
|
*
add another test file
Unknown
2013-04-30
|
/
*
Merge
allydonaldson
2013-04-30
|
\
*
|
Staged Houdini
allydonaldson
2013-04-30
|
*
Added a little bit of virtual-ness to the Inliner class. This is so that I can
akashlal
2013-04-28
|
*
AbsHoudini: Bug fix
akashlal
2013-04-28
|
*
AbsHoudini: Added support for /errorLimit:n, n > 1
akashlal
2013-04-25
|
*
AbsHoudini: Added predicate-abstraction domain and some examples.
akashlal
2013-04-25
|
*
AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini,
akashlal
2013-04-25
|
*
added free ensures to each procedure to compensate for havocing of allocator
Unknown
2013-04-19
|
*
Test case for OG --> Houdini
akashlal
2013-04-19
|
*
Made OG-Desugared parsable as a Boogie program.
akashlal
2013-04-19
|
*
Added a test case
akashlal
2013-04-19
|
*
Merge
akashlal
2013-04-19
|
|
\
|
|
*
AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute,
akashlal
2013-04-19
|
*
|
Fix mod-set traversal to do visit code inside code expressions.
Rustan Leino
2013-04-18
|
|
/
|
*
AbsHoudini: Added support for /inlineDepth, and fixed the regression tests
akashlal
2013-04-18
|
*
Nice clean re-implementation of AbstractHoudini. And tests
akashlal
2013-04-18
|
*
refactored og and fixed latest bug reported by chris
Unknown
2013-03-20
|
*
the allocator corresponding to every linear variable
Unknown
2013-03-13
|
*
Added explicit mod set analysis calls to OG transform and linear transform
Unknown
2013-03-13
|
*
added mod set checking to the linear type checker
Unknown
2013-03-13
|
*
fixed bugs in linear and og
Unknown
2013-03-11
|
*
fixed bug in model printing
Unknown
2013-03-11
|
*
Added another constructor to CallCmd
akashlal
2013-03-11
|
*
Minor changes to AbstractHoudini
akashlal
2013-03-10
|
*
Merge
Unknown
2013-03-09
|
|
\
|
|
/
|
/
|
|
*
fixed emitter for CallCmd to include async
Unknown
2013-03-09
*
|
Refactored MatchCandidate
allydonaldson
2013-03-08
*
|
Merge
allydonaldson
2013-03-08
|
\
\
*
|
|
MatchCandidate modified to match candidates by variable name, rather than by ...
allydonaldson
2013-03-08
|
|
*
Merge
Unknown
2013-03-07
|
|
|
\
|
|
|
/
|
|
/
|
|
|
*
updated the model parsing (probably caused by some change in Z3's output)
Unknown
2013-03-07
|
|
*
added support for linear sets without useArrayTheory (but there is some incom...
Unknown
2013-03-07
|
*
|
Fix LeastCommonAncestor method in Graph module
Nathan Chong
2013-03-07
|
|
*
Merge
Unknown
2013-03-06
|
|
|
\
|
|
_
|
/
|
/
|
|
|
|
*
in the process of adding support for linear sets without /useArrayTheory
Unknown
2013-03-06
|
|
/
|
*
removed Test\GPUVerify
Unknown
2013-03-06
|
*
removing GPUVerify and Dafny.sln
Unknown
2013-03-05
[next]