index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
/
VCGeneration
/
StratifiedVC.cs
Commit message (
Expand
)
Author
Age
*
Merging complete. Everything looks good *crosses fingers*
Checkmate50
2016-06-06
*
VC gen for security properties
akashlal
2015-04-05
*
Compute MustReach information lazily, on-demand
akashlal
2015-03-16
*
Added MustReach information to VC gen
akashlal
2015-03-11
*
Handle timeout in refinement loop
akashlal
2015-01-28
*
SI: print if a bound was reached.
akashlal
2014-10-29
*
Minor corrections
akashlal
2014-10-01
*
SI: VC gen with labels
akashlal
2014-09-29
*
Cleanup: removed unused code
akashlal
2014-09-29
*
Fix to VC gen
akashlal
2014-09-28
*
Fix for boolVC generation
akashlal
2014-09-27
*
Lets have a setter for TopLevelDeclarations as well
akashlal
2014-09-25
*
minor fix
akashlal
2014-09-24
*
Simple VC generation for SI
akashlal
2014-09-24
*
Did more refactoring and addressed several todos.
wuestholz
2014-09-23
*
Did some refactoring.
wuestholz
2014-09-23
*
Bug fix in SI
akashlal
2014-08-03
*
Some simplifications
akashlal
2014-07-28
*
OnModel now carries the result of the prover call
akashlal
2014-06-28
*
Fix in SI while dealing with timeouts
akashlal
2014-06-27
*
keep some stats for debugging
akashlal
2014-05-15
*
Added stack bounding
akashlal
2014-05-10
*
Recursive walking of Exprs doesn't play nice when the depth of the AST is high.
akashlal
2014-01-07
*
code cleanup
akashlal
2013-11-02
*
And a test case
akashlal
2013-10-21
*
Bug fix in stratified inlining (triggered by {:inline} functions)
akashlal
2013-10-21
*
Merge
Pantazis Deligiannis
2013-10-09
|
\
*
|
changes to support a configured errorLimit
Pantazis Deligiannis
2013-09-30
|
*
refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of Genera...
qadeer
2013-09-09
|
*
Factored out the closure for codeexpr conversion so that it can be reused.
qadeer
2013-09-04
|
/
*
Fixed several build errors in the 'Checked' configuration.
wuestholz
2013-08-05
*
ExprSeq: farewell
Ally Donaldson
2013-07-22
*
BlockSeq: farewell
Ally Donaldson
2013-07-22
*
CmdSeq: farewell
Ally Donaldson
2013-07-22
*
Started to remove ...Seq classes
Ally Donaldson
2013-07-22
*
More refactoring
Ally Donaldson
2013-07-22
*
More refactoring towards replacing PureCollections.Sequence with List
Ally Donaldson
2013-07-22
*
merge
Pantazis Deligiannis
2013-07-22
|
\
|
*
Large refactoring of Hashtable to Dictionary.
Ally Donaldson
2013-07-22
|
*
Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a plai...
Ally Donaldson
2013-07-22
*
|
merge
Pantazis Deligiannis
2013-07-06
|
\
|
|
*
Did some refactoring in the execution engine and worked on the parallelization.
wuestholz
2013-07-01
*
|
merged more CVC4 and Z3 SMTLIB2 parsing methods ... results into a more compa...
pantazis
2013-06-13
|
/
*
Parse integers returned by Z3 into BigNum
akashlal
2013-01-29
*
Use the new ProverInterface's Evaluate method in stratified inlinig
Unknown
2013-01-03
*
bunch of refactorings
Unknown
2012-10-03
*
Removed AIFramework from Boogie -- use native trivial or native interval-base...
boehmes
2012-09-27
*
deleted an unused class
qadeer
2012-06-12
*
refactoring in SI
qadeer
2012-06-12
*
1. changed new SI implemnetation so that it performs substitution for call sites
qadeer
2012-06-10
[next]