From 3a050b22f37f3c79a10a8ebae3d292fa77e91b76 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 23 May 2010 15:26:33 +0000 Subject: More faithful semantics for volatile reads and writes. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'cfrontend/Cminorgen.v') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 4ed4bc8..e60de3d 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -599,10 +599,10 @@ Definition build_compilenv (globenv, 0). Definition assign_global_variable - (ce: compilenv) (info: ident * list init_data * var_kind) : compilenv := + (ce: compilenv) (info: ident * globvar var_kind) : compilenv := match info with - | (id, _, Vscalar chunk) => PMap.set id (Var_global_scalar chunk) ce - | (id, _, Varray _) => PMap.set id Var_global_array ce + | (id, mkglobvar (Vscalar chunk) _ _ _ ) => PMap.set id (Var_global_scalar chunk) ce + | (id, mkglobvar (Varray _) _ _ _) => PMap.set id Var_global_array ce end. Definition build_global_compilenv (p: Csharpminor.program) : compilenv := -- cgit v1.2.3