diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-05 13:41:45 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-05 13:41:45 +0000 |
commit | c0bc146622528e3d52534909f5ae5cd2e375da8f (patch) | |
tree | 52c5f163a82b04d7ad56055b4bd5e852be168ae4 /backend/Machabstr.v | |
parent | adc9e990a0c338cef57ff1bd9717adcc781f283c (diff) | |
download | compcert-c0bc146622528e3d52534909f5ae5cd2e375da8f.tar.gz compcert-c0bc146622528e3d52534909f5ae5cd2e375da8f.zip |
Documentation
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Machabstr.v')
-rw-r--r-- | backend/Machabstr.v | 40 |
1 files changed, 19 insertions, 21 deletions
diff --git a/backend/Machabstr.v b/backend/Machabstr.v index ad4e8e1a..0abdd1e1 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -102,38 +102,36 @@ Definition extcall_arguments (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop := extcall_args rs fr (Conventions.loc_arguments sg) args. -(** The components of an execution state are: - -- [State cs f sp c rs fr m]: [f] is the function currently executing. - [sp] is the stack pointer. [c] is the list of instructions that - remain to be executed. [rs] assigns values to registers. - [fr] is the current frame, as described above. [m] is the memory state. -- [Callstate cs f rs m]: [f] is the function definition being called. - [rs] is the current values of registers, - and [m] the current memory state. -- [Returnstate cs rs m]: [rs] is the current values of registers, - and [m] the current memory state. - -[cs] is a list of stack frames [Stackframe f sp c fr], -where [f] is the block reference for the calling function, -[c] the code within this function that follows the call instruction, -[sp] its stack pointer, and [fr] its private frame. *) +(** Mach execution states. *) Inductive stackframe: Set := | Stackframe: - forall (f: function) (sp: val) (c: code) (fr: frame), + forall (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (c: code) (**r program point in calling function *) + (fr: frame), (**r frame state in calling function *) stackframe. Inductive state: Set := | State: - forall (stack: list stackframe) (f: function) (sp: val) - (c: code) (rs: regset) (fr: frame) (m: mem), + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r function currently executing *) + (sp: val) (**r stack pointer *) + (c: code) (**r current program point *) + (rs: regset) (**r register state *) + (fr: frame) (**r frame state *) + (m: mem), (**r memory state *) state | Callstate: - forall (stack: list stackframe) (f: fundef) (rs: regset) (m: mem), + forall (stack: list stackframe) (**r call stack *) + (f: fundef) (**r function to call *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) state | Returnstate: - forall (stack: list stackframe) (rs: regset) (m: mem), + forall (stack: list stackframe) (**r call stack *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) state. (** [parent_frame s] returns the frame of the calling function. |