summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-11-01Interpreter: last couple of builtins to get RISC-V workingJon French
2018-10-31Add rewriting pass for not-patternsAlasdair Armstrong
2018-10-31Remove Parse_ast.Int, add unique locationsAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-10-31Add helper functions in Sail Lem libraryThomas Bauereiss
2018-10-31Monad refactoring in Lem shallow embeddingThomas Bauereiss
2018-10-31Improve error messages for unsolved function quantifiersAlasdair Armstrong
2018-10-29Pretty printer tweaks for ASL parserAlasdair Armstrong
2018-10-24Add constraint synonymsAlasdair Armstrong
2018-10-24Interpreter, RISC-V: move memory actions to parts of the interpreter response...Jon French
2018-10-24Interpreter: add handling of undefs and sizeofs, and initialize registers to ...Jon French
2018-10-24Interpreter: improve error handling/messagesJon French
2018-10-24src/Makefile: add isail.byte target for debugging interpreterJon French
2018-10-24Interpreter: don't silently use OCaml externs, only interpreter externsJon French
2018-10-22Coq: use function type more carefully in untuplingBrian Campbell
2018-10-22Coq: work around constructors with tupled argumentsBrian Campbell
2018-10-22Fix lem arguments for functions with tuple argumentsAlasdair Armstrong
2018-10-22Merge branch 'sail2' into rmem_interpreterJon French
2018-10-22Pretty_print_lem.untuple_args_pat: temporary hack to allow functions that act...Jon French
2018-10-16Merge branch 'sail2' into rmem_interpreterJon French
2018-10-16Re-implement space-related mapping functions in Sail rather than backendsJon French
2018-10-16rewrites: remove now-unnecessary temporary string hack from rewrite_defs_pat_...Jon French
2018-10-15Ocaml backend: omit function definitions for externsJon French
2018-10-15Interpreter: add new command :bin <addr> <file> to load raw binary into memoryJon French
2018-10-11Change the function type in the ASTAlasdair
2018-10-10refer to Util.list_init.ml rather than List.init in sail_lib.mlChristopher Pulte
2018-10-08Interpreter: refactor get/put state into more fine-grained responses in the m...Jon French
2018-10-08Produce lists of constructors and ast building functions for test generationBrian Campbell
2018-10-05interpreter: Remove boxes (no longer used)Jon French
2018-10-05fix bug in infer_mpat losing types of identifiers inferred from other_envJon French
2018-10-04Merge branch 'ocaml-instruction-generation' into sail2Brian Campbell
2018-10-04Bit of commentary, proper TODO errorBrian Campbell
2018-10-04rename stringappend ids for more readable generated codeJon French
2018-10-03Drop unnecessary thunking; more trouble than it's worthBrian Campbell
2018-10-02Tidy up some whitespaceBrian Campbell
2018-10-02Clean up generator pretty printingBrian Campbell
2018-10-02Remove some old debugging messagesBrian Campbell
2018-10-02Trigger random generator generation with a command line optionBrian Campbell
2018-10-02Rough code to generate random instructions for testingBrian Campbell
2018-10-01Extend Coq pattern match completeness rewrite to let patternsBrian Campbell
2018-10-01New rewriting pass toplevel_string_appendJon French
2018-09-28Fix optimisation bug for certain if statementsAlasdair Armstrong
2018-09-27Add new functions in ast_util.ml for working with locationsAlasdair Armstrong
2018-09-24Coq: avoid variables called tt (the unit constant)Brian Campbell
2018-09-24Coq: add autocasts at monad returnsBrian Campbell
2018-09-20Tidy up help text for a few optionsBrian Campbell
2018-09-19Coq: track changes elsewhereBrian Campbell
2018-09-19rewrite_defs_pat_string_append: fix bug with guarded SomeJon French
2018-09-19separate decimal_string_of_bits from string_of_bitsJon French
2018-09-19src/gen_lib/sail2_string.lem: more Lem monomorphisations for hex_bits_N_match...Jon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 17:36:07 +0000