aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Cutil.ml17
-rw-r--r--cparser/Machine.ml19
-rw-r--r--cparser/validator/Alphabet.v32
-rw-r--r--cparser/validator/Interpreter_complete.v8
4 files changed, 44 insertions, 32 deletions
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 586b4a92..9bc11141 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -179,7 +179,7 @@ let rec attributes_of_type env t =
| TUnion(s, a) ->
let ci = Env.find_union env s in add_attributes ci.ci_attr a
| TEnum(s, a) ->
- let ei = Env.find_enum env s in add_attributes ei.ei_attr a
+ let ei = Env.find_enum env s in add_attributes ei.ei_attr a
(* Changing the attributes of a type (at top-level) *)
(* Same hack as above for array types. *)
@@ -937,10 +937,23 @@ let rec is_lvalue e =
whose type is not const, neither an array type, nor a function type,
nor an incomplete type. *)
+let rec is_const_type env ty =
+ List.mem AConst (attributes_of_type env ty) ||
+ begin match unroll env ty with
+ | TStruct(s, a) ->
+ let ci = Env.find_struct env s in
+ List.exists (fun m -> is_const_type env m.fld_typ) ci.ci_members
+ | TUnion(s, a) ->
+ let ci = Env.find_union env s in
+ List.exists (fun m -> is_const_type env m.fld_typ) ci.ci_members
+ | _ ->
+ false
+ end
+
let is_modifiable_lvalue env e =
is_lvalue e
- && not (List.mem AConst (attributes_of_type env e.etyp))
&& not (incomplete_type env e.etyp)
+ && not (is_const_type env e.etyp)
&& begin match unroll env e.etyp with
| TFun _ | TArray _ -> false
| _ -> true
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 4df80125..c95779b9 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -57,7 +57,7 @@ let ilp32ll64 = {
sizeof_longlong = 8;
sizeof_float = 4;
sizeof_double = 8;
- sizeof_longdouble = 16;
+ sizeof_longdouble = 8;
sizeof_void = None;
sizeof_fun = None;
sizeof_wchar = 4;
@@ -71,7 +71,7 @@ let ilp32ll64 = {
alignof_longlong = 8;
alignof_float = 4;
alignof_double = 8;
- alignof_longdouble = 16;
+ alignof_longdouble = 8;
alignof_void = None;
alignof_fun = None;
bigendian = false;
@@ -89,7 +89,7 @@ let i32lpll64 = {
sizeof_longlong = 8;
sizeof_float = 4;
sizeof_double = 8;
- sizeof_longdouble = 16;
+ sizeof_longdouble = 8;
sizeof_void = None;
sizeof_fun = None;
sizeof_wchar = 4;
@@ -103,7 +103,7 @@ let i32lpll64 = {
alignof_longlong = 8;
alignof_float = 4;
alignof_double = 8;
- alignof_longdouble = 16;
+ alignof_longdouble = 8;
alignof_void = None;
alignof_fun = None;
bigendian = false;
@@ -121,7 +121,7 @@ let il32pll64 = {
sizeof_longlong = 8;
sizeof_float = 4;
sizeof_double = 8;
- sizeof_longdouble = 16;
+ sizeof_longdouble = 8;
sizeof_void = None;
sizeof_fun = None;
sizeof_wchar = 4;
@@ -135,7 +135,7 @@ let il32pll64 = {
alignof_longlong = 8;
alignof_float = 4;
alignof_double = 8;
- alignof_longdouble = 16;
+ alignof_longdouble = 8;
alignof_void = None;
alignof_fun = None;
bigendian = false;
@@ -149,11 +149,11 @@ let x86_32 =
{ ilp32ll64 with name = "x86_32";
char_signed = true;
alignof_longlong = 4; alignof_double = 4;
- sizeof_longdouble = 12; alignof_longdouble = 4;
+ alignof_longdouble = 4;
supports_unaligned_accesses = true }
let x86_32_macosx =
- { x86_32 with sizeof_longdouble = 16; alignof_longdouble = 16 }
+ x86_32
let x86_64 =
{ i32lpll64 with name = "x86_64"; char_signed = true }
@@ -194,8 +194,7 @@ let gcc_extensions c =
(* Normalize configuration for use with the CompCert reference interpreter *)
let compcert_interpreter c =
- { c with sizeof_longdouble = 8; alignof_longdouble = 8;
- supports_unaligned_accesses = false }
+ { c with supports_unaligned_accesses = false }
(* Undefined configuration *)
diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v
index ca71bf59..a13f69b0 100644
--- a/cparser/validator/Alphabet.v
+++ b/cparser/validator/Alphabet.v
@@ -61,13 +61,13 @@ Qed.
(** nat is comparable. **)
Program Instance natComparable : Comparable nat :=
- { compare := nat_compare }.
+ { compare := Nat.compare }.
Next Obligation.
symmetry.
-destruct (nat_compare x y) as [] eqn:?.
-rewrite nat_compare_eq_iff in Heqc.
+destruct (Nat.compare x y) as [] eqn:?.
+rewrite Nat.compare_eq_iff in Heqc.
destruct Heqc.
-rewrite nat_compare_eq_iff.
+rewrite Nat.compare_eq_iff.
trivial.
rewrite <- nat_compare_lt in *.
rewrite <- nat_compare_gt in *.
@@ -78,9 +78,9 @@ trivial.
Qed.
Next Obligation.
destruct c.
-rewrite nat_compare_eq_iff in *; destruct H; assumption.
+rewrite Nat.compare_eq_iff in *; destruct H; assumption.
rewrite <- nat_compare_lt in *.
-apply (lt_trans _ _ _ H H0).
+apply (Nat.lt_trans _ _ _ H H0).
rewrite <- nat_compare_gt in *.
apply (gt_trans _ _ _ H H0).
Qed.
@@ -149,7 +149,7 @@ destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..];
right; intro; destruct H; rewrite compare_refl in Heqc; discriminate.
Defined.
-Instance NComparableUsualEq : ComparableUsualEq natComparable := nat_compare_eq.
+Instance NComparableUsualEq : ComparableUsualEq natComparable := Nat.compare_eq.
(** A pair of ComparableUsualEq is ComparableUsualEq **)
Instance PairComparableUsualEq
@@ -223,33 +223,33 @@ inversion Heqp. subst. clear Heqp.
rewrite phi_incr in H.
pose proof (phi_bounded i0).
pose proof (phi_bounded (inj x)).
-destruct (Z_lt_le_dec (Zsucc (phi i0)) (2 ^ Z_of_nat size)%Z).
+destruct (Z_lt_le_dec (Z.succ (phi i0)) (2 ^ Z.of_nat size)%Z).
rewrite Zmod_small in H by omega.
apply Zlt_succ_le, Zle_lt_or_eq in H.
destruct H; simpl; auto. left.
rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity.
-replace (Zsucc (phi i0)) with (2 ^ Z_of_nat size)%Z in H by omega.
+replace (Z.succ (phi i0)) with (2 ^ Z.of_nat size)%Z in H by omega.
rewrite Z_mod_same_full in H.
exfalso; omega.
rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal.
pose proof (phi_bounded inj_bound); pose proof (phi_bounded i).
-rewrite <- Zabs_eq with (phi i), <- Zabs_eq with (phi inj_bound) by omega.
+rewrite <- Z.abs_eq with (phi i), <- Z.abs_eq with (phi inj_bound) by omega.
clear H H0 H1.
-do 2 rewrite <- inj_Zabs_nat.
+do 2 rewrite <- Zabs2Nat.id_abs.
f_equal.
revert l i Heqp.
-assert (Zabs_nat (phi inj_bound) < Zabs_nat (2^31)).
+assert (Z.abs_nat (phi inj_bound) < Z.abs_nat (2^31)).
apply Zabs_nat_lt, phi_bounded.
-induction (Zabs_nat (phi inj_bound)); intros.
+induction (Z.abs_nat (phi inj_bound)); intros.
inversion Heqp; reflexivity.
inversion Heqp; clear H1 H2 Heqp.
match goal with |- _ (_ (_ (snd ?p))) = _ => destruct p end.
pose proof (phi_bounded i0).
-erewrite <- IHn, <- Zabs_nat_Zsucc in H |- *; eauto; try omega.
+erewrite <- IHn, <- Zabs2Nat.inj_succ in H |- *; eauto; try omega.
rewrite phi_incr, Zmod_small; intuition; try omega.
apply inj_lt in H.
-pose proof Zle_le_succ.
-do 2 rewrite inj_Zabs_nat, Zabs_eq in H; now eauto.
+pose proof Z.le_le_succ_r.
+do 2 rewrite Zabs2Nat.id_abs, Z.abs_eq in H; now eauto.
Qed.
(** Previous class instances for [option A] **)
diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v
index ff88571b..f76731d5 100644
--- a/cparser/validator/Interpreter_complete.v
+++ b/cparser/validator/Interpreter_complete.v
@@ -304,7 +304,7 @@ reflexivity.
destruct p.
reflexivity.
simpl; rewrite build_pt_dot_cost.
-simpl; rewrite <- plus_n_Sm, plus_assoc; reflexivity.
+simpl; rewrite <- plus_n_Sm, Nat.add_assoc; reflexivity.
Qed.
Lemma build_pt_dot_buffer:
@@ -593,12 +593,12 @@ Lemma parse_fix_complete:
Proof.
fix 3.
destruct n_steps; intros; simpl.
-apply lt_0_Sn.
+apply Nat.lt_0_succ.
apply step_next_ptd in H.
pose proof (next_ptd_cost ptd).
destruct (step init stack0 (ptd_buffer ptd)) as [|[]]; simpl; intuition.
rewrite H3 in H0; rewrite H0.
-apply le_n_S, le_0_n.
+apply le_n_S, Nat.le_0_l.
destruct (next_ptd ptd); intuition; subst.
eapply parse_fix_complete with (n_steps:=n_steps) in H1.
rewrite H0.
@@ -648,7 +648,7 @@ generalize (start_nt init).
dependent destruction full_pt0.
intros.
rewrite build_pt_dot_cost; simpl.
-rewrite H, plus_0_r; reflexivity.
+rewrite H, Nat.add_0_r; reflexivity.
Qed.
Lemma init_ptd_buffer:
generated by cgit (git 2.34.1) at 2024-07-26 01:21:55 +0000