source: Deliverables/D3.3/id-lookup-branch/joint/ @ 1939

Last change on this file since 1939 was 1311, checked in by campbell, 9 years ago

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

File size: 810 bytes
1(* Memory model used in the dynamic semantics of the back-end intermediate
2   languages. Inspired by common/, adapted from Compcert *)
4(* * This file develops the memory model that is used in the dynamic
5  semantics of all the languages used in the compiler.
6  It defines a type [mem] of memory states, the following 4 basic
7  operations over memory states, and their properties:
8- [load]: read a memory chunk at a given address;
9- [store]: store a memory chunk at a given address;
10- [alloc]: allocate a fresh memory block;
11- [free]: invalidate a memory block.
14include "joint/".
15include "common/".
17definition bemem ≝ mem (mk_contentT beval BVundef).
19axiom beloadv: ∀m:bemem. ∀ptr:pointer. option beval.
20axiom bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem.
Note: See TracBrowser for help on using the repository browser.