Require Addr.
Extraction NoInline ad_double ad_double_plus_un.