summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-10Check more types in monomorphisation rewritesThomas Bauereiss
2020-04-10Add test output to gitignoreThomas 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-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2020-04-10Make merlin know about pprintThomas Bauereiss
2020-04-10Implement hex_str for LemThomas Bauereiss
2020-04-10Be more careful when flow-typing loopsThomas Bauereiss
2020-04-01Update INSTALL.mdAlasdair Armstrong
2020-04-01Report SMT solver stderr on unexpected return codeBrian Campbell
2020-03-29Implement set_slice_int in the interpreterAlasdair
2020-03-25Merge pull request #64 from arichardson/intellij-syntaxAlasdair Armstrong
2020-03-25Fix a typo in write_mem for the interpreterAlasdair
2020-03-19Improve a particularly unhelpful type errorAlasdair
2020-03-18Add documentation for CLion/PyCharm/IntelliJ syntax highlightingAlex Richardson
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-24Allow overloading of subrange builtins for non-bitvectorsThomas Bauereiss
2020-02-24Avoid generating assertions multiple times during typecheckingThomas Bauereiss
2020-02-23Merge branch 'sail2' of https://github.com/rems-project/sail into sail2jp
2020-02-23set vscode syntax highlighting extension up for publicationjp
2020-02-21Add barriers to regfp.sail for full ARMv8Alasdair Armstrong
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
2020-02-20More list C codegen fixes for issue #59Alasdair Armstrong
2020-02-20Fix missing code generation builtins for lists. Fixes #59Alasdair Armstrong
2020-02-14mention vscode mode in READMEjp
2020-02-12add vscode syntax highlighting modejp
2020-02-12made list of required ubuntu packages completejp
2020-02-12Merge branch 'sail2' of https://github.com/rems-project/sail into sail2jp
2020-02-12improve syntax highlightingjp
2020-02-06Make sure tdiv_int and tmod_int are recognised by sail -iAlasdair Armstrong
2020-02-05Tweak Coq scopes for 8.11Brian Campbell
2020-02-03Add an __instr_announce builtin in regfp.sailAlasdair Armstrong
2020-02-03Update regfp.sail with ifetch changes from poly_mapping branchAlasdair Armstrong
2020-01-31Fix soundness bug found by MarkAlasdair
2020-01-30Make sure external pprint is listed as a dependency for sail when used as an ...Alasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:09:15 +0000