Ignore:
Timestamp:
Jan 4, 2013, 2:59:37 PM (7 years ago)
Author:
campbell
Message:

Fix Clight semantics for ptr + char. (Compiler works anyway.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2565 r2569  
    14361436     | 3: #Heq destruct (Heq)
    14371437          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
    1438           %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
     1438          @(ex_intro … (conj … (refl …) ?))
    14391439          @vptr_eq whd in match (pointer_translation ??);
    14401440          cases (E b1') in Hembed;
     
    14421442          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
    14431443               whd in match (shift_pointer_n ????);
    1444                cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
    1445                     (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) i))
     1444               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) tsg i) offset =
     1445                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) tsg i))
    14461446               [ 1: whd in match (offset_plus ??);
    14471447                    whd in match (shift_offset_n ????) in ⊢ (??%%);
     
    14771477     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
    14781478     #Heq destruct (Heq)
    1479      %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
     1479     @(ex_intro … (conj … (refl …) ?))
    14801480     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    14811481     elim p1 in Hembed; #b1 #o1 normalize nodelta
     
    15721572     [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ]
    15731573     #Heq destruct (Heq)
    1574      [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
     1574     [ 1: @(ex_intro … (conj … (refl …) ?))
    15751575          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    15761576          elim p1 in Hembed; #b1 #o1 normalize nodelta
     
    15791579          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
    15801580               whd in match (offset_plus ??) in ⊢ (??%%);
    1581                whd in match (neg_shift_pointer_n ????) in ⊢ (??%%);
    1582                whd in match (neg_shift_offset_n ????) in ⊢ (??%%);
     1581               whd in match (neg_shift_pointer_n ?????) in ⊢ (??%%);
     1582               whd in match (neg_shift_offset_n ?????) in ⊢ (??%%);
    15831583               whd in match (subtraction) in ⊢ (??%%); normalize nodelta
    15841584               generalize in match (short_multiplication ???); #mult
Note: See TracChangeset for help on using the changeset viewer.