aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-08-21 14:08:31 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-08-21 14:08:31 +0200
commit44df927b7e562240ca7ecbb29be8b5b1881f3c05 (patch)
tree7ad708224a74c65a9957b416a7fecc1cebb0627d /ia32
parentd0319112f1fc01b648542e66eb1597ac7b14e49c (diff)
downloadcompcert-kvx-44df927b7e562240ca7ecbb29be8b5b1881f3c05.tar.gz
compcert-kvx-44df927b7e562240ca7ecbb29be8b5b1881f3c05.zip
Asmexpand for ARM: fixed bug in Pfreeframe.
Plus: update comments and credit Bernhard Schommer.
Diffstat (limited to 'ia32')
-rw-r--r--ia32/Asmexpand.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 177f6989..137b61b5 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -3,6 +3,7 @@
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
@@ -11,8 +12,7 @@
(* *********************************************************************)
(* Expanding built-ins and some pseudo-instructions by rewriting
- of the IA32 assembly code. Currently not done, this expansion
- is performed on the fly in PrintAsm. *)
+ of the IA32 assembly code. *)
open Asm
open Asmexpandaux