summaryrefslogtreecommitdiff
path: root/src/jib/anf.ml
AgeCommit message (Expand)Author
2019-05-01SMT: Fix some C optimisations that were disabledAlasdair Armstrong
2019-05-01Jib: Refactor V_callAlasdair Armstrong
2019-04-30SMT: Fix dead-code FIXME in jib_compileAlasdair Armstrong
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-20SMT: Support writing to register referencesAlasdair Armstrong
2019-04-17SMT: Support generic vectors and handle lets between specs and functionsAlasdair Armstrong
2019-04-17SMT: Unroll simple foreach loopsAlasdair Armstrong
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-09SMT: Refactor Jib values to make inlining workAlasdair Armstrong
2019-04-06Various bugfixes and improvementsAlasdair
2019-03-22C: Fix as-patterns in C outputAlasdair Armstrong
2019-03-15C: Wrap Jib identifiersAlasdair
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-03-08C: Refactor C backendAlasdair Armstrong