summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-11-14interpreter: abstract effect requests into an Effect_request arm of frame typeJon French
2018-11-14update riscv_all.sail and riscv_platform.sail for updated riscv modelJon French
2018-11-13Make pretty printer stricter with brace placementAlasdair Armstrong
2018-11-13add linenoise to .merlinJon French
2018-11-12Infer tuple l-expressions types if all components are inferrableAlasdair Armstrong
2018-11-12Make type checker smarter at inferring l-expressionsAlasdair Armstrong
2018-11-12Add referencing commands to generated latexAlasdair Armstrong
2018-11-12rvfi_dii: take port number with optionBrian Campbell
2018-11-12Fix numbers in constructor argumentsAlasdair Armstrong
2018-11-12Improve latex naming scheme and avoid collisionsAlasdair Armstrong
2018-11-12Add RVFI DII version of the RISC-V simulator for TestRIGBrian Campbell
2018-11-12opam releaseRobert Norton
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-11-09RISC-V: add missed c.ebreak instructionPrashanth Mundkur
2018-11-09Add test case for passing register referencesThomas Bauereiss
2018-11-08RISC-V: fix a typo-induced bug in updating the PTE.Prashanth Mundkur
2018-11-07RISC-V: fix assembly mappings for lr/sc.Prashanth Mundkur
2018-11-07Move inline forall in function definitionsAlasdair Armstrong
2018-11-07Move inline forall in function definitionsAlasdair Armstrong
2018-11-07RISC-V: add some consistency checks when run with spike.Prashanth Mundkur
2018-11-06Fix bug with loop indices not being mapped to int64 in CAlasdair Armstrong
2018-11-05Ensure function quantifier is in scope when generating C return typeAlasdair Armstrong
2018-11-05Add a regression test for issue #22Alasdair Armstrong
2018-11-05Ensure type-synonyms are handled correctly in register dependenciesAlasdair Armstrong
2018-11-05Make sure undefined_type functions are generated before registersAlasdair Armstrong
2018-11-02Add code to analyse function return typesAlasdair Armstrong
2018-11-02Coq: add more autocasts for different but equal kidsBrian Campbell
2018-11-01Changes to enable analysing type errors in ASL parserAlasdair Armstrong
2018-11-01Merge branch 'sail2' into rmem_interpreterJon French
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-31Fix Isabelle 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-29Merge pull request #21 from rems-project/riscv_c_platformAlasdair 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-24RISC-V: add Sail implementations of just enough platform for interpreter to workJon French
2018-10-24add a couple things to gitignoreJon 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-23RISC-V: switch c tests to use the C platform simulator; update .gitignore.Prashanth Mundkur
2018-10-23RISC-V: use stderr for terminal output in OCaml backend.Prashanth Mundkur
2018-10-23RISC-V: separate jalr execute clause for seq model and rmem.Prashanth Mundkur
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 01:43:05 +0000