Scribble Functions
User defined functions are useful to avoid repeating similar expressions in multiple locations in the contract.
Consider the following example, we can see that the operations (x + 10) and (x + 10) * delta are repeated multiple times.
contract ExampleContract {uint delta;function set_delta(uint _delta) public {delta = _delta;}/// #if_succeeds {:msg "P0"} y == (x + 10) * delta + 15;function example(uint x, uint y) public returns (uint result) {...}/// #if_succeeds {:msg "P1"} y == (x + 10) * delta + x + 10;function example2(uint x, uint y) public returns (uint result) {...}}
This can be simplified by implementing user defined functions for (x+10) and (x+10) * delta above the smart contract. These functions get instrumented as internal functions in the contract. Hence they will be restricted to the contract that they are defined.
/// #define add10(uint x) uint = x + 10;/// #define complex_operation(uint y) uint = add10(y) * delta;contract ExampleContract {uint delta;function set_delta(uint _delta) public {delta = _delta;}/// #if_succeeds {:msg "P0"} y == complex_operation(x) + 15;function example(uint x, uint y) public returns (uint result) {...}/// #if_succeeds {:msg "P1"} y == complex_operation(x) + add10(x);function example2(uint x, uint y) public returns (uint result) {...}}
These user defined functions are restricted to being solidity view functions, so they cannot modify any state but can still access the state variables as shown in the above example.
User defined functions can be used by all inheriting contracts. Their bodies are restricted to a single side-effect free expression.
