diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
| commit | dcb523736e82d72b03fa8d055bf74472dba7345c (patch) | |
| tree | 71e797c92d45dca509527043d233c51b2ed8fc86 /common/AST.v | |
| parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
| parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
| download | compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.tar.gz compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.zip | |
Merge branch 'master' into merge_master_8.13.1
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/common/AST.v b/common/AST.v index 979db4b9..9fe32331 100644 --- a/common/AST.v +++ b/common/AST.v @@ -61,7 +61,7 @@ Definition typesize (ty: typ) : Z := end. Lemma typesize_pos: forall ty, typesize ty > 0. -Proof. destruct ty; simpl; omega. Qed. +Proof. destruct ty; simpl; lia. Qed. Lemma typesize_Tptr: typesize Tptr = if Archi.ptr64 then 8 else 4. Proof. unfold Tptr; destruct Archi.ptr64; auto. Qed. @@ -122,17 +122,17 @@ These signatures are used in particular to determine appropriate calling conventions for the function. *) Record calling_convention : Type := mkcallconv { - cc_vararg: bool; (**r variable-arity function *) - cc_unproto: bool; (**r old-style unprototyped function *) - cc_structret: bool (**r function returning a struct *) + cc_vararg: option Z; (**r variable-arity function (+ number of fixed args) *) + cc_unproto: bool; (**r old-style unprototyped function *) + cc_structret: bool (**r function returning a struct *) }. Definition cc_default := - {| cc_vararg := false; cc_unproto := false; cc_structret := false |}. + {| cc_vararg := None; cc_unproto := false; cc_structret := false |}. Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}. Proof. - decide equality; apply bool_dec. + decide equality; try (apply bool_dec). decide equality; apply Z.eq_dec. Defined. Global Opaque calling_convention_eq. @@ -275,13 +275,13 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := Lemma init_data_size_pos: forall i, init_data_size i >= 0. Proof. - destruct i; simpl; try xomega. destruct Archi.ptr64; omega. + destruct i; simpl; try extlia. destruct Archi.ptr64; lia. Qed. Lemma init_data_list_size_pos: forall il, init_data_list_size il >= 0. Proof. - induction il; simpl. omega. generalize (init_data_size_pos a); omega. + induction il; simpl. lia. generalize (init_data_size_pos a); lia. Qed. (** Information attached to global variables. *) |