  In this paper, we show a new approach to transformations of an imperative
program with function calls and global variables into a logically constrained
term rewriting system. The resulting system represents transitions of the whole
execution environment with a call stack. More precisely, we prepare a function
symbol for the whole environment, which stores values for global variables and
a call stack as its arguments. For a function call, we prepare rewrite rules to
push the frame to the stack and to pop it after the execution. Any running
frame is located at the top of the stack, and statements accessing global
variables are represented by rewrite rules for the environment symbol. We show
a precise transformation based on the approach and prove its correctness.
