diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-05 12:32:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-05 12:32:59 +0000 |
| commit | 6c0511a03c8c970435d8b97e600312ac45340801 (patch) | |
| tree | d42b16c8f77d1aa34e570647eb6728a4a9f4e72b /cfrontend/Csem.v | |
| parent | 81afbd38d1597cefc03dd699fd115c4261c6877f (diff) | |
| download | compcert-kvx-6c0511a03c8c970435d8b97e600312ac45340801.tar.gz compcert-kvx-6c0511a03c8c970435d8b97e600312ac45340801.zip | |
Revu traitement des variables globales dans AST.program et dans Globalenvs.
Adaptation frontend, backend en consequence.
Integration passe C -> C#minor dans common/Main.v.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Csem.v')
| -rw-r--r-- | cfrontend/Csem.v | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index b73e83cc..ed5a1b4c 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -367,12 +367,6 @@ Inductive cast : val -> type -> type -> val -> Prop := Definition genv := Genv.t fundef. -Definition globalenv (p: program) : genv := - Genv.globalenv (program_of_program p). - -Definition init_mem (p: program) : mem := - Genv.init_mem (program_of_program p). - (** Local environment *) Definition env := PTree.t block. (* map variable -> location *) @@ -743,8 +737,8 @@ End RELSEM. (** Execution of a whole program *) Definition exec_program (p: program) (t: trace) (r: val) : Prop := - let ge := globalenv p in - let m0 := init_mem p in + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in exists b, exists f, exists m1, Genv.find_symbol ge p.(prog_main) = Some b /\ Genv.find_funct_ptr ge b = Some f /\ |