summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Collapse)AuthorAge
* Kill {:prover "..."} attribute support; no one ever used this stuffGravatar MichalMoskal2011-02-17
|
* Stratified inlining: Added concrete values to error traces. Added an extra ↵Gravatar akashlal2011-02-17
| | | | flag "inferLeastForUnsat".
* Fix with timeoutGravatar akashlal2011-02-12
|
* Better support for timeoutGravatar akashlal2011-02-12
|
* Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP ↵Gravatar MichalMoskal2011-02-11
| | | | provers. Add handling of help message about /proverOpt.
* Minor change to stratified inliningGravatar akashlal2011-02-11
|
* Added a new method StratifiedVC for refinement.Gravatar akashlal2011-02-08
| | | | Added a method to copy a FunctionCall.
* implemented /UseUnsatCoreForInlining option for use in stratified inliningGravatar qadeer2011-02-06
|
* deleted debugging statementGravatar akashlal2011-02-05
|
* Fix to counterexample generation for over-approx queryGravatar akashlal2011-02-05
|
* Don't treat "Inconclusive" answer as fatal when splitting.Gravatar MichalMoskal2011-02-02
|
* stratified inlining: minor fix to the call tree being savedGravatar akashlal2010-12-21
|
* stratified inlining: record the name of the main procedure.Gravatar akashlal2010-12-18
|
* Add new feature: {:selective_checking} on procedures. See testcase for a ↵Gravatar MichalMoskal2010-12-17
| | | | description (it was implemented in VCC before and is quite useful).
* Add functions generated in lambda-expansion of function body to top-level ↵Gravatar MichalMoskal2010-12-17
| | | | program declarations.
* stratified inlining: minor changes to coverage reporterGravatar akashlal2010-12-13
|
* Boogie: Did some minor refactoring.Gravatar wuestholz2010-12-10
|
* stratified inlining: added option of turning off CheckAssumptionsGravatar akashlal2010-12-07
|
* z3api: Bug fix with timeout. Use CheckAssumptions.Gravatar akashlal2010-12-07
|
* Added version.cs as link to those projects that were missing itGravatar stobies2010-12-06
| | | | Select 4.0 client profile on all projects
* Factored out the ParserHelper class into a separate project and updated the ↵Gravatar wuestholz2010-12-02
| | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
* Construct @MV_state function only once so it doesn't get renamed to ↵Gravatar MichalMoskal2010-12-02
| | | | @MV_state@@0 when we have more than one procedure to verify
* stratified inlining: small fixGravatar akashlal2010-12-01
|
* stratified inlining: reuse call tree across queriesGravatar akashlal2010-12-01
|
* Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.slnGravatar qadeer2010-12-01
|
* z3api: Print log in smtlib2 format. Use CheckAssumptions (currently broken)Gravatar akashlal2010-11-29
|
* Added CheckAssumptions api interfaceGravatar akashlal2010-11-28
|
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* small fix to previous checkinGravatar akashlal2010-11-24
|
* Some changes to the prover interface to make way for z3-api.Gravatar akashlal2010-11-24
|
* more refactoringGravatar akashlal2010-11-23
|
* More refactoringGravatar akashlal2010-11-23
|
* Refactoring: pulled out all code for stratified inlining to a new file.Gravatar akashlal2010-11-23
|
* Changed stratified inlining: can now be user-guidedGravatar akashlal2010-11-22
|
* Minor updates for printing coverage graph of stratified inliningGravatar akashlal2010-11-14
|
* ModelViewer:Gravatar rustanleino2010-11-02
| | | | | | | * map back values introduced by bool_2_U and int_2_U * map back internal names for select/store to [n] and [n:=], where n is the arity of the map * added /break switch to ModelViewer * display more things (including sequences) in Dafny provider
* Dafny: a partial first crack at a Dafny model-viewer provider, including ↵Gravatar rustanleino2010-11-01
| | | | captureState mark-ups in the Boogie code generated from Dafny
* Skip unchagned variables in model dumps. Fix testcaseGravatar MichalMoskal2010-10-14
|
* Bug fixes and speed up for doomed program point analysisGravatar schaef2010-10-13
|
* Add interfaces for langauge providers. Start with VCC provider.Gravatar MichalMoskal2010-10-12
|
* Put Model.cs in separate assembly. Fix signing/versioning with it.Gravatar MichalMoskal2010-10-12
|
* Add missing Clone() when storing incarnation maps; update testcase to make ↵Gravatar MichalMoskal2010-10-12
| | | | | | this clear Construct states in Model properly, nuke direct printing.
* Add function and constant viewGravatar MichalMoskal2010-10-12
|
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
|
* Boogie:Gravatar rustanleino2010-10-12
| | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
* Boogie: fixed a Code Contract in the sourceGravatar rustanleino2010-10-09
|
* Fixes in state printing/initializationGravatar MichalMoskal2010-10-09
|
* Fix some bugs.Gravatar MichalMoskal2010-10-09
|
* Add model/state printing and parsingGravatar MichalMoskal2010-10-09
|
* Add state sequence API and creation, still untestedGravatar MichalMoskal2010-10-08
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 17:00:33 +0000