summaryrefslogtreecommitdiff
path: root/src/sail.ml
AgeCommit message (Expand)Author
2018-06-04Fix an issue with riscv_platform involving flow typingAlasdair Armstrong
2018-06-04Fix bug with function return types in C backendAlasdair Armstrong
2018-05-28Coq: add option to produce axioms for unimplemented functionsBrian Campbell
2018-05-21Add an -ocaml-nobuild option to avoid building the generated ocaml by default...Prashanth Mundkur
2018-05-03Flow typing and l-expression changes for ASL parserAlasdair Armstrong
2018-05-03Work in progress on the coq backendBrian Campbell
2018-04-25Start working on documentationAlasdair Armstrong
2018-04-18add some experimental support for latex output in multiple files.Robert Norton
2018-04-04Use solver properly to simplify nexps in mono analysis, Lem printingBrian Campbell
2018-04-04Initial rewrite to move complex nexps in fn sigs into constraintsBrian Campbell
2018-03-14WIP Latex formattingAlasdair Armstrong
2018-03-14Fix toplevel pattern compilationAlasdair Armstrong
2018-03-12ELF loading for C backendAlasdair Armstrong
2018-03-09Specialise constructors for polymorphic unionsAlasdair Armstrong
2018-02-27Fix some bugs in C compilation, and optimise struct updatesAlasdair Armstrong
2018-02-26Add some obvious optimisations to C backend.Alasdair Armstrong
2018-02-23Fix some bugs in C compilationAlasdair Armstrong
2018-02-19Have generic vectors working in C backendAlasdair Armstrong
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss
2018-02-08Can now generate control flow graphs with C backendAlasdair Armstrong
2018-02-07Remove warnings during re-writingAlasdair Armstrong
2018-02-01More work on running sail tests compiled to CAlasdair Armstrong
2018-01-30Optionally give *all* monomorphisation errors at onceBrian Campbell
2018-01-30Updates to C backendAlasdair Armstrong
2018-01-30Generate functions from enums to numbers and vice versaAlasdair Armstrong
2018-01-25Add pattern completness check for match statementsAlasdair Armstrong
2018-01-25Add simple conditional processing and file includeAlasdair Armstrong
2018-01-24Have some simple sail programs compiling to CAlasdair Armstrong
2018-01-18Clean up command line options slightlyAlasdair Armstrong
2018-01-15Add help to interactive mode, and load files incrementallyAlasdair Armstrong
2018-01-15Refactored and improved ocaml interpreterAlasdair Armstrong
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
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-11Ocaml semantics can now run aarch64 hello world example using octapodAlasdair Armstrong
2018-01-10Add an all_split_errors optionBrian Campbell
2018-01-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
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-03Lots of experimental changes on this branchAlasdair Armstrong
2017-12-18Clean up last commitBrian Campbell
2017-12-18Handle multiple -lem_lib optionsBrian Campbell
2017-12-14Make sequential and mwords global variables in Lem pretty-printerThomas Bauereiss
2017-12-11Prototype interactive mode for sail.Alasdair Armstrong
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-30Improvements to enable parsing and checking intermediate rewritingAlasdair Armstrong
2017-11-14Automatic analysis for monomorphisationBrian Campbell
2017-11-10Fixed some tricky typechecking bugsAlasdair Armstrong
2017-11-03Fix a bug where sail would throw an exception with empty file listAlasdair Armstrong
2017-10-26Updated ocaml backend so tracing instrumentation is optional.Alasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:21:39 +0000