summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-12-19Coq: handle pairs of ranges (and other existential types) properlyBrian Campbell
2018-12-19Coq: add zeros library function (used by MIPS)Brian Campbell
2018-12-19Coq: handle existentials in hypotheses during solving, add max_nat, better castsBrian Campbell
2018-12-18Check more carefully for recursive functions when generating LemThomas Bauereiss
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian Campbell
2018-12-14Add some experimental support for non-lexical flow-typing rulesAlasdair Armstrong
2018-12-14Add a few more tests for JenkinsAlasdair Armstrong
2018-12-14Prepare for new release.Robert Norton
2018-12-14Add truncateLSB builtin useful for implementing Cheri Concentrate. Also add b...Robert Norton
2018-12-14Get real number tests working in OCaml/InterpreterAlasdair
2018-12-14A few additional testsAlasdair
2018-12-13Fix typo in boolean constraint desugaringAlasdair Armstrong
2018-12-13Remove redundant zero extensions more aggressively in mono rewritesThomas Bauereiss
2018-12-13Fix issue with sizeof-rewriting and monomorphisationAlasdair Armstrong
2018-12-13Fixing rationals in Sail interpreter and OCamlAlasdair Armstrong
2018-12-13Add hooks to call cgen stub file for RISC-VAlasdair Armstrong
2018-12-13Add a stub file for future cgen generationsAlasdair Armstrong
2018-12-13Merge remote-tracking branch 'origin/sail2' into asl_flowAlasdair
2018-12-12Fix some small bugsAlasdair
2018-12-12Add parallelism limit to C and builtins testAlasdair Armstrong
2018-12-12Move much of recursive function termination to a rewriteBrian Campbell
2018-12-12Add a test for flow typing as found in the ARM 32-bit instructionsAlasdair Armstrong
2018-12-12Add a test case for various simple boolean propertiesAlasdair Armstrong
2018-12-12Get typechecking example with boolean argument flow-typing workingAlasdair
2018-12-12Generalise existentials for non-integer type variablesAlasdair
2018-12-12Remove KOpt_none constructorAlasdair
2018-12-12Fix various boolean type-variable related issuesAlasdair
2018-12-11Fix all tests with type checking changesAlasdair Armstrong
2018-12-11Initial attempt at using termination measures in CoqBrian Campbell
2018-12-11Fix most remaining tests on branchAlasdair
2018-12-10Various changes:Alasdair Armstrong
2018-12-08Compiling againAlasdair
2018-12-07Working on better flow typing for ASLAlasdair Armstrong
2018-12-06Desugar constraints from atyp rather than n_constraintAlasdair Armstrong
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-12-04Remove FES_Fexps constructorAlasdair Armstrong
2018-12-04Simplify kinds in the ASTAlasdair Armstrong
2018-12-03Fix = / == in a couple of monomorphisation testsBrian Campbell
2018-11-30Remove constraint synonymsAlasdair Armstrong
2018-11-30Parser tweaks and fixesAlasdair Armstrong
2018-11-30RISC-V: update the riscv/readme to point to the new repository.Prashanth Mundkur
2018-11-30Improvements for ASL parserAlasdair Armstrong
2018-11-29RISC-V: more tidying up of the Spike interface.Prashanth Mundkur
2018-11-29RISC-V: implement WFI in the platform model.Prashanth Mundkur
2018-11-29RISC-V: factor the execution trace.Prashanth Mundkur
2018-11-29RISC-V: no ldu for rv64iBrian Campbell
2018-11-29RISC-V: properly set mstatus.FS in absence of floating-point support.Prashanth Mundkur
2018-11-29RISC-V: minor cleanup of the spike interface.Prashanth Mundkur
2018-11-29Update install instructions.Prashanth Mundkur
2018-11-29RISC-V: add some missing constraints on compressed instruction encodingsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 04:10:02 +0000