Changeset 3045


Ignore:
Timestamp:
Mar 29, 2013, 10:15:54 PM (4 years ago)
Author:
tranquil
Message:

fixed what made test3 fail. However it involves a different notion of
what actually the ASM preamble is (table of addresses rather than
table of sizes). It will need to be discussed

Files:
3 edited

Legend:

Unmodified
Added
Removed
  • driver/tests/PROBLEMI

    r3043 r3045  
    111. ok
    222. assembly ko, inizializzazione?
    3 3. rotto di nuovo dopo commit Paolo
     33. ok
    444. ok
    555. ok
  • src/ASM/Status.ma

    r3024 r3045  
    10301030definition construct_datalabels: list (Identifier × Word) → ? ≝
    10311031  λthe_preamble.
    1032     \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
    1033     λt. λpreamble.
     1032    foldl ((identifier_map ASMTag Word)) ? (
     1033    λpreamble,t. add … preamble (\fst t) (\snd t)) (empty_map ??) the_preamble.
     1034(*
    10341035      let 〈datalabels, addr〉 ≝ t in
    10351036      let 〈name, size〉 ≝ preamble in
     
    10371038        〈add ? ? datalabels name addr, sum〉)
    10381039          〈empty_map …, zero 16〉 (the_preamble)).
     1040*)
  • src/LIN/LINToASM.ma

    r3040 r3045  
    430430  ! Id ← Identifier_of_ident … id ;
    431431  let mut ≝ mk_init_mutable (virtual_dptr mut) (actual_dptr mut) (built_code mut)
     432  (* Paolo: this is what you intended Claudio:
     433      (〈Id, bitvector_of_nat … (size_init_data_list … data)〉 :: built_preamble mut) in
     434  however, if we do initialization here, we need to actually fix the addresses!
     435  for now, I'll change lookup_datalabels... *)
    432436      (〈Id, bitvector_of_Z … (virtual_dptr mut)〉 :: built_preamble mut) in
    433437  foldr … do_store_init_data (return mut) data.
Note: See TracChangeset for help on using the changeset viewer.