aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-05-18 09:58:14 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-05-18 09:58:14 +0200
commit4663ad4b31e351e29a4d8d034ad4a961a48263f1 (patch)
treed21554c60ed607bf8fdd1476431f9707bf882604 /cparser
parent10def48b639b8e83ae6cc8bf9c14da8c12e98370 (diff)
parent5d017f110f6c23c29a182465ab7832a944c0ba26 (diff)
downloadcompcert-4663ad4b31e351e29a4d8d034ad4a961a48263f1.tar.gz
compcert-4663ad4b31e351e29a4d8d034ad4a961a48263f1.zip
Merge branch 'master' into json_export
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Elab.ml22
-rw-r--r--cparser/ExtendedAsm.ml7
2 files changed, 19 insertions, 10 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 10af10a1..fe74a786 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1801,12 +1801,20 @@ let enter_or_refine_ident local loc env s sto ty =
| None ->
warning loc "redefinition of '%s' with incompatible type" s; ty in
let new_sto =
- if old_sto = Storage_extern then sto else
- if sto = Storage_extern then old_sto else
- if old_sto = sto then sto else begin
- warning loc "redefinition of '%s' with incompatible storage class" s;
- sto
- end in
+ (* The only case not allowed is removing static *)
+ match old_sto,sto with
+ | Storage_static,Storage_static
+ | Storage_extern,Storage_extern
+ | Storage_register,Storage_register
+ | Storage_default,Storage_default -> sto
+ | _,Storage_static ->
+ error loc "static redefinition of '%s' after non-static definition" s; sto
+ | Storage_static,_ -> Storage_static (* Static stays static *)
+ | Storage_extern,_ -> sto
+ | _,Storage_extern -> old_sto
+ | _,Storage_register
+ | Storage_register,_ -> Storage_register
+ in
(id, new_sto, Env.add_ident env id new_sto new_ty)
| Some(id, II_enum v) when Env.in_current_scope env id ->
error loc "illegal redefinition of enumerator '%s'" s;
@@ -1854,7 +1862,7 @@ let enter_decdefs local loc env sto dl =
let elab_fundef env spec name body loc =
let (s, sto, inline, ty, env1) = elab_name env spec name in
if sto = Storage_register then
- error loc "a function definition cannot have 'register' storage class";
+ fatal_error loc "a function definition cannot have 'register' storage class";
(* Fix up the type. We can have params = None but only for an
old-style parameterless function "int f() {...}" *)
let ty =
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 94d23102..fbf8d569 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -161,9 +161,10 @@ let transf_outputs loc env = function
let check_clobbers loc clob =
List.iter
(fun c ->
- if Machregsaux.register_by_name c <> None
- || List.mem c Machregsaux.scratch_register_names
- || c = "memory" || c = "cc"
+ let c' = String.uppercase c in
+ if Machregsaux.register_by_name c' <> None
+ || List.mem c' Machregsaux.scratch_register_names
+ || c' = "MEMORY" || c' = "CC"
then ()
else error "%aError: unrecognized asm register clobber '%s'"
formatloc loc c)