Ignore:
Timestamp:
Mar 26, 2013, 6:32:38 PM (7 years ago)
Author:
sacerdot
Message:

Bug fixed: the pre-main for the final code is now

COST k1
initialization code
CALL main

l: COST k2

Jmp l

with l the label of the final state. In this way the static analysis on the
object code does not diverge.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/lINToASM.mli

    r2951 r2963  
    134134                      label_map : ASM.identifier Identifiers.identifier_map
    135135                                  Identifiers.identifier_map;
    136                       address_map : BitVector.word Identifiers.identifier_map }
     136                      address_map : BitVector.word Identifiers.identifier_map;
     137                      fresh_cost_label : Positive.pos }
    137138
    138139val aSM_universe_rect_Type4 :
     
    140141  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    141142  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    142   __ -> 'a1) -> aSM_universe -> 'a1
     143  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    143144
    144145val aSM_universe_rect_Type5 :
     
    146147  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    147148  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    148   __ -> 'a1) -> aSM_universe -> 'a1
     149  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    149150
    150151val aSM_universe_rect_Type3 :
     
    152153  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    153154  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    154   __ -> 'a1) -> aSM_universe -> 'a1
     155  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    155156
    156157val aSM_universe_rect_Type2 :
     
    158159  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    159160  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    160   __ -> 'a1) -> aSM_universe -> 'a1
     161  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    161162
    162163val aSM_universe_rect_Type1 :
     
    164165  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    165166  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    166   __ -> 'a1) -> aSM_universe -> 'a1
     167  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    167168
    168169val aSM_universe_rect_Type0 :
     
    170171  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    171172  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    172   __ -> 'a1) -> aSM_universe -> 'a1
     173  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
    173174
    174175val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe
     
    188189  Identifiers.identifier_map
    189190
     191val fresh_cost_label : AST.ident List.list -> aSM_universe -> Positive.pos
     192
    190193val aSM_universe_inv_rect_Type4 :
    191194  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    192195  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    193196  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    194   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     197  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    195198
    196199val aSM_universe_inv_rect_Type3 :
     
    198201  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    199202  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    200   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     203  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    201204
    202205val aSM_universe_inv_rect_Type2 :
     
    204207  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    205208  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    206   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     209  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    207210
    208211val aSM_universe_inv_rect_Type1 :
     
    210213  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    211214  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    212   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     215  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    213216
    214217val aSM_universe_inv_rect_Type0 :
     
    216219  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    217220  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    218   Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     221  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
    219222
    220223val aSM_universe_jmdiscr :
    221224  AST.ident List.list -> aSM_universe -> aSM_universe -> __
     225
     226val report_cost :
     227  AST.ident List.list -> CostLabel.costlabel -> Types.unit0
     228  Monad.smax_def__o__monad
    222229
    223230val new_ASM_universe : Joint.joint_program -> aSM_universe
Note: See TracChangeset for help on using the changeset viewer.