diff options
| -rw-r--r-- | src/Makefile | 13 | ||||
| -rw-r--r-- | src/_tags | 8 | ||||
| -rw-r--r-- | src/myocamlbuild.ml | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 6 |
4 files changed, 15 insertions, 15 deletions
diff --git a/src/Makefile b/src/Makefile index 34b58c6d..57ae0981 100644 --- a/src/Makefile +++ b/src/Makefile @@ -11,6 +11,9 @@ interpreter: ocamlbuild lem_interp/extract.cmxa ocamlbuild lem_interp/extract.cma +elf: + ocamlbuild -use-ocamlfind -pkgs batteries,uint src_elf/main_elf.native + test: sail interpreter ocamlbuild test/run_tests.native ./run_tests.native @@ -23,16 +26,6 @@ install_elf: cp -p ../../system-v-abi/src/*.ml elf_model/ cp -p -r ../../system-v-abi/src/libraries elf_model/libraries -elf: - $(MAKE) -C elf_model ocaml_native - mkdir -p _build/elf_model - cp -p elf_model/*.cmi _build/elf_model/ - cp -p elf_model/*.cmx _build/elf_model/ - cp -p elf_model/*.o _build/elf_model/ - cd _build/elf_model ;\ - ocamlfind ocamlopt -package batteries -package uint -package bitstring -I $(LEMLIBOCAML) -a -o elf_extract.cmxa missing_pervasives.cmx \ -show.cmx endianness.cmx error.cmx ml_bindings.cmx default_printing.cmx bitstring_local.cmx elf_types.cmx elf_header.cmx elf_file1.cmx elf_program_header_table.cmx elf_executable_file2.cmx string_table.cmx elf_section_header_table.cmx elf_interpreted_segment.cmx elf_symbol_table.cmx elf_executable_file3.cmx elf_linking_file2.cmx elf_linking_file3.cmx elf_relocation.cmx sail_interface.cmx - power: sail interpreter elf mkdir -p _build/test @@ -3,9 +3,15 @@ true: -traverse, debug <lem_interp> or <test>: include <sail.{byte,native}>: use_pprint, use_nums <pprint> or <pprint/src>: include +<{src_elf,src_elf/abis,src_elf/abis/power64,src_elf/abis/amd64,src_elf/abis/aarch64,src_elf/adaptors}> : include + # see http://caml.inria.fr/mantis/view.php?id=4943 <lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, use_lem -<test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str +<test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str, use_batteries +<src_elf/*.ml> : use_batteries, use_lem, use_nums +<src_elf/abis/*.ml> : use_batteries, use_lem, use_nums +<src_elf/abis/*/*.ml> : use_batteries, use_lem, use_nums +<src_elf/adaptors/*.ml> : use_batteries, use_lem, use_nums, use_unix # disable partial match and unused variable warnings <**/*.ml>: warn_y diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml index e38dbb4d..c0172700 100644 --- a/src/myocamlbuild.ml +++ b/src/myocamlbuild.ml @@ -37,7 +37,8 @@ dispatch begin function (* ocaml_lib "lem_interp/interp"; *) ocaml_lib ~extern:true ~dir:lem_libdir ~tag_name:"use_lem" lem_lib; ocaml_lib ~extern:false ~dir:"pprint/src" ~tag_name:"use_pprint" "pprint/src/PPrintLib"; - + ocaml_lib ~extern:true ~dir:"src_elf_libraries/batteries/_build/src" ~tag_name:"use_batteries" "src_elf_libraries/batteries"; + rule "lem -> ml" ~prod: "%.ml" ~dep: "%.lem" diff --git a/src/type_check.ml b/src/type_check.ml index 6b738c97..37d9ba19 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1538,7 +1538,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) | Tapp("register",[TA_typ t]) | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t,true,false | Tapp("reg",[TA_typ t]) -> t,false,false | _ -> item_t,false,true in - let ef = if add_reg_write then add_effect (BE_aux(BE_wreg,l)) efl else efl in + let ef,tag = if add_reg_write then (add_effect (BE_aux(BE_wreg,l)) efl,External None) else (efl,tag) in if is_top && reg_still_required && reg_required then typ_error l "Assignment expected a register or non-parameter non-letbound identifier to mutate" else @@ -1739,7 +1739,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) = let (bf_t, _, _) = range_to_type_inc bf in ((id_to_string id),bf_t)) ranges in - let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e,pure_e,nob)) in + let tannot = into_register d_env (Base(([],ty),External None,[],pure_e,pure_e,nob)) in (TD_aux(td,(l,tannot)), Env({d_env with rec_env = ((id',Register,tannot,franges)::d_env.rec_env); abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env))) @@ -1782,7 +1782,7 @@ let check_type_def envs (TD_aux(td,(l,annot))) = (fun (bf,id) -> let (bf_t, _, _) = range_to_type_dec bf in (id_to_string id, bf_t)) ranges in - let tannot = into_register d_env (Base(([],ty),Emp_global,[],pure_e,pure_e,nob)) in + let tannot = into_register d_env (Base(([],ty),External None,[],pure_e,pure_e,nob)) in (TD_aux(td,(l,tannot)), Env({d_env with rec_env = (id',Register,tannot,franges)::d_env.rec_env; abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env))) |