Changeset 3178 for src/Clight/Csyntax.ma
 Timestamp:
 Apr 25, 2013, 6:03:24 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csyntax.ma
r2645 r3178 346 346 347 347 (* * Natural alignment of a type, in bytes. *) 348 let rec alignof (t: type) : nat ≝ (*1*)349 (* these are old values for 32 bit machines *)348 let rec alignof (t: type) : nat ≝ 1. 349 (* these are old values for 32 bit machines 350 350 match t with 351 351 [ Tvoid ⇒ 1 … … 363 363 [ Fnil ⇒ 1 364 364  Fcons id t f' ⇒ max (alignof t) (alignof_fields f') 365 ]. 365 ].*) 366 366 367 367 (* … … 412 412 (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs f') 413 413 ]. 414 414 (* 415 415 lemma alignof_fields_pos: 416 416 ∀f. alignof_fields f > 0. 417 417 @fieldlist_ind //; 418 418 #i #t #fs' #IH @max_r @IH qed. 419 419 *) 420 420 lemma alignof_pos: 421 421 ∀t. alignof t > 0. 422 #t elim t; normalize; //; 422 #t elim t; normalize; //;(* 423 423 [ 1,2: #z cases z; /2/; 424 424  3,4: #i @alignof_fields_pos 425 ] qed.425 ]*) qed. 426 426 427 427 (* * Size of a type, in bytes. *) … … 450 450  Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld') 451 451 ]. 452 (* TODO: needs some Z_times results 452 453 453 lemma sizeof_pos: 454 454 ∀t. sizeof t > 0. 455 #t0 456 napply (type_ind2 (λt. sizeof t > 0) 457 (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0)); 458 [ 1,4,6,9: //; 459  #i cases i;#s //; 460  #f cases f;// 461  #t #n #H whd in ⊢ (?%?); 462 Proof. 463 intro t0. 464 apply (type_ind2 (fun t => sizeof t > 0) 465 (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 > sizeof_struct f pos >= 0)); 466 intros; simpl; auto; try omega. 467 destruct i; omega. 468 destruct f; omega. 469 apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega. 470 destruct H. 471 generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). 472 generalize (Zmax1 1 (sizeof_struct f 0)). omega. 473 generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). 474 generalize (Zmax1 1 (sizeof_union f)). omega. 475 split. omega. auto. 476 destruct H0. split; intros. 477 generalize (Zmax2 (sizeof t) (sizeof_union f)). omega. 478 apply H1. 479 generalize (align_le pos (alignof t) (alignof_pos t)). omega. 480 Qed. 481 455 #t elim t // 456 [ * // 457  #t' * [ /2/  #n #H change with (0 < ?) whd in ⊢ (??%); change with (0*0) in ⊢ (?%?); @lt_times // ] 458  #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1 459 >commutative_plus cases (sizeof_struct ??) [2:#x] whd in ⊢ (?(?%?)?); 460 // 461  #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1 462 >commutative_plus cases (sizeof_union ?) [2:#x] whd in ⊢ (?(?%?)?); 463 // 464 ] qed. 465 466 (* 482 467 Lemma sizeof_struct_incr: 483 468 forall fld pos, pos <= sizeof_struct fld pos.
Note: See TracChangeset
for help on using the changeset viewer.