summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* updated the linear type system based on Chris' design with linear, ↵Gravatar qadeer2014-07-15
| | | | linear_in, linear_out
* fixed a regression failureGravatar qadeer2014-07-15
|
* mergeGravatar qadeer2014-07-15
|\
* | simplified yield type chcking and added treiber stack (not fully done)Gravatar qadeer2014-07-15
| |
| * Fixed a minor issue.Gravatar wuestholz2014-07-14
| |
| * Refactored how checksums are computed.Gravatar wuestholz2014-07-13
|/
* added testsGravatar qadeer2014-07-12
|
* fixed some tests in ogGravatar qadeer2014-07-11
| | | | | added another test in linear (based on bug reported by Chris) removed the QED build configuration
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching (ignore comments for ↵Gravatar wuestholz2014-07-10
| | | | computing statement checksums).
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-09
|
* Worked on adding support for "canned errors".Gravatar wuestholz2014-07-07
|
* Added more tests and worked on adding support for "canned errors".Gravatar wuestholz2014-07-06
|
* Worked on adding support for "canned errors".Gravatar wuestholz2014-07-06
|
* Did some refactoring, fixed minor issues, and made it apply the more ↵Gravatar wuestholz2014-07-06
| | | | advanced verification result caching even for implementations with errors.
* Made it collect more statistics about the more advanced verification result ↵Gravatar wuestholz2014-07-04
| | | | caching.
* Implemented an optimization for assignments to assumption variables that are ↵Gravatar wuestholz2014-07-04
| | | | injected by the verification result caching for calls within loops.
* Made it not include free preconditions when producing partially verified ↵Gravatar wuestholz2014-07-03
| | | | preconditions.
* Fixed issue involving axioms in the dependency analysis used for ↵Gravatar wuestholz2014-07-03
| | | | verification result caching.
* Made it collect more statistics about the more advanced verification result ↵Gravatar wuestholz2014-07-01
| | | | caching.
* Made it collect some statistics about the more advanced verification result ↵Gravatar wuestholz2014-06-30
| | | | caching.
* a fix in Inline method; it should look for inline attribute only on ↵Gravatar qadeer2014-06-28
| | | | procedures and implementations
* Added a program cache (used by the more advanced verification result caching).Gravatar wuestholz2014-06-28
|
* Minor refactoringGravatar wuestholz2014-06-28
|
* Changed the verification result cache to use the built-in 'MemoryCache' class.Gravatar wuestholz2014-06-28
|
* OnModel now carries the result of the prover callGravatar akashlal2014-06-28
|
* Fix in SI while dealing with timeoutsGravatar akashlal2014-06-27
|
* Optimized the way that assertions are marked as partially verified.Gravatar wuestholz2014-06-26
|
* Fixed issue in verification result caching.Gravatar wuestholz2014-06-26
|
* Optimized the way that dependency checkums are computed.Gravatar wuestholz2014-06-26
|
* Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"Gravatar Dan Rosén2014-06-24
| | | | | | 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.
* Worked on an extension of the existing verification result caching.Gravatar wuestholz2014-06-23
|
* Changed the 'verifySnapshots' command-line option to accept a numeric ↵Gravatar wuestholz2014-06-20
| | | | argument instead of a boolean one.
* Fixed crash in resolverGravatar Rustan Leino2014-06-19
|
* Fix bug in BigDec.FromString() which would not parse negativeGravatar Dan Liew2014-06-18
| | | | | | | | 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.
* Added mechanism for getting the variables referenced by a loop (not just the ↵Gravatar Ally Donaldson2014-06-09
| | | | modified vars)
* Fixed a bug in revised mod set analysisGravatar Ally Donaldson2014-06-06
|
* Refactored modset analysis to avoid the use of static fields. Static fields ↵Gravatar Ally Donaldson2014-06-06
| | | | cause data races when we run parts of Boogie that both do mod set analysis at the same time.
* MergeGravatar Ally Donaldson2014-06-06
|\
* | Small refactoringGravatar Ally Donaldson2014-06-06
| |
* | Made VarsAssignedInLoop public, since it can be useful in computing modifies ↵Gravatar Ally Donaldson2014-06-06
| | | | | | | | sets elsewhere.
| * updated golden outputs and removed irrelevant testsGravatar qadeer2014-06-02
| |
| * MergeGravatar qadeer2014-06-02
| |\
| * | various fixesGravatar qadeer2014-06-02
| | |
| | * Added more tests (snapshots).Gravatar wuestholz2014-05-30
| | |
| | * Add isBvConst and asBvConst accessors to LiteralExpr to match theGravatar Dan Liew2014-05-28
| | | | | | | | | | | | others already present for bool, BigNum and BigDec.
| | * Documented the clean.py scriptGravatar Dan Liew2014-05-28
| | |
| | * Document lit's ``-s`` option.Gravatar Dan Liew2014-05-28
| | |
| | * Merge.Gravatar Dan Liew2014-05-28
| | |\
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-22 15:07:10 +0000