Skip to main content

Module arm_semantics

Module arm_semantics 

Source
Expand description

ARM Semantics Encoding to SMT

Encodes ARM operation semantics as SMT bitvector formulas. Each ARM operation is translated to a mathematical formula that precisely captures its behavior, including register updates and condition flags.

Structsยง

ArmSemantics
ARM semantics encoder
ArmState
ARM processor state representation in SMT
ConditionFlags
ARM condition flags