		Search-engine friendly clone of the ACL2 documentation.

*gcc-builtin*

gcc-builtin-vars

A partial list of variables built-in to GCC.

This list consists of variables corresponding to certain x86 registers. We could not find mention of these variables in the GCC manual, but they have been observed in practical code.

See dimb-transunit for further discussion of these variables.

Definition: *gcc-builtin-vars*

(defconst *gcc-builtin-vars*
  (list (ident "__eax")
        (ident "__ebp")
        (ident "__ebx")
        (ident "__ecx")
        (ident "__edi")
        (ident "__edx")
        (ident "__esi")
        (ident "__esp")))