| Commit message (Collapse) | Author | Age |
|\ |
|
| | |
|
| |\ |
|
| | |
| | |
| | |
| | | |
a Chalice release.
|
| | | |
|
| | |\ |
|
| | | | |
|
| | | |\
| | | |/
| | |/| |
|
| | | | |
|
| | |\ \ |
|
| | | | | |
|
| | | |/
| | |/|
| | | |
| | | | |
fixed proc copy bounding
|
| | | |\
| | | |/
| | |/| |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- changed the way candidate conditions are discovered; now it simply uses
all sub-expressions found in the spec that evaluate to TrueLiteral
- changed the implementation so that when trying to infer a precondition,
try out several different possibilities (and see which one works)
- added some very basic (and incomplete) type inference
- fixed a bug in the Modularizer (it didn't fix the solution after trying
out the spec infered from the solution)
- fixed a bug in DafnyModelUtils so that now when reading from the boogie
model file it keeps getting information from Seq# functions until
reaching a fixpoint (that's needed because the order or reads is important)
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
same
I will open a plugin branch to make more deeper changes until everything is stable
|
| | |\ \ |
|
| | | | | |
|
| | | |\ \
| | | |/ /
| | |/| | |
|
| | |\ \ \ |
|
| | | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
the general heap uses.
Updated regressions.
|
| | |/ / /
| |/| | | |
|
| |\ \ \ \ |
|
| | | | | |\
| | | |_|_|/
| | |/| | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
- added concreteValues field to HeapInstance
- brought back reading from Seq#Build when restoring Boogie models
- changed the how the candidate conditions are inferred: now it only
looks for unmodifiable concrete fields
- method in parameter values are added to the list of potential
candidate conditions
|
| | |/ / / |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
AssertionInjector: Check for invalid source locations (FeeFee) so they don't
confuse the injection.
|
| | | |/
| | |/| |
|
| |/ /
| | |
| | |
| | | |
be passed to Chalice
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- changed the synthesis of the Valid() function to synthesize both unrolled
and recursive definition of it, because both are needed in certain cases
- to make the recursive definition of Valid() work, a "decreases" clause is
needed. For now, decreases clause is always "decreases Repr", and that
seems to be enough for now.
|
| | |
| | |
| | |
| | | |
that now a simple example like Node.Tail work.
|
| |\ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- added "modifiable objects" to heap instance
- when verifying synthesized program, only fields of the modifiable
objects are considered
|
| | | | |
|
| | |\ \ |
|
| | | | | |
|
| | | | | |
|
| | |\ \ \ |
|
| | | | | | |
|
| | | |/ / |
|
| | | |\ \ |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
reported at end of analysis
|
| | | | | | |
|
| | | |/ / |
|
| | | |\ \ |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
BCT now links to CCI in CodeBox, get the CodeBox tree into C:\CCICodeBox
|
| | |_|/ /
| |/| | | |
|
| |\| | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
infrastructural things have been implemented, like handling return parameters,
generating different "fresh" spec for methods than for constructors,
adding "Valid()" to method preconditions.
|
| | |/ / |
|