Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (8 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLToERTL.ml

    r2882 r2951  
    7272
    7373open RegisterSet
     74
     75open Extra_bool
     76
     77open Coqlib
     78
     79open Values
     80
     81open FrontEndVal
     82
     83open GenMem
     84
     85open FrontEndMem
     86
     87open Globalenvs
    7488
    7589open String
Note: See TracChangeset for help on using the changeset viewer.