summaryrefslogtreecommitdiff
path: root/src/jib/anf.ml
AgeCommit message (Expand)Author
2020-08-10Fix a C backend bug with letbindings in guards shadowing body definitionsAlasdair
2020-06-23Fix bug with duplicate enum identifiers in patternsAlasdair
2020-05-22Fix atomicity of register field writesAlasdair
2020-05-15Add coverage tracking toolAlasdair
2020-05-12Add support for instrumenting generated C with branch coverage metricsAlasdair
2019-10-28Some C backend refactoringAlasdair
2019-10-25Remove global symbol generatorAlasdair
2019-10-25Refactor Jib IR pretty printerAlasdair Armstrong
2019-06-04Make sure aarch64_small can generate Jib for SMTAlasdair Armstrong
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
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