| Commit message (Collapse) | Author | Age |
|
|
|
| |
linear_in, linear_out
|
| |
|
|\ |
|
| | |
|
| | |
|
|/ |
|
|
|
|
|
| |
added another test in linear (based on bug reported by Chris)
removed the QED build configuration
|
| |
|
|
|
|
| |
computing statement checksums).
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
advanced verification result caching even for implementations with errors.
|
|
|
|
| |
caching.
|
|
|
|
| |
injected by the verification result caching for calls within loops.
|
|
|
|
| |
preconditions.
|
|
|
|
| |
verification result caching.
|
|
|
|
| |
caching.
|
|
|
|
| |
caching.
|
|
|
|
| |
procedures and implementations
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
When running boogie form the command line, this should be on by default.
On the other hand, the TokenTextWriter constructors and PrintBplFile now have an
argument for this, but by default it is off.
|
| |
|
|
|
|
| |
argument instead of a boolean one.
|
| |
|
|
|
|
|
|
|
|
| |
numbers correctly.
For example BigDec.FromString("-1.5") would be interpreted as
-0.5 due to the incorrect way the method handles the fractional
part of the string.
|
|
|
|
| |
modified vars)
|
| |
|
|
|
|
| |
cause data races when we run parts of Boogie that both do mod set analysis at the same time.
|
|\ |
|
| | |
|
| |
| |
| |
| | |
sets elsewhere.
|
| |\ |
|
| | | |
|
| | |
| | |
| | |
| | | |
others already present for bool, BigNum and BigDec.
|
| |/
|/| |
|
| |
| |
| |
| | |
duplication of code
|
| | |
|
| | |
|
| | |
|
|\ \ |
|