Skip to content

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

Open
@caiosabarros

Description

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

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