Changeset 740 for Deliverables/D2.2/8051/src/driver.ml

Timestamp:

Apr 4, 2011, 5:18:15 PM (10 years ago)

Author:

ayache

Message:

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File:

• Deliverables/D2.2/8051/src/driver.ml (modified) (2 diffs)

Deliverables/D2.2/8051/src/driver.ml

@@ -2 +2 @@
 (** This module defines the target architecture and instanciates the memory
     functor for each intermediate language. *)
-
-(* Clight as an interpretation independant from the target
-   architecture. Integers and addresses are 4 bytes long. *)
 
 module DataSize32 =
@@ -17 +14 @@
 module TargetArch = I8051
 
-module ClightMemory = Memory.Make (DataSize32)
-module CminorMemory = Memory.Make (TargetArch)
-module RTLabsMemory = Memory.Make (TargetArch)
-module RTLMemory    = Memory.Make (TargetArch)
-module ERTLMemory   = Memory.Make (TargetArch)
-module LTLMemory    = Memory.Make (TargetArch)
-module LINMemory    = Memory.Make (TargetArch)
+module Memory32     = Memory.Make (DataSize32)
+module MemoryTarget = Memory.Make (TargetArch)
+
+module ClightMemory = Memory32
+module CminorMemory = Memory32
+module RTLabsMemory = Memory32
+module RTLMemory    = MemoryTarget
+module ERTLMemory   = MemoryTarget
+module LTLMemory    = MemoryTarget
+module LINMemory    = MemoryTarget