trailofbits/manticore
1
0
Fork 0
mirror of https://github.com/trailofbits/manticore.git synced 2026-10-11 22:29:55 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix: typos (#2615)

Browse Source
This commit is contained in:
omahs
2023-01-13 16:10:05 -05:00
committed by GitHub
parent 49e0438578
commit dc8c3c822b
2 changed files with 8 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
README.md
+1 -1
View File
@@ -104,7 +104,7 @@ $ manticore examples/evm/umd_example.sol
##### Manticore-verifier
An alternative CLI tool is provided that simplifys contract testing and
An alternative CLI tool is provided that simplifies contract testing and
allows writing properties methods in the same high-level language the contract uses.
Checkout manticore-verifier [documentation](http://manticore.readthedocs.io/en/latest/verifier.html).
See a [demo](https://asciinema.org/a/xd0XYe6EqHCibae0RP6c7sJVE)
docs/verifier.rst
+7 -7
View File
@@ -6,7 +6,7 @@ Manticore installs a separated CLI tool to do property based symbolic execution
**manticore-verifier** initializes an emulated blockchain environment with a configurable set of
accounts and then sends various symbolic transactions to the target contract containing property methods.
If a way to break a property is found the full transaction trace to reproduce the behaivor is provided.
If a way to break a property is found the full transaction trace to reproduce the behavior is provided.
A configurable stopping condition bounds the exploration, properties not failing are considered to pass.
@@ -48,8 +48,8 @@ Reverting property are any property method that contains "revert". For example:
Selecting a target contract
===========================
**manticore-verifier** needs to be pointed to a the target contract containing any number of property methods.
The target contract is the entry point of the exploration. It needs to initilize any internal structure or external contracts to a correct initial state. All methods of this contract matching the property name criteria will be tested. ::
**manticore-verifier** needs to be pointed to the target contract containing any number of property methods.
The target contract is the entry point of the exploration. It needs to initialize any internal structure or external contracts to a correct initial state. All methods of this contract matching the property name criteria will be tested. ::
--contract_name CONTRACT_NAME The target contract name defined in the source code
@@ -57,7 +57,7 @@ The target contract is the entry point of the exploration. It needs to initilize
User accounts
=============
You can specify what are the accounts used in the exploration.
Normaly you do not want the owner or deployer of the contract to send the symbolic transaction and to use a separate unused account to actually check the property methods.
Normally you do not want the owner or deployer of the contract to send the symbolic transaction and to use a separate unused account to actually check the property methods.
There are 3 types of user accounts:
- deployer: The account used to create the target contract
@@ -90,12 +90,12 @@ The exploration will continue to send symbolic transactions until one of the sto
Maximum number of transactions
-----------------------------
You can be interested only in what could happen under a number of transactions. After a maximun number of transactions is reached the explorations ends. Properties that had not be found to be breakable are considered a pass.
You can be interested only in what could happen under a number of transactions. After a maximum number of transactions is reached the explorations ends. Properties that had not been found to be breakable are considered a pass.
You can modify the max number of transactions to test vis a command line argument, otherwise it will stop at 3 transactions. ::
--maxt MAXT Max transaction count to explore
Maximun coverage % attained
Maximum coverage % attained
---------------------------
By default, if a transaction does not produce new coverage, the exploration is stopped. But you can add a further constraint so that if the provided coverage percentage is obtained, stop. Note that this is the total % of runtime bytecode covered. By default, compilers add dead code, and also in this case the runtime contains the code of the properties methods. So use with care. ::
@@ -105,7 +105,7 @@ By default, if a transaction does not produce new coverage, the exploration is s
Timeout
-------
Exploration will stop after the timeout seconds have pass. ::
Exploration will stop after the timeout seconds have passed. ::
--timeout TIMEOUT Exploration timeout in seconds