summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
Commit message (Collapse)AuthorAge
* Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
|
* Add simplified may-unverified analysis and instrumentation.Gravatar Valentin Wüstholz2015-11-20
|
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
|
* Add support for annotating implementations with k-ind. depth.Gravatar Valentin Wüstholz2015-10-29
|
* Improve output for diagnosing timeouts.Gravatar Valentin Wüstholz2015-09-30
|
* updateGravatar Shaz Qadeer2015-09-28
|
* Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Rustan Leino2015-08-28
|\ | | | | | | | | | | | | | | | | | | Conflicts: Source/Core/CommandLineOptions.cs Source/ExecutionEngine/ExecutionEngine.cs Source/ExecutionEngine/VerificationResultCache.cs Source/VCGeneration/VC.cs Test/snapshots/runtest.snapshot Test/snapshots/runtest.snapshot.expect
* | Added /verifySnapshots:3, which prints recycled errors messages with the ↵Gravatar Rustan Leino2015-08-28
| | | | | | | | source locations of the new code.
| * Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
|/ | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
* Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
|
* Fixed minor issue.Gravatar wuestholz2015-01-26
|
* Minor changeGravatar wuestholz2015-01-26
|
* Fixed a postcondition.Gravatar wuestholz2014-12-26
|
* Added an annotation, :split_here, for predicate statements.Gravatar Bryan Parno2014-12-16
| | | | | | The annotation allows the programmer to manually indicate where the verification of a procedure implementation should be split into pieces.
* Fixed issue in the verification result caching.Gravatar wuestholz2014-11-10
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-17
|
* fixed StackOverflow in TraceCounterexample;Gravatar qadeer2014-09-30
| | | | converted tail recursion into a loop
* Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
|
* Did some refactoring.Gravatar wuestholz2014-09-23
|
* fixed codexpr bug reported by Michael Emmi; removed special handling of ↵Gravatar qadeer2014-08-08
| | | | codexpr in InjectPostConditions
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
* 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.
* OnModel now carries the result of the prover callGravatar akashlal2014-06-28
|
* Added mechanism for getting the variables referenced by a loop (not just the ↵Gravatar Ally Donaldson2014-06-09
| | | | modified vars)
* Made VarsAssignedInLoop public, since it can be useful in computing modifies ↵Gravatar Ally Donaldson2014-06-06
| | | | sets elsewhere.
* Add support for assumption variables.Gravatar wuestholz2014-04-21
|
* Changed all lambda-expression rewriting to be done as a pre-processing step ↵Gravatar Rustan Leino2014-02-28
| | | | | | before real verification. Fixed treatment of lambda-expression attributes.
* Fixed errors in the use of Code ContractsGravatar Rustan Leino2014-02-10
|
* Added functionality to rename state captures when programs are unrolled.Gravatar Ally Donaldson2014-01-17
|
* Integrated support for k-induction, implemented a while ago by Philipp ↵Gravatar Ally Donaldson2014-01-17
| | | | Ruemmer but never previously committed.
* Resolve a concurrency issue (reported by Alex Summers).Gravatar wuestholz2013-12-12
|
* Patch by Nathan Chong: iterative version of remove empty blocks algorithm. ↵Gravatar Ally Donaldson2013-12-02
| | | | This appears to fix a small deficiency in the original recursive implementation, so now a larger number of empty blocks are removed. As a result, various tests produce slightly different counterexamples and have been updated to reflect this. Also, default VC generation strategy has been changed to DAGIterative, to avoid stack overflow problems.
* MergeGravatar Pantazis Deligiannis2013-10-09
|\
* | small refactoringGravatar Pantazis Deligiannis2013-10-02
| |
* | support for disabling loop entry invariant assertion checkingGravatar Pantazis Deligiannis2013-10-01
| |
* | changes to support a configured errorLimitGravatar Pantazis Deligiannis2013-09-30
| |
* | more changes towards parallelisation of HoudiniGravatar Pantazis Deligiannis2013-09-29
| |
| * refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of ↵Gravatar qadeer2013-09-09
| | | | | | | | GenerateVC
| * fixed bug introduced by the last checkin in letvciterativeGravatar qadeer2013-09-08
| | | | | | | | added /vc:i to all tests in stratifiedinline
| * fixed the problem with codexprsGravatar qadeer2013-09-07
| | | | | | | | now positive/negative context is detected and appropriate translation is done
| * When a codeexpr is used at the top-level in an assume statement, we use the ↵Gravatar qadeer2013-09-04
| | | | | | | | alternative existential semantics.
| * Factored out the closure for codeexpr conversion so that it can be reused.Gravatar qadeer2013-09-04
| | | | | | | | Enabled it in stratified inlining.
| * Applied Chris Hawblitzel's changes to deal with {:expand}Gravatar qadeer2013-08-23
| | | | | | | | Erased {:yields} in the resulting sequential program in OwickiGriesTransform
* | MergeGravatar Pantazis Deligiannis2013-08-20
|\|
* | new option to disable checking for loop maintained invariants - this leads ↵Gravatar Pantazis Deligiannis2013-08-15
| | | | | | | | to an underapproximation that helps to speedup houdini refutation of candidates
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 13:39:30 +0000