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/lINToASM.mli

    r2773 r2951  
    8282
    8383open ASM
     84
     85open Extra_bool
     86
     87open Coqlib
     88
     89open Values
     90
     91open FrontEndVal
     92
     93open GenMem
     94
     95open FrontEndMem
     96
     97open Globalenvs
    8498
    8599open Sets
     
    254268  AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __
    255269
     270val store_bytes :
     271  BitVector.byte List.list -> ASM.labelled_instruction List.list
     272
     273val do_store_init_data :
     274  AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data ->
     275  ASM.labelled_instruction List.list
     276
     277val do_store_init_data_list :
     278  AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data List.list ->
     279  ASM.labelled_instruction List.list
     280
     281val translate_initialization :
     282  LIN.lin_program -> ASM.labelled_instruction List.list
     283  Monad.smax_def__o__monad
     284
    256285val get_symboltable :
    257286  AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
Note: See TracChangeset for help on using the changeset viewer.