summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-10-24Limit quantifiers printed in Lem to type variables that actuallyBrian Campbell
2017-10-24Handle existential types in Lem backend by stripping them andBrian Campbell
2017-10-24Generate undefined_bitvector function when targeting machine wordsBrian Campbell
2017-10-24Produce debug message when an expression can't be converted to a constraintBrian Campbell
2017-10-24Remove special case for boolean (as opposed to bool)Brian Campbell
2017-10-23Type check external castsBrian Campbell
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-10-19Fix pretty-printing of type abbreviation definitions with argumentsThomas Bauereiss
2017-10-19Mangle names with '#' characters in Lem pretty-printingThomas Bauereiss
2017-10-19Rewrite undefined values, add type annotations to early returnsThomas Bauereiss
2017-10-19Make some potentially non-terminating library functions terminateThomas Bauereiss
2017-10-19Preserve more type environment information during rewritingThomas Bauereiss
2017-10-19Follow AST changes in (Lem) pretty-printersThomas Bauereiss
2017-10-18Fixes and updates to ocaml backend to compile aarch64_no_vectorAlasdair Armstrong
2017-10-18Merge branch 'experiments' of Peter_Sewell/sail into mono-experimentsBrian Campbell
2017-10-13Handle bitvector_access in constant propagationBrian Campbell
2017-10-13Make Sail_values.repeat total, and remove duplicateBrian Campbell
2017-10-13Fix some bugs that surfaced in the ASL exportThomas Bauereiss
2017-10-13Add rewriting step for tuple-vector assignmentsThomas Bauereiss
2017-10-13Add rewriting step for function effect propagationThomas Bauereiss
2017-10-13Name (bit)vector operations more explicitlyThomas Bauereiss
2017-10-13Add support for real numbers to Lem backendThomas Bauereiss
2017-10-13Improve debugging outputThomas Bauereiss
2017-10-13Repeat and while loops in menhir parser and pretty printerAlasdair Armstrong
2017-10-12Fixes pattern matching exact values ([:'n:]) on integer literalsAlasdair Armstrong
2017-10-10More improvements to menhir parserAlasdair Armstrong
2017-10-10Fixes to menhir parser and pretty printerAlasdair Armstrong
2017-10-09Improvements to menhir pretty printer and ocaml backendAlasdair Armstrong
2017-10-06Remove BK_effect constructorAlasdair Armstrong
2017-10-06Various improvements to menhir parser, and performance improvments for Z3 callsAlasdair Armstrong
2017-10-06Produce type signatures in Lem outputBrian Campbell
2017-10-06Implement replicate_bits for mwordsBrian Campbell
2017-10-06Fix constant propagation on multi-argument functionsBrian Campbell
2017-10-04Fixed a bug in vector concatenation l-expressionsAlasdair Armstrong
2017-10-04Add pretty printer for menhir parserAlasdair Armstrong
2017-10-04Merge branch 'cleanup' into experimentsAlasdair Armstrong
2017-10-04Add pretty printing for while loopsAlasdair Armstrong
2017-10-04Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-10-03Fixes to new parserAlasdair Armstrong
2017-10-03Fixed some loop bugs for ASL parserAlasdair Armstrong
2017-10-02Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-02Make undefined constant propagation stop at ex_intBrian Campbell
2017-09-29Support vector registers (other than bitvectors)Thomas Bauereiss
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
2017-09-29Add MIPS->Isabelle target to MakefileThomas Bauereiss
2017-09-28Use (K)Bindings from ast_util rather than making new onesBrian Campbell
2017-09-28Add loops to monomorphisationBrian Campbell
2017-09-28Merge branch 'experiments' into mono-experimentsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 07:48:50 +0000