source: src/joint/ @ 1321

Last change on this file since 1321 was 1213, checked in by sacerdot, 10 years ago

1) New values (joint/ and memory model for the back-ends

(joint/ where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/ and common/ shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in
(cut&paste code).

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.