Opam Package sail.0.14

Package info

opam-namesail
opam-version0.14
synopsisSail is a language for describing the instruction semantics of processors
description Sail is a language for describing the instruction-set architecture (ISA) semantics of processors. Sail aims to provide a engineer-friendly, vendor-pseudocode-like language for describing instruction semantics. It is essentially a first-order imperative language, but with lightweight dependent typing for numeric types and bitvector lengths, which are automatically checked using Z3. It has been used for several papers, available from http://www.cl.cam.ac.uk/~pes20/sail/.
authors
  • Alasdair Armstrong
  • Thomas Bauereiss
  • Brian Campbell
  • Shaked Flur
  • Jonathan French
  • Kathy Gray
  • Robert Norton
  • Christopher Pulte
  • Peter Sewell
  • Mark Wassell
homepagehttp://www.cl.cam.ac.uk/~pes20/sail/
licenseBSD3
deps (15)
revdeps(0)
metas (1)
libraries (1)

Package modules

Package sources

sail

Package files

share/sail/src/util.ml
share/sail/src/sail_lib.ml
share/sail/src/lem_interp/sail2_impl_base.lem
share/sail/src/lem_interp/run_with_elf_cheri128.ml
share/sail/src/lem_interp/run_with_elf_cheri.ml
share/sail/src/lem_interp/run_with_elf.ml
share/sail/src/lem_interp/run_interp_model.ml
share/sail/src/lem_interp/run_interp.ml
share/sail/src/lem_interp/printing_functions.mli
share/sail/src/lem_interp/printing_functions.ml
share/sail/src/lem_interp/pretty_interp.ml
share/sail/src/lem_interp/interp_utilities.lem
share/sail/src/lem_interp/interp_lib.lem
share/sail/src/lem_interp/interp_interface.lem
share/sail/src/lem_interp/interp_inter_imp.lem
share/sail/src/lem_interp/interp.lem
share/sail/src/lem_interp/instruction_extractor.lem
share/sail/src/lem_interp/extract.mllib
share/sail/src/lem_interp
share/sail/src/gen_lib/sail2_values.lem
share/sail/src/gen_lib/sail2_string.lem
share/sail/src/gen_lib/sail2_state_monad.lem
share/sail/src/gen_lib/sail2_state_lifting.lem
share/sail/src/gen_lib/sail2_state.lem
share/sail/src/gen_lib/sail2_prompt_monad.lem
share/sail/src/gen_lib/sail2_prompt.lem
share/sail/src/gen_lib/sail2_operators_mwords.lem
share/sail/src/gen_lib/sail2_operators_bitlists.lem
share/sail/src/gen_lib/sail2_operators.lem
share/sail/src/gen_lib/sail2_instr_kinds.lem
share/sail/src/gen_lib/sail2_deep_shallow_convert.lem
share/sail/src/gen_lib
share/sail/src/elf_loader.ml
share/sail/src
share/sail/lib/vector_inc.sail
share/sail/lib/vector_dec.sail
share/sail/lib/trace.sail
share/sail/lib/string.sail
share/sail/lib/smt.sail
share/sail/lib/sail_state.h
share/sail/lib/sail_failure.h
share/sail/lib/sail_failure.c
share/sail/lib/sail_coverage.h
share/sail/lib/sail.tex
share/sail/lib/sail.h
share/sail/lib/sail.c
share/sail/lib/rts.h
share/sail/lib/rts.c
share/sail/lib/reverse_endianness.sail
share/sail/lib/regfp.sail
share/sail/lib/real.sail
share/sail/lib/prelude_wrappers.sail
share/sail/lib/prelude.sail
share/sail/lib/option.sail
share/sail/lib/nostd/test/test.c
share/sail/lib/nostd/test
share/sail/lib/nostd/stubs/sail_failure.c
share/sail/lib/nostd/stubs
share/sail/lib/nostd/sail_spinlock.h
share/sail/lib/nostd/sail_failure.h
share/sail/lib/nostd/sail_arena.h
share/sail/lib/nostd/sail_arena.c
share/sail/lib/nostd/sail_alloc.h
share/sail/lib/nostd/sail.h
share/sail/lib/nostd/sail.c
share/sail/lib/nostd
share/sail/lib/myocamlbuild_coverage.ml
share/sail/lib/mono_rewrites.sail
share/sail/lib/mapping.sail
share/sail/lib/main.ml
share/sail/lib/isabelle/manual/document/root.tex
share/sail/lib/isabelle/manual/document
share/sail/lib/isabelle/manual/ROOT
share/sail/lib/isabelle/manual/Manual.thy
share/sail/lib/isabelle/manual
share/sail/lib/isabelle/document/root.tex
share/sail/lib/isabelle/document
share/sail/lib/isabelle/Sail2_values_lemmas.thy
share/sail/lib/isabelle/Sail2_values.thy
share/sail/lib/isabelle/Sail2_string.thy
share/sail/lib/isabelle/Sail2_state_monad_lemmas.thy
share/sail/lib/isabelle/Sail2_state_monad.thy
share/sail/lib/isabelle/Sail2_state_lifting.thy
share/sail/lib/isabelle/Sail2_state_lemmas.thy
share/sail/lib/isabelle/Sail2_state.thy
share/sail/lib/isabelle/Sail2_prompt_monad_lemmas.thy
share/sail/lib/isabelle/Sail2_prompt_monad.thy
share/sail/lib/isabelle/Sail2_prompt.thy
share/sail/lib/isabelle/Sail2_operators_mwords_lemmas.thy
share/sail/lib/isabelle/Sail2_operators_mwords.thy
share/sail/lib/isabelle/Sail2_operators_bitlists.thy
share/sail/lib/isabelle/Sail2_operators.thy
share/sail/lib/isabelle/Sail2_instr_kinds.thy
share/sail/lib/isabelle/ROOT
share/sail/lib/isabelle/Makefile
share/sail/lib/isabelle/Hoare.thy
share/sail/lib/isabelle/.gitignore
share/sail/lib/isabelle
share/sail/lib/int128/sail.h
share/sail/lib/int128/sail.c
share/sail/lib/int128/rts.h
share/sail/lib/int128/rts.c
share/sail/lib/int128
share/sail/lib/instr_kinds.sail
share/sail/lib/hol/sail2_valuesScript.sml
share/sail/lib/hol/sail2_valuesAuxiliaryScript.sml
share/sail/lib/hol/sail2_stringScript.sml
share/sail/lib/hol/sail2_state_monadScript.sml
share/sail/lib/hol/sail2_stateScript.sml
share/sail/lib/hol/sail2_stateAuxiliaryScript.sml
share/sail/lib/hol/sail2_prompt_monadScript.sml
share/sail/lib/hol/sail2_prompt_monad.lem
share/sail/lib/hol/sail2_promptScript.sml
share/sail/lib/hol/sail2_prompt.lem
share/sail/lib/hol/sail2_operators_mwordsScript.sml
share/sail/lib/hol/sail2_operators_bitlistsScript.sml
share/sail/lib/hol/sail2_operatorsScript.sml
share/sail/lib/hol/sail2_instr_kindsScript.sml
share/sail/lib/hol/Makefile
share/sail/lib/hol/Holmakefile
share/sail/lib/hol/.gitignore
share/sail/lib/hol
share/sail/lib/generic_equality.sail
share/sail/lib/flow.sail
share/sail/lib/exception_basic.sail
share/sail/lib/elf.sail
share/sail/lib/elf.h
share/sail/lib/elf.c
share/sail/lib/coverage/src/lib.rs
share/sail/lib/coverage/src
share/sail/lib/coverage/Makefile
share/sail/lib/coverage/Cargo.toml
share/sail/lib/coverage
share/sail/lib/coq/_CoqProject
share/sail/lib/coq/Values_lemmas.v
share/sail/lib/coq/Values.v
share/sail/lib/coq/String.v
share/sail/lib/coq/State_monad_lemmas.v
share/sail/lib/coq/State_monad.v
share/sail/lib/coq/State_lifting.v
share/sail/lib/coq/State_lemmas.v
share/sail/lib/coq/State.v
share/sail/lib/coq/Real.v
share/sail/lib/coq/Prompt_monad.v
share/sail/lib/coq/Prompt.v
share/sail/lib/coq/Operators_mwords.v
share/sail/lib/coq/Operators_bitlists.v
share/sail/lib/coq/Operators.v
share/sail/lib/coq/Makefile
share/sail/lib/coq/Instr_kinds.v
share/sail/lib/coq/Impl_base.v
share/sail/lib/coq/Hoare.v
share/sail/lib/coq/Base.v
share/sail/lib/coq
share/sail/lib/arith.sail
share/sail/lib/_tags_coverage
share/sail/lib/_tags
share/sail/lib
share/sail
lib/sail/value2.cmx
lib/sail/value2.cmi
lib/sail/value.cmx
lib/sail/value.cmi
lib/sail/util.mli
lib/sail/util.cmx
lib/sail/util.cmi
lib/sail/type_error.cmx
lib/sail/type_error.cmi
lib/sail/type_check.mli
lib/sail/type_check.cmx
lib/sail/type_check.cmi
lib/sail/toFromInterp_lib_mword.cmx
lib/sail/toFromInterp_lib_mword.cmi
lib/sail/toFromInterp_lib_bitlist.cmx
lib/sail/toFromInterp_lib_bitlist.cmi
lib/sail/toFromInterp_backend.cmx
lib/sail/toFromInterp_backend.cmi
lib/sail/state.cmx
lib/sail/state.cmi
lib/sail/splice.cmx
lib/sail/splice.cmi
lib/sail/specialize.mli
lib/sail/specialize.cmx
lib/sail/specialize.cmi
lib/sail/spec_analysis.mli
lib/sail/spec_analysis.cmx
lib/sail/spec_analysis.cmi
lib/sail/smtlib.cmx
lib/sail/smtlib.cmi
lib/sail/slice.mli
lib/sail/slice.cmx
lib/sail/slice.cmi
lib/sail/scattered.cmx
lib/sail/scattered.cmi
lib/sail/sail_lib.cmx
lib/sail/sail_lib.cmi
lib/sail/sail2_values.cmx
lib/sail/sail2_values.cmi
lib/sail/sail2_prompt_monad.cmx
lib/sail/sail2_prompt_monad.cmi
lib/sail/sail2_prompt.cmx
lib/sail/sail2_prompt.cmi
lib/sail/sail2_operators_bitlists.cmx
lib/sail/sail2_operators_bitlists.cmi
lib/sail/sail2_operators.cmx
lib/sail/sail2_operators.cmi
lib/sail/sail2_instr_kinds.cmx
lib/sail/sail2_instr_kinds.cmi
lib/sail/sail.cmx
lib/sail/sail.cmi
lib/sail/rewrites.mli
lib/sail/rewrites.cmx
lib/sail/rewrites.cmi
lib/sail/rewriter.mli
lib/sail/rewriter.cmx
lib/sail/rewriter.cmi
lib/sail/reporting.mli
lib/sail/reporting.cmx
lib/sail/reporting.cmi
lib/sail/property.mli
lib/sail/property.cmx
lib/sail/property.cmi
lib/sail/profile.cmx
lib/sail/profile.cmi
lib/sail/process_file.mli
lib/sail/process_file.cmx
lib/sail/process_file.cmi
lib/sail/pretty_print_sail.cmx
lib/sail/pretty_print_sail.cmi
lib/sail/pretty_print_lem.cmx
lib/sail/pretty_print_lem.cmi
lib/sail/pretty_print_coq.cmx
lib/sail/pretty_print_coq.cmi
lib/sail/pretty_print_common.cmx
lib/sail/pretty_print_common.cmi
lib/sail/pretty_print.mli
lib/sail/pretty_print.cmx
lib/sail/pretty_print.cmi
lib/sail/pattern_completeness.mli
lib/sail/pattern_completeness.cmx
lib/sail/pattern_completeness.cmi
lib/sail/parser_combinators.cmx
lib/sail/parser_combinators.cmi
lib/sail/parser.mli
lib/sail/parser.cmx
lib/sail/parser.cmi
lib/sail/parse_ast.cmx
lib/sail/parse_ast.cmi
lib/sail/optimize.cmx
lib/sail/optimize.cmi
lib/sail/ocaml_backend.cmx
lib/sail/ocaml_backend.cmi
lib/sail/nl_flow.mli
lib/sail/nl_flow.cmx
lib/sail/nl_flow.cmi
lib/sail/monomorphise.mli
lib/sail/monomorphise.cmx
lib/sail/monomorphise.cmi
lib/sail/manifest.cmx
lib/sail/manifest.cmi
lib/sail/libsail.mllib
lib/sail/libsail.cmxa
lib/sail/libsail.cma
lib/sail/libsail.a
lib/sail/lexer.cmx
lib/sail/lexer.cmi
lib/sail/latex.cmx
lib/sail/latex.cmi
lib/sail/jib_util.cmx
lib/sail/jib_util.cmi
lib/sail/jib_ssa.mli
lib/sail/jib_ssa.cmx
lib/sail/jib_ssa.cmi
lib/sail/jib_smt_fuzz.cmx
lib/sail/jib_smt_fuzz.cmi
lib/sail/jib_smt.mli
lib/sail/jib_smt.cmx
lib/sail/jib_smt.cmi
lib/sail/jib_optimize.mli
lib/sail/jib_optimize.cmx
lib/sail/jib_optimize.cmi
lib/sail/jib_ir.cmx
lib/sail/jib_ir.cmi
lib/sail/jib_interactive.mli
lib/sail/jib_interactive.cmx
lib/sail/jib_interactive.cmi
lib/sail/jib_compile.mli
lib/sail/jib_compile.cmx
lib/sail/jib_compile.cmi
lib/sail/jib.cmx
lib/sail/jib.cmi
lib/sail/isail.cmx
lib/sail/isail.cmi
lib/sail/interpreter.cmx
lib/sail/interpreter.cmi
lib/sail/interactive.mli
lib/sail/interactive.cmx
lib/sail/interactive.cmi
lib/sail/initial_check.mli
lib/sail/initial_check.cmx
lib/sail/initial_check.cmi
lib/sail/graph.mli
lib/sail/graph.cmx
lib/sail/graph.cmi
lib/sail/gdbmi_types.cmx
lib/sail/gdbmi_types.cmi
lib/sail/gdbmi_parser.mli
lib/sail/gdbmi_parser.cmx
lib/sail/gdbmi_parser.cmi
lib/sail/gdbmi_lexer.cmx
lib/sail/gdbmi_lexer.cmi
lib/sail/gdbmi.cmx
lib/sail/gdbmi.cmi
lib/sail/error_format.cmx
lib/sail/error_format.cmi
lib/sail/elf_loader.cmx
lib/sail/elf_loader.cmi
lib/sail/constraint.mli
lib/sail/constraint.cmx
lib/sail/constraint.cmi
lib/sail/constant_propagation_mutrec.cmx
lib/sail/constant_propagation_mutrec.cmi
lib/sail/constant_propagation.mli
lib/sail/constant_propagation.cmx
lib/sail/constant_propagation.cmi
lib/sail/constant_fold.cmx
lib/sail/constant_fold.cmi
lib/sail/c_codegen.cmx
lib/sail/c_codegen.cmi
lib/sail/c_backend.mli
lib/sail/c_backend.cmx
lib/sail/c_backend.cmi
lib/sail/bitfield.cmx
lib/sail/bitfield.cmi
lib/sail/ast_util.mli
lib/sail/ast_util.cmx
lib/sail/ast_util.cmi
lib/sail/ast_defs.cmx
lib/sail/ast_defs.cmi
lib/sail/ast.cmx
lib/sail/ast.cmi
lib/sail/anf.mli
lib/sail/anf.cmx
lib/sail/anf.cmi
lib/sail/META
lib/sail
bin/sail