Ignore:
Timestamp:
Feb 2, 2011, 12:41:05 PM (10 years ago)
Author:
campbell
Message:

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/AST.ma

    r483 r485  
    147147  | Init_space: Z → init_data
    148148  | Init_null: region → init_data
    149   | Init_addrof: ident → int → init_data   (*r address of symbol + offset *)
    150   | Init_pointer: list init_data → init_data.
     149  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
    151150
    152151(* * Whole programs consist of:
Note: See TracChangeset for help on using the changeset viewer.