summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
Commit message (Collapse)AuthorAge
* Make set iteration order deterministicGravatar Michal Moskal2011-12-07
| | | | Make the set class generic
* Boogie: Fixed a crash due to old expressions in lambda expressions that were ↵Gravatar wuestholz2011-12-02
| | | | | | not replaced after lambda expansion. (reported by Florian Egli)
* Remove invariant that was just wrongGravatar Michal Moskal2011-11-28
|
* Added option of turning off model generation in SI. Can be very expensive ↵Gravatar akashlal2011-11-26
| | | | sometimes.
* minor bug fix in SIGravatar akashlal2011-11-24
|
* minor changes to summary computationGravatar akashlal2011-11-24
|
* fixes to summary computationGravatar Unknown2011-11-22
|
* Added lazy summary computation to stratified inlining (not finished yet)Gravatar akashlal2011-11-20
|
* Dafny: fixed bad Code ContractsGravatar Rustan Leino2011-11-16
|
* refactoring houdini so that it creates only a single instance of z3Gravatar qadeer2011-11-16
|
* Eliminated unused argument in the constructor for CheckerGravatar qadeer2011-11-16
|
* MergeGravatar akashlal2011-11-16
|\
| * Debugging output for stratified inlining. Emit attribute on Ensures whileGravatar Unknown2011-11-16
| | | | | | | | printing it.
* | 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.
* MergeGravatar qadeer2011-11-07
|\
* | change in model parsing with datatype valuesGravatar qadeer2011-11-07
| |
* | Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
| |
* | Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
| |
* | Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵Gravatar Rustan Leino2011-10-27
| | | | | | | | as if the old /bv:z were used
* | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵Gravatar Rustan Leino2011-10-27
| | | | | | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
| * various refactoringsGravatar qadeer2011-10-27
|/
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
|
* revised implementation of proc copy boundingGravatar qadeer2011-10-16
|
* Bug fix to stratified inlining error trace valuesGravatar Unknown2011-09-28
|
* Name the constant used in @MV_state function applications - otherwise we get ↵Gravatar Michal Moskal2011-09-26
| | | | invalid Z3 files
* fixed bug in data value generationGravatar qadeer2011-09-13
|
* Added some extra functionality to Model code for corralGravatar Unknown2011-09-13
|
* fixes to model value generation for stratified inliningGravatar qadeer2011-09-12
|
* further fixesGravatar qadeer2011-09-08
|
* minor fixesGravatar qadeer2011-09-07
|
* MergeGravatar qadeer2011-09-07
|\
| * Improvement for ProcCopyBoundingGravatar Unknown2011-09-07
| |
* | bug fixGravatar qadeer2011-09-06
| |
* | further fixesGravatar qadeer2011-09-06
| |
* | partial check in regarding getting states working with stratified inliningGravatar qadeer2011-09-06
|/
* Options.PostParse() is called by Parse(), so set command-line-derived ↵Gravatar Michal Moskal2011-08-30
| | | | options before calling Parse()
* Bug fix for Proc-Copy-BoundingGravatar Unknown2011-08-28
|
* Procedure Copy Bounding for Stratified InlinigGravatar Unknown2011-08-25
|
* reverting irreducible handling temporarilyGravatar qadeer2011-08-21
|\
* | added code to handle irreducible graphsGravatar qadeer2011-08-20
| |
* | minor refactoringGravatar qadeer2011-08-17
| |
* | deleted lazyinlining option 2 and 3Gravatar qadeer2011-08-17
| | | | | | | | fixed proc copy bounding
* | Added "procedure-copy bounding" for lazy inliningGravatar Unknown2011-08-10
| |
* | further changes for making houdini workGravatar qadeer2011-08-04
|/
* ported all the counterexample code to Michal's new Model class; the goal is ↵Gravatar Unknown2011-06-27
| | | | to eliminate the class ErrorModel from the codebase.
* Fixed non-incremental option of stratified inliningGravatar Unknown2011-06-27
|
* FindLeastToVerify: accept multiple proceduresGravatar Unknown2011-06-26
|
* Avoid restarting the theorem prover for stratified inlining because itGravatar Unknown2011-06-25
| | | | | can lose context. Added a cache for FindLeastToVerify
* early clearing of live variables and incarnation mapsGravatar qadeer2011-06-24
|
* implementation of iterative LetVCGravatar qadeer2011-06-23
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 10:44:18 +0000