Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 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/joint_LTL_LIN_semantics.ml

    r2867 r2951  
    11open Preamble
    22
     3open Extra_bool
     4
     5open Coqlib
     6
     7open Values
     8
     9open FrontEndVal
     10
     11open GenMem
     12
     13open FrontEndMem
     14
     15open Globalenvs
     16
    317open String
    418
     
    132146
    133147open IO
    134 
    135 open Extra_bool
    136 
    137 open Coqlib
    138 
    139 open Values
    140 
    141 open FrontEndVal
    142 
    143 open GenMem
    144 
    145 open FrontEndMem
    146 
    147 open Globalenvs
    148148
    149149open Joint_semantics
Note: See TracChangeset for help on using the changeset viewer.