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/LTLin.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/LTLin.v')
-rw-r--r-- | backend/LTLin.v | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/backend/LTLin.v b/backend/LTLin.v index 368c13cd..da8719ac 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -100,18 +100,33 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := Inductive stackframe : Set := | Stackframe: - forall (res: loc) (f: function) (sp: val) (ls: locset) (c: code), + forall (res: loc) (**r where to store the result *) + (f: function) (**r calling function *) + (sp: val) (**r stack pointer in calling function *) + (ls: locset) (**r location state in calling function *) + (c: code), (**r program point in calling function *) stackframe. Inductive state : Set := | State: - forall (stack: list stackframe) (f: function) (sp: val) - (c: code) (ls: locset) (m: mem), state + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r function currently executing *) + (sp: val) (**r stack pointer *) + (c: code) (**r current program point *) + (ls: locset) (**r location state *) + (m: mem), (**r memory state *) + state | Callstate: - forall (stack: list stackframe) (f: fundef) (ls: locset) (m: mem), + forall (stack: list stackframe) (**r call stack *) + (f: fundef) (**r function to call *) + (ls: locset) (**r location state at point of call *) + (m: mem), (**r memory state *) state | Returnstate: - forall (stack: list stackframe) (sig: signature) (ls: locset) (m: mem), + forall (stack: list stackframe) (**r call stack *) + (sig: signature) (**r signature of returning function *) + (ls: locset) (**r location state at point of return *) + (m: mem), (**r memory state *) state. Definition parent_locset (stack: list stackframe) : locset := |