scribble
scribble copied to clipboard
Consensys
Scribble instrumentation tool
The typing logic for `SId` is split between several functions: `tcId`, `tcIdVariable`, `tcLetAnnotation`, `tcUserConstant`, `lookupFun`, `lookupVarDef`, `lookupTypeDef`, `tcIdBuiltinSymbol`, `tcIdImportUnitRef`. Whats worse, there are 2 redundant styles of checking types: a)...
Hi, I am encountering a compilation error in the Scribble generated `ReentrancyUtils` file. The file I am instrumenting has the following data structure: `mapping(address => uint256) private _valueMap;` I ran...
In our smart contracts, there are several properties dependent on the state variables which need to be initialized through the constructor. In one such instance, we need to check that...
Currently low-level tools (such as the Harvey fuzzer) report a bytecode offset where a user-provided assertion failure was detected. This is usually the offset of the `LOG1` instruction that corresponds...
As described in #163 we changed the scribble type-checker to reject annotations that talk about private state variables of base contracts. So for example it would reject samples such as...
Is it possible to achieve something like this? ```solidity contract Vault { struct Account { uint256 id; uint256 shares; } mapping(address => Account) accounts; uint256 totalShares; /// #invariant unchecked_sum(accounts.shares) ==...
Scribble is sometimes used to instrument the code for local testing. When this is done in a Hardhat environment, people often use `console.log(...)` to print out various information. In this...
We have use cases for comparing strings, arrays and structs in properties. However the base Solidity language doesn't support equality comparison of non-value types. We could add structural equality comparison...
With #128 we added an internal yaml schema checker function in `yaml.ts`. This is overkill, and should be replaced with an external library (e.g. https://www.npmjs.com/package/yaml-schema-validator). Note that it would be...
Instrumentation turns the following terminating code into non-terminating code: ```solidity contract Foo { function double1(uint x) public view returns (uint) { return double2(x); } /// if_succeeds $result == double1(x); function...