summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-05-04Lem: Add some reserved identifiersThomas Bauereiss
2020-05-04Add some more cases in mono rewritesThomas Bauereiss
2020-05-04Mono: Try to fix bug in inter-procedural analysisThomas Bauereiss
2020-05-04Try to fix bug in size parameter rewritingThomas Bauereiss
2020-04-29Add progress reporting to monomorphisationThomas Bauereiss
2020-04-27Fix try in exception handler jib bugBrian Campbell
2020-04-22Add an interactive command to evaluate until the end of a functionAlasdair
2020-04-21Fix build with OCaml 4.06.1Thomas Bauereiss
2020-04-21Lem: Print more type annotationsThomas Bauereiss
2020-04-21Add more SMT builtinsThomas Bauereiss
2020-04-21Add more monomorphisation rewritesThomas Bauereiss
2020-04-21Take kid synonyms into account when propagating constantsThomas Bauereiss
2020-04-21Mono: Check for non-constant calls to make_the_valueThomas Bauereiss
2020-04-21Mono: Extract more kid instantiations from assertionsThomas Bauereiss
2020-04-21Mono: Propagate constants after applying pattern choicesThomas Bauereiss
2020-04-21Add rewrite for constant-folding top-level letbindingsThomas Bauereiss
2020-04-21Various monomorphisation fixesThomas Bauereiss
2020-04-21Consider literals in pattern disjointness checkThomas Bauereiss
2020-04-21Mono: Extract set constraints from (in)equalitiesThomas Bauereiss
2020-04-21Handle more cases in bitvector cast rewriteThomas Bauereiss
2020-04-21Add support for some ASL idioms in mono rewritesThomas Bauereiss
2020-04-21Tweak types of loop combinators for prover combinatorsThomas Bauereiss
2020-04-21Save SMT cache when terminating with an exceptionThomas Bauereiss
2020-04-21Add more mono rewrites for bitvector subrangesThomas Bauereiss
2020-04-21Rewrite vector concat lexps to sequences of assignmentsThomas Bauereiss
2020-04-21Be more careful about type annotations in rewrites to LemThomas Bauereiss
2020-04-15Add more intuitive defaults to interactive toplevelAlasdair
2020-04-14Add add_symbol to the API of Process_fileAlasdair
2020-04-10Check more types in monomorphisation rewritesThomas Bauereiss
2020-04-10Allow empty Sail source filesThomas Bauereiss
2020-04-10Add Lem builtins for operations on realsThomas Bauereiss
2020-04-10Make bounds check for vector subrange assignments stricterThomas Bauereiss
2020-04-10Implement hex_str for LemThomas Bauereiss
2020-04-10Be more careful when flow-typing loopsThomas Bauereiss
2020-04-01Report SMT solver stderr on unexpected return codeBrian Campbell
2020-03-29Implement set_slice_int in the interpreterAlasdair
2020-03-25Fix a typo in write_mem for the interpreterAlasdair
2020-03-19Improve a particularly unhelpful type errorAlasdair
2020-03-18Expose details of failed lexp bounds checksThomas Bauereiss
2020-03-13SMT fixes for some corner cases of vector updatesThomas Bauereiss
2020-03-02Fix jenkinsAlasdair Armstrong
2020-03-02Add arith_shiftr to SMT and interpreterThomas Bauereiss
2020-02-25Implement count_leading_zeros for interpreterThomas Bauereiss
2020-02-24Avoid generating assertions multiple times during typecheckingThomas Bauereiss
2020-02-21Make sure we test that struct literals have a complete set of fields. Fixes #60Alasdair Armstrong
2020-02-21Distinguish type identifiers in topological sortingThomas Bauereiss
2020-02-21Fix bug in last patch to topological sorting (e5ee087f)Thomas Bauereiss
2020-02-21SMT: Implement a few more primopsThomas Bauereiss
2020-02-21Nl_flow: Consider early returnsThomas Bauereiss
2020-02-21Move topological sorting code to graph.mlThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:20:33 +0000