diff options
Diffstat (limited to 'backend/Locations.v')
| -rw-r--r-- | backend/Locations.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/backend/Locations.v b/backend/Locations.v index ea614585..6ca84ea7 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -84,6 +84,28 @@ Proof. destruct ty; compute; auto. Qed. +Definition typealign (ty: typ) : Z := + match ty with + | Tint => 1 + | Tlong => 2 + | Tfloat => 1 + | Tsingle => 1 + | Tany32 => 1 + | Tany64 => 1 + end. + +Lemma typealign_pos: + forall (ty: typ), typealign ty > 0. +Proof. + destruct ty; compute; auto. +Qed. + +Lemma typealign_typesize: + forall (ty: typ), (typealign ty | typesize ty). +Proof. + intros. exists (typesize ty / typealign ty); destruct ty; reflexivity. +Qed. + (** ** Locations *) (** Locations are just the disjoint union of machine registers and |