|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| None | __init__ (self) |
Public Attributes | |
| float | max = 1.7976931348623157e+308 |
| int | max_exp = 1024 |
| int | max_10_exp = 308 |
| float | min = 2.2250738585072014e-308 |
| int | min_exp = -1021 |
| int | min_10_exp = -307 |
| int | dig = 15 |
| int | mant_dig = 53 |
| float | epsilon = 2.220446049250313e-16 |
| int | radix = 2 |
| int | rounds = 1 |
Static Public Attributes | |
| _FloatInfo | float_info = _FloatInfo() |
| int | maxsize = 9223372036854775807 |
| int | maxunicode = 1114111 |
| str | byteorder = "little" |
| str | platform = "linux" |
| list | argv = [""] |
sys.float_info — IEEE-754 binary64 limits.
| None sys._FloatInfo.__init__ | ( | self | ) |
|
static |
|
static |
| int sys._FloatInfo.dig = 15 |
| float sys._FloatInfo.epsilon = 2.220446049250313e-16 |
|
static |
| int sys._FloatInfo.mant_dig = 53 |
| float sys._FloatInfo.max = 1.7976931348623157e+308 |
| int sys._FloatInfo.max_10_exp = 308 |
| int sys._FloatInfo.max_exp = 1024 |
|
static |
|
static |
| float sys._FloatInfo.min = 2.2250738585072014e-308 |
| int sys._FloatInfo.min_10_exp = -307 |
| int sys._FloatInfo.min_exp = -1021 |
|
static |
| int sys._FloatInfo.radix = 2 |
| int sys._FloatInfo.rounds = 1 |