summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver/BoogieDriver.cs
Commit message (Collapse)AuthorAge
* houdini cleanup continuedGravatar qadeer2012-03-10
|
* small fix for a bug I introduced during the refactoring of InferAndVerifyGravatar qadeer2012-03-02
|
* various refactorings related to houdiniGravatar qadeer2012-03-02
|
* further fixes related to using uninterpreted function for error tracesGravatar qadeer2012-02-25
| | | | removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution
* bug fixes related to using ControlFlowFunction instead of labelsGravatar qadeer2012-02-23
|
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
| | | | see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx
* Dafny: changed translation to be sensitive to refinement inheritance; this ↵Gravatar Rustan Leino2012-01-09
| | | | feature is now functional, provided the refining module does not add or change anything
* Boogie: output number of proof obligations (asserts) along with timing ↵Gravatar Rustan Leino2012-01-09
| | | | information when using the /trace option
* MergeGravatar Rustan Leino2011-12-05
|\
* | Boogie: Added new abstract interpretation harness, which uses native Boogie ↵Gravatar Rustan Leino2011-12-05
| | | | | | | | | | | | | | | | Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred}
| * added more instrumentation to HoudiniGravatar qadeer2011-12-05
| | | | | | | | | | when vcgen fails, instead of stopping houdini, the failing vc is added to a list of blacklisted vcs fixed bug in the call graph generation when inlining is used
| * added a mechanism for supplying the list of input bpl files inside a .txt fileGravatar qadeer2011-12-01
|/
* added some more statistics to houdiniGravatar qadeer2011-11-24
| | | | added a coupe more regressions for houdini+inlineDepth
* fixed bug in the inlineDepth option for houdiniGravatar qadeer2011-11-23
| | | | small clean up in the inlining implementation
* commented calls to GC.Collect()Gravatar qadeer2011-11-18
|
* /contractInfer always prints the computed assignment nowGravatar qadeer2011-11-16
| | | | enabled the houdini regressions
* Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵Gravatar Rustan Leino2011-11-15
| | | | CommandLineOptions to separate the options that belong to these 3 tools.
* added the option /inlineDepth:n. This option defaults to -1. If the user ↵Gravatar qadeer2011-11-13
| | | | | | provides a non-negative number then that number is used to inline procedures not annotated by {:inline n} attribute.
* moved the addition of selectors and testers to program.ResolveGravatar qadeer2011-11-11
|
* copied all attributes of the constructor (except for :constructor) to the ↵Gravatar qadeer2011-11-09
| | | | selector and membership functions
* added membership testsGravatar qadeer2011-10-05
|
* implementing datatypesGravatar qadeer2011-10-05
|
* updated Houdini so it works with SMTLibGravatar qadeer2011-09-27
|
* further updates to bit vector analysisGravatar qadeer2011-08-09
|
* various changes to boogie for bitvector analysis and bctproviderGravatar qadeer2011-08-08
|
* further changes for making houdini workGravatar qadeer2011-08-04
|
* cleaned up houdini optionsGravatar qadeer2011-08-04
|
* Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
| | | | | can lose context. Added a cache for FindLeastToVerify
* Boogie: added features to help with modular verification. In particular, ↵Gravatar Rustan Leino2011-05-13
| | | | define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations.
* Stratified inlining: Added concrete values to error traces. Added an extra ↵Gravatar akashlal2011-02-17
| | | | flag "inferLeastForUnsat".
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
|
* Add functions generated in lambda-expansion of function body to top-level ↵Gravatar MichalMoskal2010-12-17
| | | | program declarations.
* Refactoring: pulled out all code for stratified inlining to a new file.Gravatar akashlal2010-11-23
|
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
|
* Get rid of some CCI dependencies in DriverGravatar MichalMoskal2010-10-07
|
* Boogie:Gravatar rustanleino2010-09-23
| | | | | | * Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument
* Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome.Gravatar akashlal2010-09-18
|
* Dafny:Gravatar rustanleino2010-09-14
| | | | | | | | * Added internal support for multi-dimensional arrays (but not all surface syntax is there yet) * Removed unused variables from Dafny.atg Boogie and Dafny: * Improved error message for postcondition violations
* Fix for extractLoopsGravatar akashlal2010-09-04
|
* Added a way of recovering counterexample paths after loop extraction. ↵Gravatar akashlal2010-09-01
| | | | Stable, but still buggy.
* Boogie: Removed a completed task commentGravatar tabarbe2010-08-19
|
* Added the option /extractLoops to extract loops as procedure calls. If ↵Gravatar qadeer2010-08-11
| | | | either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
* Boogie: Changed BoogieDriver.cs to use a copy of cce.cs, rather than an ↵Gravatar tabarbe2010-07-30
| | | | internal cce.cs class.
* <Boogie> <BoogieDriver> Committing my porting of BoogieDriver.cs and the ↵Gravatar tabarbe2010-07-14
| | | | | | | changes made to the .csproj and Boogie.sln file that are necessary for the port. My Microsoft alias is t-abarbe, so if any of this stuff breaks for you, you can contact me. </BoogieDriver> </Boogie>
* Renaming the old boogiedriver sources in preparation for syncing my ported ↵Gravatar tabarbe2010-07-13
| | | | changes.
* These 2 files are remnants of attempting the earlier planned method of ↵Gravatar tabarbe2010-07-01
| | | | | | renaming the .ssc files to .cs. They are being deleted because my porting work will be done completely on my local disc, until such time that I want to merge ported code into the project. With regards to the renaming problem, Stephan Tobies has found that the logs are kept on the CodePlex server, and are just not provided to the SVN client. He has created a Codeplex work item at http://codeplex.codeplex.com/workitem/25490. If it gets voted up sufficiently, it may get CodePlex to provide that log information, and thus help with future work regarding the Boogie depot.
* I am working to port Boogie from Spec# to C#. As part of this process, I ↵Gravatar tabarbe2010-06-30
need to rename the .ssc files to .cs. Unfortunately, using the Tortoise SVN Source Control software, the changelog of the files I rename is lost. (I welcome anyone's ideas on how to do a more efficient/useful rename.) I will then port using VS 2010, creating a duplicate project on my harddisk, and translating it to pure C#. When I have my code successfully compiling, I will replace the Spec# version with my C# porting, run regressions, and if successful, commit my changes. Editing Boogie in Spec# should still function with the .ssc files renamed to .cs files.
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-05 02:26:38 +0000