search

christoftorres / Osiris

A tool to detect integer bugs in Ethereum smart contracts (ACSAC 2018).
62 stars 17 forks source link

Osiris finds no bugs in example Division.sol contract #5

Open lukasdenk opened 4 years ago

lukasdenk commented 4 years ago

Hello,

When I try to test the Division.sol contract with the Docker, Osiris does not find any bugs (even after uncommenting the first function). Why? I used this command inside the docker: python osiris/osiris.py -s datasets/Division/Division.sol

contract Division {

function unsigned_division(uint32 x, uint32 y) returns (int r) {
  //if (y == 0) { throw; }
  r = x / y;
}

function signed_division(int x, int y) returns (int) {
  //if ((y == 0) || ((x == -2**255) && (y == -1))) { throw; }
  return x / y;
}
}

The result:

  .oooooo.             o8o            o8o
 d8P'  `Y8b            `"'            `"'
888      888  .oooo.o oooo  oooo d8b oooo   .oooo.o
888      888 d88(  "8 `888  `888""8P `888  d88(  "8
888      888 `"Y88b.   888   888      888  `"Y88b.
`88b    d88' o.  )88b  888   888      888  o.  )88b
 `Y8bood8P'  8""888P' o888o d888b    o888o 8""888P'

INFO:root:Contract datasets/Division/Division.sol:Division:
INFO:symExec:Running, please wait...
INFO:symExec:   ============ Results ===========
INFO:symExec:     EVM code coverage:     99.4%
INFO:symExec:     Arithmetic bugs:       False
INFO:symExec:     └> Overflow bugs:      False
INFO:symExec:     └> Underflow bugs:     False
INFO:symExec:     └> Division bugs:      False
INFO:symExec:     └> Modulo bugs:        False
INFO:symExec:     └> Truncation bugs:    False
INFO:symExec:     └> Signedness bugs:    False
INFO:symExec:     Callstack bug:         False
INFO:symExec:     Concurrency bug:       False
INFO:symExec:     Time dependency bug:   False
INFO:symExec:     Reentrancy bug:        False
INFO:symExec:    --- 1.09610509872 seconds ---
INFO:symExec:   ====== Analysis Completed ======