From 53b57751c1981e0bce3aa470e426a12034bb165e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 17 Sep 2006 08:58:05 +0000
Subject: Ajout de Init_pointer (experimental)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/AST.v | 3 ++-
 common/Mem.v | 7 ++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'common')

diff --git a/common/AST.v b/common/AST.v
index 673f1d81..5b8c997a 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -62,7 +62,8 @@ Inductive init_data: Set :=
   | Init_int32: int -> init_data
   | Init_float32: float -> init_data
   | Init_float64: float -> init_data
-  | Init_space: Z -> init_data.
+  | Init_space: Z -> init_data
+  | Init_pointer: list init_data -> init_data.
 
 (** Whole programs consist of:
 - a collection of function definitions (name and description);
diff --git a/common/Mem.v b/common/Mem.v
index 7af696e1..679c41e1 100644
--- a/common/Mem.v
+++ b/common/Mem.v
@@ -636,6 +636,9 @@ Fixpoint contents_init_data (pos: Z) (id: list init_data) {struct id}: contentma
       store_contents Size64 (contents_init_data (pos + 8) id') pos (Vfloat f)
   | Init_space n :: id' =>
       contents_init_data (pos + Zmax n 0) id'
+  | Init_pointer x :: id' =>
+      (* Not handled properly yet *)
+      contents_init_data (pos + 4) id'
   end.
 
 Definition size_init_data (id: init_data) : Z :=
@@ -646,6 +649,7 @@ Definition size_init_data (id: init_data) : Z :=
   | Init_float32 _ => 4
   | Init_float64 _ => 8
   | Init_space n => Zmax n 0
+  | Init_pointer _ => 4
   end.
 
 Definition size_init_data_list (id: list init_data): Z :=
@@ -679,6 +683,7 @@ Proof.
   unfold size_init_data in H; destruct a;
   try (apply H1; [reflexivity|assumption]).
   apply IHid. generalize (Zmax2 z 0). omega. 
+  apply IHid. omega. 
 Qed.
 
 Definition block_init_data (id: list init_data) : block_contents :=
@@ -2136,7 +2141,7 @@ Proof.
   destruct a;
   try (apply H1; [reflexivity|repeat constructor]).
   apply IHid. generalize (Zmax2 z 0). omega. simpl in H0; omega.
-
+  apply IHid. omega. simpl size_init_data in H0. omega. 
   apply H. omega. unfold sz0. omega.
 Qed.
 
-- 
cgit