Ignore:
Timestamp:
Oct 11, 2011, 12:45:16 PM (8 years ago)
Author:
sacerdot
Message:

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1329 r1352  
    285285        ! st ← pair_reg_move … st dst_src ;
    286286          ret ? 〈E0, next … l st〉
    287       (*CSC: XXX bug here dest unused *)
    288287      | CALL_ID id argsno dest ⇒
    289288        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    292291          [ Internal fn ⇒
    293292            ! st ← save_ra … st l;
    294               let st ≝ save_frame … st in
     293              let st ≝ save_frame … dest st in
    295294              let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
     295+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
     296+ ALLOCARE LO STACK FRAME
    296297              let l' ≝ joint_if_entry … fn in
    297298             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
     
    307308          ]]
    308309    | RETURN ⇒
     310+ CHIAMARE UNA FUNZIONE PER ANDARE A SOSTITUIRE IL VALORE TROVATO NEL REGISTRO
     311DI RITORNO DELLA FUNZIONE AL POSTO GIUSTO
     312+ DEALLOCARE LO STACK FRAME
    309313      ! st ← pop_frame … st;
    310314      ! 〈st,pch〉 ← pop … st;
Note: See TracChangeset for help on using the changeset viewer.