Merge branch 'master' of https://github.com/AbsInt/CompCert

5 files changed, 35 insertions, 19 deletions

diff --git a/Makefile b/Makefile
index 3f87287e..896a456e 100644
--- a/Makefile
+++ b/Makefile
@@ -222,16 +222,16 @@ latexdoc:
 	@chmod -w $*.v
 
 compcert.ini: Makefile.config VERSION
-	(echo stdlib_path=$(LIBDIR); \
-         echo prepro=$(CPREPRO); \
-         echo asm=$(CASM); \
-         echo linker=$(CLINKER); \
-         echo arch=$(ARCH); \
-         echo model=$(MODEL); \
-         echo abi=$(ABI); \
-         echo system=$(SYSTEM); \
-         echo has_runtime_lib=$(HAS_RUNTIME_LIB); \
-         echo asm_supports_cfi=$(ASM_SUPPORTS_CFI); \
+	(echo "stdlib_path=$(LIBDIR)"; \
+         echo "prepro=$(CPREPRO)"; \
+         echo "asm=$(CASM)"; \
+         echo "linker=$(CLINKER)"; \
+         echo "arch=$(ARCH)"; \
+         echo "model=$(MODEL)"; \
+         echo "abi=$(ABI)"; \
+         echo "system=$(SYSTEM)"; \
+         echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
+         echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
          version=`cat VERSION`; \
          echo version=$$version) \
         > compcert.ini
diff --git a/configure b/configure
index fda59dab..80cb2bcd 100755
--- a/configure
+++ b/configure
@@ -154,7 +154,7 @@ case "$target" in
     abi="standard"
     system="macosx"
     cc="${toolprefix}gcc -arch i386"
-    cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' -E"
+    cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E"
     casm="${toolprefix}gcc -arch i386 -c"
     case `uname -r` in
       [1-9].*|10.*|11.*)    # up to MacOS 10.7 included
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index aff638e7..e73125f7 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -58,8 +58,6 @@ let get_config key =
 let bad_config key v =
   Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2
 
-let stdlib_path = get_config "stdlib_path"
-
 let prepro = get_config "prepro"
 let asm = get_config "asm"
 let linker = get_config "linker"
@@ -81,6 +79,13 @@ let has_runtime_lib =
   | "false" -> false
   | v -> bad_config "has_runtime_lib" v
 
+
+let stdlib_path =
+  if has_runtime_lib then
+    get_config "stdlib_path"
+  else
+    ""
+
 let asm_supports_cfi = 
   match get_config "asm_supports_cfi" with
   | "true" -> true
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 5c84af6b..41002bac 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -161,7 +161,7 @@ module MacOS_System =
      fprintf oc "_%s" s
 
     let symbol oc symb =
-      fprintf oc "%s" (extern_atom symb)
+      fprintf oc "_%s" (extern_atom symb)
 
     let label oc lbl =
       fprintf oc "L%d" lbl
@@ -206,7 +206,8 @@ module MacOS_System =
           fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s;
           fprintf oc "	.indirect_symbol %a\n" raw_symbol s;
           fprintf oc "	.long	0\n")
-        !indirect_symbols
+        !indirect_symbols;
+      indirect_symbols := StringSet.empty
 
   end:SYSTEM)
 
@@ -638,7 +639,6 @@ let print_builtin_inline oc name args res =
 let float64_literals : (int * int64) list ref = ref []
 let float32_literals : (int * int32) list ref = ref []
 let jumptables : (int * label list) list ref = ref []
-let indirect_symbols : StringSet.t ref = ref StringSet.empty
 
 (* Reminder on AT&T syntax: op source, dest *)
 
@@ -1042,4 +1042,6 @@ let print_program oc p =
                Target.raw_symbol "__negs_mask";
     fprintf oc "%a:	.long   0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n"
                Target.raw_symbol "__abss_mask"
-  end
+  end;
+  Target.print_epilogue oc
+
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index 874c2be3..53013337 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -58,7 +58,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ointconst n, nil => I n
   | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop
   | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop
-  | Oindirectsymbol id, nil => Ptr (Gl id Int.zero)
+  | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero)
   | Ocast8signed, v1 :: nil => sign_ext 8 v1
   | Ocast8unsigned, v1 :: nil => zero_ext 8 v1
   | Ocast16signed, v1 :: nil => sign_ext 16 v1
@@ -145,7 +145,16 @@ Proof.
   intros; apply symbol_address_sound; apply GENV.
 Qed.
 
-Hint Resolve symbol_address_sound: va.
+Lemma symbol_address_sound_2:
+  forall id ofs,
+  vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)).
+Proof.
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. 
+  constructor. constructor. apply GENV; auto.
+  constructor.
+Qed.
+
+Hint Resolve symbol_address_sound symbol_address_sound_2: va.
 
 Ltac InvHyps :=
   match goal with