| Commit message (Collapse) | Author | Age | Files |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
If the variable is an argument that is passed by-reference, and, if its
value is changed during the execution of the system, its reference will
be propagated until here. Consequently, in the post-state of the system,
the value of the variable in the pre-state will be equal to the value in
the post-state. This is an error. Thus, we copy the value instead of
using a reference (initially introduced for performance reason).
|
| |
|
|
|
|
| |
`this->foo` is considered as a borrowing variable, with the type
`TYPE_EXTERNAL`. Verifications use the contract registry and the binded
class of specifications.
|
| |
|
|
|
| |
Create the sub-library `Hoa\Praspel\AssertionChecker` and introduce
$this support through “implicit variables”.
|
| | |
|
| | |
|
|
|
A borrowing variable represents a link between two variables (kind a
redirection). It is useful to create link between pre- and post-state in
the contract, such as \old(…).
|
