sys Namespace Reference

Classes
class	_FloatInfo

Detailed Description

Operational model for the sys module.

Data only: the interpreter-state attributes a verification harness reads. The
standard streams (stdout/stderr/stdin), sys.exit and the frame/trace
introspection API are not modelled.

Values describe the 64-bit little-endian target ESBMC's C models assume and
the IEEE-754 binary64 float the frontend maps `float` onto; they match CPython
on that target. `platform` names the target the models assume, not the host
interpreter.

`version_info` is deliberately absent: the frontend does not dispatch
`__getitem__`, so the usual `sys.version_info[0]` would report a spurious
IndexError. An attribute-only stand-in that turns the common form into a false
alarm is worse than no attribute at all.