Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (9 years ago)
Author:
campbell
Message:

Initial work on Clight semantics with 8051 memory spaces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Globalenvs.ma

    r24 r124  
    330330  (λF,V,p. empty)  (* init_mem *)
    331331  (λF,ge. functions ? ge) (* find_funct_ptr *)
    332   (λF,ge,v. match v with [ Vptr b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
     332  (λF,ge,v. match v with [ Vptr _ b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    333333  (λF,ge. symbols ? ge) (* find_symbol *)
    334334  ?
     
    359359    ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
    360360    ##| ##2,3: #x; nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
    361     ##| #b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero);
     361    ##| #pcl b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero);
    362362        nwhd in ⊢ (??%? → ??%?);
    363363        ##[ nelim p; #fns main vars; nelim fns;
     
    420420  ##[ nnormalize; #H; ndestruct;
    421421  ##| ##2,3: #x; nnormalize; #H; ndestruct;
    422   ##| #b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero);
     422  ##| #pcl b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero);
    423423    ##[ nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
    424424      nelim fns;
Note: See TracChangeset for help on using the changeset viewer.