push_string
static __inline void push_string(char *);
push_string(bstrdup(str));
push_string(read_string(&bmachine.readstack[bmachine.readsp]));