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

1 files changed, 2 insertions, 2 deletions

diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 4c61918..558ae1c 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -516,7 +516,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State f f.(fn_body) k e m2)
 
   | step_external_function: forall ef vargs k m t vres m',
-      external_call ef (Genv.find_symbol ge) vargs m t vres m' ->
+      external_call ef ge vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
          t (Returnstate vres k m')        
 
@@ -554,7 +554,7 @@ Inductive final_state: state -> int -> Prop :=
 
 Definition global_var_env (p: program): gvarenv :=
   List.fold_left
-    (fun gve x => match x with (id, init, k) => PTree.set id k gve end)
+    (fun gve x => match x with (id, v) => PTree.set id (gvar_info v) gve end)
     p.(prog_vars) (PTree.empty var_kind).
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=