extern void write_object(
    char *out_file_name);

/* FROM line 196 */
extern void number_to_chars_littleendian (char *, signed_expr_t, int);
extern void number_to_chars_bigendian (char *, signed_expr_t, int);