summaryrefslogtreecommitdiff
path: root/src/sail.ml
AgeCommit message (Expand)Author
2019-01-21Add output directory option for generated Isabelle auxiliary theoriesThomas Bauereiss
2019-01-21Fix some issues with latex generation so manual builds againAlasdair Armstrong
2019-01-14Add options for output directories for the lem and coq backends.Prashanth Mundkur
2018-12-14Add some experimental support for non-lexical flow-typing rulesAlasdair Armstrong
2018-12-13Add hooks to call cgen stub file for RISC-VAlasdair Armstrong
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-11-30Remove constraint synonymsAlasdair Armstrong
2018-11-27Fix memory leak in string_of_bitsAlasdair Armstrong
2018-11-23C backend improvementsAlasdair Armstrong
2018-11-19Merge branch 'latex' into sail2Robert Norton
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-11-15When outputing latex do not expand type synonyms in val specs during type check.Robert Norton
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-11-06Fix bug with loop indices not being mapped to int64 in CAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-10-24Add constraint synonymsAlasdair Armstrong
2018-10-02Trigger random generator generation with a command line optionBrian Campbell
2018-10-02Rough code to generate random instructions for testingBrian Campbell
2018-09-20Tidy up help text for a few optionsBrian Campbell
2018-09-13C: Fix an issue with assigning to unitialized variables at end of blocksAlasdair Armstrong
2018-09-06Allow options to be set in the interactive modeAlasdair Armstrong
2018-09-04C: add an option to control generation of main().Prashanth Mundkur
2018-08-30Allow additional includes to be specified for C backend.Prashanth Mundkur
2018-08-23Fix interpreter after re-writer changeAlasdair Armstrong
2018-08-17Improve builtins testsAlasdair Armstrong
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
2018-07-24Merge branch 'c_fixes' into sail2Alasdair Armstrong
2018-07-24Merge remote-tracking branch 'origin/sail2' into c_fixesAlasdair Armstrong
2018-07-24Move monomorphisation after mapping rewritesBrian Campbell
2018-07-23Coq: make all pattern matches in the output exhaustiveBrian Campbell
2018-07-08Add -static flag that controls whether generated C functions are staticAlasdair
2018-06-29Try to fix some tricky C compilation bugs, break everything insteadAlasdair Armstrong
2018-06-28Add option to build ocaml with bisect_ppx coverage support. Add cheri targets...Robert Norton
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-19Coq: use undefined_bitvectorBrian Campbell
2018-06-15Fixes for C RTS for aarch64 no it's split into multiple filesAlasdair Armstrong
2018-06-13Tracing instrumentation for C backendAlasdair Armstrong
2018-06-07Add a constant folding optimization passAlasdair
2018-06-06Some additional fixes to C backend. Re-enable primitive optimizations.Alasdair Armstrong
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 07:20:28 +0000