changed output of formatNumberReadable so that it shows powers of two and one-less-than powers of two in a more compact format

This commit is contained in:
Ishtiaque Zahid
2022-11-14 17:37:38 +01:00
committed by chriseth
parent 310a58dd31
commit 3abf2724a1
13 changed files with 250 additions and 135 deletions
@@ -7,4 +7,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (95-100): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))
// Warning 4984: (95-100): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))
@@ -7,5 +7,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.
// Warning 4281: (77-82): CHC: Division by zero happens here.
@@ -8,4 +8,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))
@@ -8,5 +8,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 3944: (78-83): CHC: Underflow (resulting value less than -0x80 * 2**248) happens here.
// Warning 4984: (78-83): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
// Warning 3944: (78-83): CHC: Underflow (resulting value less than -2**255) happens here.
// Warning 4984: (78-83): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.
@@ -7,5 +7,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 3944: (77-82): CHC: Underflow (resulting value less than -0x80 * 2**248) happens here.
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
// Warning 3944: (77-82): CHC: Underflow (resulting value less than -2**255) happens here.
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.
@@ -7,5 +7,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 3944: (77-82): CHC: Underflow (resulting value less than -0x80 * 2**248) happens here.
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
// Warning 3944: (77-82): CHC: Underflow (resulting value less than -2**255) happens here.
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.
@@ -7,5 +7,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 3944: (77-82): CHC: Underflow (resulting value less than -0x80 * 2**248) happens here.
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
// Warning 3944: (77-82): CHC: Underflow (resulting value less than -2**255) happens here.
// Warning 4984: (77-82): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.
@@ -15,4 +15,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 4281: (85-90): CHC: Division by zero happens here.\nCounterexample:\n\na = 0\nb = 0\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
// Warning 4984: (242-248): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\n_check = true\n = 0\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n\nTransaction trace:\nC.constructor()\nC.g(true)
// Warning 4984: (242-248): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.\nCounterexample:\n\n_check = true\n = 0\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n\nTransaction trace:\nC.constructor()\nC.g(true)