parser.constant_annotations Namespace Reference

Functions
bool	_fits_int64 (int v)
bool	_is_usub_unaryop (object node)
None	_tag_bignum_constants (object node, bool in_usub_operand=False)
str	_spell_nonfinite (float v)
None	_tag_nonfinite_floats (object node)
None	tag_nonfinite_floats (object node)
str	encode_bytes (bytes value)
None	annotate_constant_node (ast.AST value_node)
None	add_type_annotation (ast.Assign node)
None	tag_bignum_constants (object node)

Variables
	_INT64_MIN = -(1 << 63)
tuple	_INT64_MAX = (1 << 63) - 1

Detailed Description

Constant-annotation helpers used by parser orchestration.

Function Documentation

_fits_int64()

bool parser.constant_annotations._fits_int64 ( int v )

protected

_is_usub_unaryop()

bool parser.constant_annotations._is_usub_unaryop ( object node )

protected

_spell_nonfinite()

str parser.constant_annotations._spell_nonfinite ( float v )

protected

_tag_bignum_constants()

None parser.constant_annotations._tag_bignum_constants ( object node, bool in_usub_operand = False )

protected

_tag_nonfinite_floats()

None parser.constant_annotations._tag_nonfinite_floats ( object node )

protected

add_type_annotation()

None parser.constant_annotations.add_type_annotation

(

ast.Assign

node

)

Propagate annotation to assignment RHS constant values.

annotate_constant_node()

None parser.constant_annotations.annotate_constant_node

(

ast.AST

value_node

)

Attach ESBMC-specific type metadata to supported Constant nodes.

encode_bytes()

str parser.constant_annotations.encode_bytes

(

bytes

value

)

Encode raw bytes as ASCII base64 for JSON transport.

tag_bignum_constants()

None parser.constant_annotations.tag_bignum_constants

(

object

node

)

Public façade for bigint tagging in AST-JSON dictionaries.

tag_nonfinite_floats()

None parser.constant_annotations.tag_nonfinite_floats

(

object

node

)

Public façade for non-finite float tagging in AST-JSON dictionaries.

Variable Documentation

_INT64_MAX

tuple parser.constant_annotations._INT64_MAX = (1 << 63) - 1

protected

_INT64_MIN

parser.constant_annotations._INT64_MIN = -(1 << 63)

protected