summaryrefslogtreecommitdiff
path: root/src/sail.ml
AgeCommit message (Expand)Author
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-23SMT: Add parser for generated modelsAlasdair Armstrong
2019-04-17SMT: Automatically get model when $counterexample is used rather than $propertyAlasdair Armstrong
2019-04-17SMT: Support register referencesAlasdair Armstrong
2019-04-15SMT: Allow partial specializationsAlasdair Armstrong
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-13SMT: Add count_leading_zeros and more builtinsAlasdair
2019-04-13SMT: More builtinsAlasdair
2019-04-11SMT: Add property and counterexample directiveAlasdair Armstrong
2019-04-09SMT: Experimental Jib->SMT translationAlasdair Armstrong
2019-04-05Fix: Don't remove uncalled polymorphic constructors if they are matched uponAlasdair Armstrong
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-26Rewriter: Expose rewrite passes to interactive modeAlasdair Armstrong
2019-03-19C: Some simplificationAlasdair Armstrong
2019-03-15Add a rewriting pass for constant propagation in mutrecsThomas Bauereiss
2019-03-14C: Some further tweaksAlasdair Armstrong
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-13Remove prover reference from typecheck env when marshalling out defsJon French
2019-03-13C: Improve Jib IR, add SSA representationAlasdair Armstrong
2019-03-09C: Fix miscompilation of constrained struct field accessAlasdair
2019-03-08C: Refactor C backendAlasdair Armstrong
2019-03-06Add an -ir option to print the intermediate representation of a fileAlasdair Armstrong
2019-03-05More optimizations and improvments for C generationAlasdair Armstrong
2019-03-05Additional optimizations for C compilationAlasdair
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-03-04Marshalling: remove prover before marshallingJon French
2019-03-04Do not store type synonyms as functions in the environmentAlasdair Armstrong
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-02-28Allow user-specified state to be passed through generated CAlasdair Armstrong
2019-02-27Tweaks to C compilation to make it more usable for embedding into other programsAlasdair Armstrong
2019-02-27Make -o option work as usual with C compilationAlasdair Armstrong
2019-02-26Further work on toFromInterp backendJon French
2019-02-25Allow int-specialization for non-externs onlyAlasdair Armstrong
2019-02-25Merge branch 'sail2' into rmem_interpreterJon French
2019-02-22Fix more bugs in int-specializationAlasdair Armstrong
2019-02-19Refactor specializationAlasdair Armstrong
2019-02-19Progress on toFromInterp backend from-interp generationJon French
2019-02-18Add option to linearize constraints containing exponentialsAlasdair Armstrong
2019-02-15Use multiple solversAlasdair
2019-02-14Don't do any rewrites when checking files for EmacsAlasdair Armstrong
2019-02-13Merge branch 'sail2' into rmem_interpreterJon French
2019-02-08Slightly tweak the help message.Prashanth Mundkur
2019-02-08Resurrect Sail output option (with new name: -output_sail)Brian Campbell
2019-02-08Rewrite type definitions in rewrite_nexp_idsThomas Bauereiss
2019-02-07Fix implicits in v8.2 public ARM specAlasdair Armstrong
2019-02-06Emacs mode understands relationships between Sail filesAlasdair
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:12:51 +0000