X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fread_write%2FFreescale_load_write.ma;h=38c9053e3e949600b7d02322040aa5e39e8bd7ff;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=be04ff2f1d761bd4b5e5cd0a1984c57ac70aec89;hpb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma index be04ff2f1..38c9053e3 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma @@ -20,8 +20,8 @@ (* *) (* ********************************************************************** *) -include "emulator/read_write/load_write_base.ma". include "emulator/status/status_getter.ma". +include "emulator/read_write/load_write_base.ma". (* lettura da [curpc]: IMM1 *) ndefinition mode_IMM1_load ≝ @@ -417,7 +417,7 @@ ndefinition Freescale_multi_mode_load_auxw ≝ (* **************************************** *) ndefinition Freescale_multi_mode_write_auxb ≝ -λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwriteb:byte8.match i with +λm,t.λs:any_status m t.λcur_pc:word16.λflag:aux_mod_type.λi:Freescale_instr_mode.λwriteb:byte8.match i with (* NO: non ci sono indicazioni *) [ MODE_INH ⇒ None ? (* scrive A *)