Changeset 482


Ignore:
Timestamp:
Jan 28, 2011, 2:41:46 PM (6 years ago)
Author:
campbell
Message:

Note the purpose of the region in a pointer value.

File:
1 edited

Legend:

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

    r480 r482  
    3030- a machine integer;
    3131- a floating-point number;
    32 - a pointer: a pair of a memory address and an integer offset with respect
    33   to this address;
     32- a pointer: a triple giving the representation of the pointer (in terms of the
     33             memory regions such a pointer could address), a memory address and
     34             an integer offset with respect to this address;
    3435- the [Vundef] value denoting an arbitrary bit pattern, such as the
    3536  value of an uninitialized variable.
    3637*)
    3738
    38 (* TODO: should comparison and subtraction of pointers of different sorts
    39          be supported? *)
    40 
    4139ninductive val: Type[0] ≝
    4240  | Vundef: val
    43   | Vint: int -> val
    44   | Vfloat: float -> val
    45   | Vptr: region → block -> int -> val.
     41  | Vint: int val
     42  | Vfloat: float val
     43  | Vptr: region → block → int → val.
    4644
    4745ndefinition Vzero: val ≝ Vint zero.
Note: See TracChangeset for help on using the changeset viewer.