Skip to content

Getting Internal Error For Different Commands When Trying To Execute Symbolic On Live Contracts 聽#989

Description

@caiosabarros

Hi! Thanks for the tool! Just started using it, but having some problems so far. Any guidance is appreciated 馃憤

Here are the commands I have tried:
First Command:

$ hevm symbolic --rpc $ETH_RPC_URL --address 0x2A8e1E676Ec238d8A992307B495b45B3fEAa5e86 --assertions '[0x01, 0x11]'

Second Command:

$ hevm symbolic --rpc $ETH_RPC_URL --code $(seth code 0x2A8e1E676Ec238d8A992307B495b45B3fEAa5e86) --assertions '[0x01, 0x11]'

Here are the errors I am getting:
Error for first command:

Exploring contract
hevm: Internal Error: contract marked external not found in cache -- CallStack (from HasCallStack):
  internalError, called at src/EVM.hs:1316:26 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM
CallStack (from HasCallStack):
  error, called at src/EVM/Types.hs:1344:19 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.Types
  internalError, called at src/EVM.hs:1316:26 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM

Partial Output and Error for second command:

Exploring contract
Simplifying expression
Explored contract (37 branches)

WARNING: hevm was only able to partially explore the given contract due to the following issues:

  - Unexpected Symbolic Arguments to Opcode
    msg: "Unable to determine a call target"
    program counter: 2535
    arguments:
      (SLoad
        slot:
          24440054405305269366569402256811496959409073762505157381672968839269610695612]
// ...
Checking for reachability of 2 potential property violation(s)
hevm: Internal Error: TODO: implement copySlice with a symbolically sized region -- CallStack (from HasCallStack):
  internalError, called at src/EVM/SMT.hs:899:23 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.SMT
CallStack (from HasCallStack):
  error, called at src/EVM/Types.hs:1344:19 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.Types
  internalError, called at src/EVM/SMT.hs:899:23 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.SMT
hevm: thread blocked indefinitely in an MVar operation

I was triyng to follow this article from the EF.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions