Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2145 r2176  
    103103  whd in ⊢ (?(??%?)?);
    104104  cases ty' in EX1rem ⊢ %;
    105   [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r)
    106        #pc normalize #E destruct /2/
     105  [ 4: #ty' normalize #E destruct /2/
    107106  | *: normalize #A try #B try #C try #D destruct
    108107  ]
     
    672671        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
    673672        | // ] | /3/ ]
    674       | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
     673      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    675674      ]
    676675    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
     
    720719        %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
    721720        @refl | // ] | /4/ ] | skip ]
    722       | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
     721      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    723722      ]
    724723    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
Note: See TracChangeset for help on using the changeset viewer.