1extern void write_object(
2    char *out_file_name);
3
4/* FROM line 196 */
5extern void number_to_chars_littleendian (char *, signed_expr_t, int);
6extern void number_to_chars_bigendian (char *, signed_expr_t, int);
7