With following solidity code: <div class="highlight highlight-source-solidity notr

Wow, also that printing is horrible, it needs to be more tight: <div class="snippe

BTW, this also helped inspire me to write a PR <a class="issue-link js-issue-link" dat

The inputs for this branch then becomes <div class="highlight highlight-text-adblo

Fixed in <a class="issue-link js-issue-link" data-error-text="Failed to load title" da

Just to be clear, it now prints: <div class="snippet-clipboard-content notranslate

BTW, this also helped inspire me to write a PR <a class="issue-link js-is

Fixed in <a class="issue-link js-issue-link" data-error-text="Failed to load title" da

Display `SymAddr "caller"` in `formatCex` function when call `hevm --get-models` about hevm HOT 7 CLOSED

ethever commented on September 15, 2024

Display `SymAddr "caller"` in `formatCex` function when call `hevm --get-models`

from hevm.

Comments (7)

msooseth commented on September 15, 2024 1

Wow, also that printing is horrible, it needs to be more tight:

--- Branch ---

Inputs:

  Calldata:
    0x0dbe671f
  
  Transaction Context:
    TxValue: 0x0
  

End State:

Should look like:

--- Branch ---

Inputs:
  Calldata:
    0x0dbe671f
  Transaction Context:
    TxValue: 0x0
  
End State:

I'm fixing this and also will try to add the Addrs...

from hevm.

msooseth commented on September 15, 2024 1

BTW, this also helped inspire me to write a PR #539 to improve the symbolic execution tutorial :) Thanks again!

from hevm.

ethever commented on September 15, 2024

The inputs for this branch then becomes

--- Branch ---

Inputs:

  Calldata:
    0x0dbe671f
  
  Addrs:
    SymAddr "caller": 0x95222290DD7278Aa3Ddd389Cc1E1d165CC4BAfe5
  
  Transaction Context:
    TxValue: 0x0

from hevm.

msooseth commented on September 15, 2024

Fixed in #535

Thanks again. Once it's reviewed, I'll merge!

from hevm.

msooseth commented on September 15, 2024

Just to be clear, it now prints:

Discovered the following 1 counterexample(s):

Calldata:
  0x0dbe671f
Storage:
  Addr SymAddr "origin": []
  Addr LitAddr 0x388C818CA8B9251b393131C08a736A67ccB19297: []
Transaction Context:
  TxValue: 0x0
Addrs:
  SymAddr "caller": 0x0000000000000000000000000000000000000000


=== Reachable Expression ===
...

=== Models for 5 branches ===

--- Branch ---
Inputs:
  Calldata:
    Empty
End State:
  (Failure
....

--- Branch ---
Inputs:
  Calldata:
    0x0dbe671f
  Transaction Context:
    TxValue: 0x0
  Addrs:
    SymAddr "caller": 0x95222290DD7278Aa3Ddd389Cc1E1d165CC4BAfe5
End State:
  (Success
    Data:
      (ConcreteBuf "")

    State:
      (SymAddr "entrypoint"):
...

from hevm.

ethever commented on September 15, 2024