summaryrefslogtreecommitdiff
path: root/src/isail.ml
AgeCommit message (Expand)Author
2019-04-05Lem: Make generated assertion messages look nicer in prover outputAlasdair
2019-03-27C: Generate C from sliced specificationsAlasdair Armstrong
2019-03-27Interactive: Refactor sail.ml some moreAlasdair Armstrong
2019-03-27Interactive: Refactor sail.mlAlasdair Armstrong
2019-03-27Rewriter: Finish refactoring rewrite sequencesAlasdair Armstrong
2019-03-26Rewriter: Expose rewrite passes to interactive modeAlasdair Armstrong
2019-03-15Interactive: Auto-complete options and add hintsAlasdair Armstrong
2019-03-15Interactive: Auto-complete file namesAlasdair Armstrong
2019-03-14Add various useful methods to interactive modeAlasdair Armstrong
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-03-08C: Refactor C backendAlasdair Armstrong
2019-02-25Allow int-specialization for non-externs onlyAlasdair Armstrong
2019-02-22Fix some bugs in int-specializationAlasdair Armstrong
2019-02-19Refactor specializationAlasdair Armstrong
2019-02-14Don't do any rewrites when checking files for EmacsAlasdair Armstrong
2019-02-12Improvements for emacs modeAlasdair Armstrong
2019-02-08Rewrite type definitions in rewrite_nexp_idsThomas Bauereiss
2019-02-06Emacs mode understands relationships between Sail filesAlasdair
2019-02-06Improve emacs modeAlasdair Armstrong
2018-12-26Some cleanupAlasdair Armstrong
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
2018-12-19Improve sizeof rewriting performanceAlasdair Armstrong
2018-12-10Various changes:Alasdair Armstrong
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-11-23C backend improvementsAlasdair Armstrong
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-09-06Allow options to be set in the interactive modeAlasdair Armstrong
2018-08-23Fix interpreter after re-writer changeAlasdair Armstrong
2018-08-16Various cleanups to ott grammarAlasdair Armstrong
2018-07-12Handle failures during interpreting betterAlasdair Armstrong
2018-06-07Add a constant folding optimization passAlasdair
2018-06-06Factor utility functions for IR into separate file and struct update optimiza...Alasdair Armstrong
2018-06-06Some work on improving error messagesAlasdair Armstrong
2018-05-31Fixes to get ARM u-boot working in Sail.Alasdair Armstrong
2018-04-25Start working on documentationAlasdair Armstrong
2018-03-14WIP Latex formattingAlasdair Armstrong
2018-03-01Cleanup intermediate bytecode representation in C backendAlasdair Armstrong
2018-02-07Have exceptions working in C backendAlasdair Armstrong
2018-01-30Updates to C backendAlasdair Armstrong
2018-01-24More work on experimental C backendAlasdair Armstrong
2018-01-23Started working on C backend for sailAlasdair Armstrong
2018-01-22Added rewriter that specializes all function calls in a specification.Alasdair Armstrong
2018-01-18Modified unification so Type_check.instantiation_of works after sizeof rewritingAlasdair Armstrong
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-15Add help to interactive mode, and load files incrementallyAlasdair Armstrong
2018-01-15Refactored and improved ocaml interpreterAlasdair Armstrong
2018-01-12OCaml interactive mode can now run full aarch64 examples, and ocaml test cases.Alasdair Armstrong