Skip to content

What's in the workspace?

Eric Hennenfent edited this page Mar 3, 2020 · 2 revisions

After running Manticore, you'll see a mcore_xxxxxx directory containing several files. If Manticore finished executing successfully, these will mostly describe the results of the run. The following describes what you can expect to find in this directory, depending on which architecture you're running:

All Architectures

  • command.sh - A text file containing the manticore command used to start this run
  • manticore.yml - A YAML file describing the configuration values set in this Manticore run
  • Various .pkl files - Saved Manticore states
  • [user | test]_xxxxxxxx.* - Test case files corresponding to each of the final states reached

Native

  • test_xxxxxxxx.argv - Concretized arguments passed to the target binary on the command line
  • test_xxxxxxxx.env - Concretized environment variables provided to the target binary
  • test_xxxxxxxx.input - A listing of all the input symbols provided to the binary, including stdin, argv, etc.
  • test_xxxxxxxx.messages - A summary of the final conditions of the program state that produced this testcase
  • test_xxxxxxxx.net - A dump of socket IO performed by this testcase
  • test_xxxxxxxx.pkl - A saved copy of the state that produced this testcase
  • test_xxxxxxxx.smt - The symbolic constraint set provided to Z3 for this testcase
  • test_xxxxxxxx.stderr - A dump of any stderr output emitted by this testcase
  • test_xxxxxxxx.stdin - Concretized stdin values provided to the target binary
  • test_xxxxxxxx.stdout - A dump of any stdout output emitted by this testcase
  • test_xxxxxxxx.syscalls - A trace of any system calls encountered by this test case
  • test_xxxxxxxx.trace - a trace of the instructions visited by this state
  • visited.txt - a dump of all the instructions visited across all of the states

EVM

  • user_xxxxxxxx.constraints - The constraint set provided to Z3 for this test case (similar to native .smt files)
  • user_xxxxxxxx.logs - Any log messages emitted by the smart contract under test
  • user_xxxxxxxx.pkl - A saved copy of the state that produced this testcase
  • user_xxxxxxxx.summary - A human-readable summary of the final state of the testcase
  • user_xxxxxxxx.trace - An instruction trace for this testcase
  • user_xxxxxxxx.tx - A human-readable record of the transactions made to produce this testcase
  • user_xxxxxxxx.tx.json - A JSON representation of the transactions
  • global.findings - The results of any detectors that were triggered during execution
  • global.summary - A summary of the code coverage across all states
  • global_.init_asm - Disassembly of the init bytecode
  • global_.init_visited - Visited instructions during contract initialization
  • global_.runtime_asm - Disassembly of the runtime bytecode
  • global_.runtime_visited - Visited instructions when the contract is running
  • global_.sol - The solidity source code for the contract
  • global__init.bytecode - The bytecode executed to initialize the contract
  • global__runtime.bytecode - The runtime bytecode of the contract