summaryrefslogtreecommitdiff
path: root/src/isail.ml
AgeCommit message (Expand)Author
2019-10-25Allow interactive commands to be setup outside isail.mlAlasdair Armstrong
2019-10-14Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and bitvector...Alasdair Armstrong
2019-06-19Rewriting improvements for monomorphic aarch64_smallBrian Campbell
2019-05-31Change specialization interface slightlyAlasdair Armstrong
2019-05-24Add a :thin_slice command to isail to isolate a given set of functionsBrian Campbell
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
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-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-13Refactor interpreter monad to include pp in effect requests/failuresJon French
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-03-08C: Refactor C backendAlasdair Armstrong
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-02-25Allow int-specialization for non-externs onlyAlasdair Armstrong
2019-02-25Merge branch 'sail2' into rmem_interpreterJon French
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-13Merge branch 'sail2' into rmem_interpreterJon French
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-28Merge branch 'sail2' into rmem_interpreterJon French
2018-12-27pass typechecking environment around interpreter and rewritersJon French
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-14interpreter: abstract effect requests into an Effect_request arm of frame typeJon French
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-10-15Interpreter: add new command :bin <addr> <file> to load raw binary into memoryJon French
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