| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
|
| | |
|
| |
|
|
|
|
| |
* enhanced the printing of captured states
* addressed some warnings issued by VS 2010
* some code formatting
|
| | |
|
| |
|
|
|
| |
* Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators.
* Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time.
|
| |
|
|
|
|
| |
* 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
|
| |
|
|
|
| |
only this target has a compile time dependency on Microsoft.Z3.dll.
To compile this target, a reference to z3api must be manually added to BoogieDriver.
|
| |
|
|
| |
fewer error messages when compiling with runtime checking on.
|
| |
|
|
| |
doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
|
| |
|
|
| |
project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
|
| |
|
|
| |
Z3api.csproj shouldn't get in the way this time 'round.
|
| |
|
|
| |
files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
|
| |
|
|
| |
Core to jive with recent changes made to the cce class.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Contract.EnsuresOnThrow<>()
|
| |
|
|
| |
use separate Z3 type per Boogie type
|
| | |
|
| | |
|
| |
|
|
| |
-z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).
|
| | |
|
| |
|
|
| |
for better performance on VCs that are heavy on bitvector arithmetic
|
| |
|
|
| |
svn-ignoring some build artifacts
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
projects which have a (more up-to-date) copy of cce.cs.
|
| |
|
|
| |
the version information.
|
| |
|
|
| |
project; making Core work with the port by removing the nonnull requirements on one abstract method.
|
| |
|
|
| |
were pointing to the yet-to-exist C# version.
|
| | |
|
| |
|
|
| |
structured.
|
| | |
|
| |
|
|
| |
rather than Provers.Z3. I updated that.
|
| |
|
|
| |
that it matches the namespace.
|
| |
|
|
| |
Contracts dll) in AbsInt, Isabelle, and Z3
|
| |
|
|
| |
Contracts Extensions - utility methods for the port that are not present in Code Contracts.)
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
of the project.
|
| |
|
|
| |
typo in the Spec# version of Z3's ProverInterface.ssc
|
| |
|
|
| |
/stratifiedInline:1.
|
| |
|
|
|
|
|
|
|
| |
* Set Z3's QI_COST as the sum of "weight" and "generation", not their product. This worked better when setting the :weight of a quantifier (see below).
Dafny:
* Improved axiomatization of sequences; in particular, use an axiom to generate terms that say what the two pieces of a concatenation are
* Two of the (previous) sequence axioms could cause a matching loop, in cases where Z3's arithmetic reasoning does not infer all rational arithmetic equalities during instantiation. The effect of this was apparently not noticed before, perhaps the concatenation/drop properties previously had to be supplied in manual assert statements. But now, with the improved sequence axiomatization (see previous bullet), this effect became remarkably noticeable. To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results.
* Removed several assert lemmas that are no longer needed in Test programs (the test programs now contain only about a handful of such lemmas)
|
| |
|
|
| |
option is activated by /lazyInline:2. The original method is activated by /lazyInline:1.
|
| |
|
|
|
|
| |
variable analysis as well
2. Separeted model printing from the lazy inlining option
|
| |
|
|
|
| |
2. Added code for printing array partitions
3. Set UseAbstractInterpretation=false in case lazy inlining is being used
|
qadeer