scribble:npm install in the directory containing the tutorial:truffle and ganache-cli and any remaining dependencies.scribble-getting-started/in-place-testing directory of the repository you should find a simple Truffle project. Under contracts/ there are 2 contracts of interest - a base contract Managed that contains some logic for adding and removing administrators and a test contract Test that extendsManaged.Managed.sol, is that only current administrators may call the addAdminInternal function. The contract Test violates that property - Test.addAdmin calls addAdminInternal without first checking if the caller is an admin.
As a first try we can add the following annotation in Managed.sol (extra brownie points if you see something weird already ;)):#if_succeeds specifies that the predicate should only be checked if the addAdminInternal function succeeds.{:msg "only owner can add admins"} provides a human-readable message to help remind you what this property is checking. As shorthand you can skip the {:msg } and only specify "only owner can add admins".admins[msg.sender] is the actual property. Its a valid boolean Solidity expression. In this case we are saying that the value of admin[msg.sender] must be true upon successful execution of addAdminInternal.test/tests.js in which a random user tries to add himself as an admin.scribble created a .instrumented version for Managed.sol. Indeed we should see the new under contracts:__scribble_ReentrancyUtils.sol. This is a contract for internal use that scribble always emits..instrumented file with its original counterpart and re-run the tests. Since we don't want to loose our original files, lets first copy the originals to the side:ganache-cli by running:admin[msg.sender] predicate was evaluated - it was evaluated after the function had successfully executed, at which point the sender had already added themselves to the admin map. To fix this, we want to talk about the value of admin[msg.sender] before the function started executing. We can do this using the old()operator, which specifies that scribble should compute the value of a given expression before the function is called.--armand --disarm..sol.instrumented and .sol.original files is annoying. So scribble provides you with two options that take care of this for you.--arm option when instrumenting, then scribble will automatically create .sol.original copies of the original files, and swap the instrumented files in-place, so you can start testing immediately. So now that we have fixed our annotation, lets use --arm and --disarm.--disarm option:.original and .instrumented files, as well as other auxilary files emitted by scribble are all removed:.instrumented files for debugging purposes, add the --keep-instrumented option when disarming.--no-assert option:--no-assert option tells scribble to not emit an explicit assert(false) on failure, and instead just emit an event. As a result, the tests may not fail anymore, but if you run them with--show-eventsyou will see all the failing properties:AssertionFailed event. Its text contains the human-readable label from the original annotation.