summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* stratified inlining: record the name of the main procedure.Gravatar akashlal2010-12-18
|
* Improve handling of arrays embedded in structsGravatar MichalMoskal2010-12-17
|
* 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.
* A couple of bug fixesGravatar akashlal2010-12-16
|
* fixed a couple of issues:Gravatar qadeer2010-12-16
| | | | | 1. eliminated special case for alloc 2. added iteration over out parameters in VisitCallCmd
* Better handling of user provided skolem variablesGravatar MichalMoskal2010-12-16
|
* Search in long names, not the short onesGravatar MichalMoskal2010-12-16
|
* Cleanup up the inlining codeGravatar qadeer2010-12-15
| | | | | 1. For some reason, constructors weren't being inlined. Now they can be. 2. Cleaned up the search for implementations
* Changed the behavior of /doModSetAnalysis so thatGravatar qadeer2010-12-15
| | | | | (1) Boogie errors due to modifies clause mismatch are suppressed (2) modset analysis is performed and modifies clauses of procedures with implementations are updated
* Display ghost localsGravatar MichalMoskal2010-12-15
|
* Add reload-model option. Bugfixes when switching modelsGravatar MichalMoskal2010-12-15
|
* Include one more expert level (this need to be rethought I guess).Gravatar MichalMoskal2010-12-14
| | | | Display res__ VCC variables.
* Add information about field being volatileGravatar MichalMoskal2010-12-14
|
* Support arrays and & pseudo-fieldGravatar MichalMoskal2010-12-14
|
* Add Func.OptEval function and some docsGravatar MichalMoskal2010-12-14
|
* stratified inlining: minor changes to coverage reporterGravatar akashlal2010-12-13
|
* Rework the namer interface a bitGravatar MichalMoskal2010-12-10
|
* Improve type detectionGravatar MichalMoskal2010-12-10
|
* Yet another icon updateGravatar MichalMoskal2010-12-10
|
* Fix typoGravatar MichalMoskal2010-12-10
|
* Improve the iconGravatar MichalMoskal2010-12-10
|
* Add an icon. Get rid of SearchBox (not used).Gravatar MichalMoskal2010-12-10
|
* Boogie: Did some minor refactoring.Gravatar wuestholz2010-12-10
|
* Display Skolem constants (no functions yet)Gravatar MichalMoskal2010-12-10
|
* Allow for model selection if there are multiple in the fileGravatar MichalMoskal2010-12-10
|
* Use a made-up name when Context.Lookup() cannot find a nameGravatar MichalMoskal2010-12-10
|
* Don't crash in Context.Lookup when the namer has never seen the name. This ↵Gravatar MichalMoskal2010-12-10
| | | | happens when the name is never used in the VC (e.g. it gets peep-hole optimized).
* Add ToString() overrides to help in debuggingGravatar MichalMoskal2010-12-10
|
* Rename BVD binary to (suprise!) BVDGravatar MichalMoskal2010-12-08
|
* stratified inlining: added option of turning off CheckAssumptionsGravatar akashlal2010-12-07
|
* z3api: Bug fix with timeout. Use CheckAssumptions.Gravatar akashlal2010-12-07
|
* Move CCE to 4.0Gravatar MichalMoskal2010-12-06
|
* Ignore one more VCC functionGravatar MichalMoskal2010-12-06
|
* One more link to version.csGravatar stobies2010-12-06
|
* Removed superfluous app.configGravatar stobies2010-12-06
|
* 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
* Get rid of F# dependencies - use System.Numerics and a custom Rational ↵Gravatar MichalMoskal2010-12-02
| | | | structure instead
* Set output directory to Binaries/Gravatar MichalMoskal2010-12-02
|
* Introduce node categories; sort fields based on that not special charactersGravatar MichalMoskal2010-12-01
|
* 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
|
* forgot to check this file inGravatar qadeer2010-11-28
|
* Added CheckAssumptions api interfaceGravatar akashlal2010-11-28
|
* added a fix for a bug in the Evaluate function.Gravatar qadeer2010-11-27
|
* changed the procedure Check so that the conflict clause is blocked only when ↵Gravatar qadeer2010-11-27
| | | | more than one counterexample is needed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-03 16:30:35 +0000