Changeset 3045 for src/LIN


Ignore:
Timestamp:
Mar 29, 2013, 10:15:54 PM (8 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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.