Changeset 2951 for extracted/costInj.mli


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

    r2773 r2951  
    11open Preamble
    2 
    3 open Listb_extra
    4 
    5 open Executions
    6 
    7 open CostMisc
    8 
    9 open Deqsets_extra
    10 
    11 open CostSpec
    12 
    13 open Sets
    14 
    15 open Listb
    16 
    17 open StructuredTraces
    182
    193open BitVectorTrie
     
    259open Registers
    2610
    27 open FrontEndOps
    28 
    29 open RTLabs_syntax
    30 
    31 open SmallstepExec
    32 
    33 open CostLabel
    34 
    35 open Events
    36 
    37 open IOMonad
    38 
    39 open IO
    40 
    41 open Extra_bool
    42 
    43 open Coqlib
    44 
    45 open Values
    46 
    4711open FrontEndVal
    4812
     
    5014
    5115open ByteValues
     16
     17open GenMem
     18
     19open FrontEndMem
    5220
    5321open Division
     
    5927open Pointers
    6028
    61 open GenMem
     29open Coqlib
    6230
    63 open FrontEndMem
     31open Values
     32
     33open FrontEndOps
     34
     35open CostLabel
    6436
    6537open Proper
     
    6941open Deqsets
    7042
     43open ErrorMessages
     44
     45open PreIdentifiers
     46
     47open Errors
     48
    7149open Extralib
    7250
    7351open Lists
     52
     53open Positive
    7454
    7555open Identifiers
     
    8969open BitVector
    9070
    91 open Extranat
     71open Jmeq
    9272
    93 open Integers
     73open Russell
    9474
    95 open AST
    96 
    97 open Globalenvs
    98 
    99 open ErrorMessages
    100 
    101 open Option
     75open List
    10276
    10377open Setoids
     
    10579open Monad
    10680
    107 open Jmeq
     81open Option
    10882
    109 open Russell
    110 
    111 open Positive
    112 
    113 open PreIdentifiers
    114 
    115 open Errors
     83open Extranat
    11684
    11785open Bool
     
    12088
    12189open Nat
     90
     91open Integers
     92
     93open Types
     94
     95open AST
    12296
    12397open Hints_declaration
     
    129103open Logic
    130104
    131 open Types
     105open RTLabs_syntax
    132106
    133 open List
    134 
    135 open RTLabs_semantics
    136 
    137 open RTLabs_abstract
    138 
    139 open RTLabs_traces
     107open CostSpec
    140108
    141109val reverse_label_map :
Note: See TracChangeset for help on using the changeset viewer.