summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-01-19Update monomorphisation for sail2Brian Campbell
2018-01-18Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-18Modified ocaml backend to use ocamlfind for linksem and lemAlasdair Armstrong
2018-01-18Add elf_loader fileAlasdair Armstrong
2018-01-18Modified unification so Type_check.instantiation_of works after sizeof rewritingAlasdair Armstrong
2018-01-17Use right effect annotations in early return rewritingThomas Bauereiss
2018-01-17Try to remove early returns more aggressivelyThomas Bauereiss
2018-01-17Rewrite topological sortingThomas Bauereiss
2018-01-17Fix use of nexps in type annotations when not using machine wordsThomas Bauereiss
2018-01-16Test the ocaml interpreter with the same tests as the ocaml compilationAlasdair Armstrong
2018-01-16Created version of typecheck test suite for sail2 branchAlasdair Armstrong
2018-01-16Fix problem with let-bindings in pattern guardsThomas Bauereiss
2018-01-16Output more type annotations in Lem backendThomas Bauereiss
2018-01-16Handle for loops correctly when rewriting size parametersBrian Campbell
2018-01-16Another useful monomorphisation rewriteBrian Campbell
2018-01-15Add help to interactive mode, and load files incrementallyAlasdair Armstrong
2018-01-15Check monomorphisation case split size once for each patternBrian Campbell
2018-01-15Refactored and improved ocaml interpreterAlasdair Armstrong
2018-01-15Support non-trivial literal patternsBrian Campbell
2018-01-12Interpreter can now pass local values by referenceAlasdair Armstrong
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-12Try to keep types for undefined around during monomorphisationBrian Campbell
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-12OCaml interactive mode can now run full aarch64 examples, and ocaml test cases.Alasdair Armstrong
2018-01-12Remove generic comparisonBrian Campbell
2018-01-12Support constant propagation on casts in monomorphisationBrian Campbell
2018-01-11Ocaml semantics can now run aarch64 hello world example using octapodAlasdair Armstrong
2018-01-10Add an all_split_errors optionBrian Campbell
2018-01-10Fix control dependencies in monomorphisation analysisBrian Campbell
2018-01-09More monomorphisation rewrites for aarch64Brian Campbell
2018-01-09Tidy up monomorphisation interfaceBrian Campbell
2018-01-09Proper location for no set constraint errorsBrian Campbell
2018-01-09Move reordering in alpha_equivalent before relabelling to giveBrian Campbell
2018-01-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
2018-01-08Improved fix for alpha-equivalence re-ordering issueAlasdair Armstrong
2018-01-08Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2018-01-08Potential fix for bug where different quantifer order in existentials will br...Alasdair Armstrong
2018-01-05Moved parser, lexer and pretty printer to correct locations.Alasdair Armstrong
2018-01-05Removed legacy parser/lexer and pretty printerAlasdair Armstrong
2018-01-05Fix duplicate definitions created by mergeAlasdair Armstrong
2018-01-05Merge remote-tracking branch 'origin/interactive' into vectorAlasdair Armstrong
2018-01-05Added sail_lib fileAlasdair Armstrong
2018-01-05Added bitfield syntax to replicate register bits typeAlasdair Armstrong
2018-01-04Additional tests for ocaml backendAlasdair Armstrong
2018-01-03Lots of experimental changes on this branchAlasdair Armstrong
2018-01-03Updates to interpreterAlasdair Armstrong
2018-01-02Experimenting with power specAlasdair Armstrong
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-19Add rewriting step for numeral patternsThomas Bauereiss
2017-12-19Fix a bug in untupling function arguments for LemThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 15:37:14 +0000