summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-05-11Functorise and refactor C code generatorAlasdair
2020-04-22Add an interactive command to evaluate until the end of a functionAlasdair
2020-04-15Add more intuitive defaults to interactive toplevelAlasdair
2020-04-14Add add_symbol to the API of Process_fileAlasdair
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
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-06Make sure tdiv_int and tmod_int are recognised by sail -iAlasdair 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
2020-01-28Use external PPrintThomas Bauereiss
2020-01-28Fix a bug with lexp->exp conversion for register referencesAlasdair
2020-01-22Preserve effect annotation when realising mappingsThomas Bauereiss
2020-01-21Reduce the amount of unnecessary parentheses in Coq outputBrian Campbell
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
2020-01-17Merge scattered mapping fixesJames Clarke
2020-01-17Merge branch 'coq-bool-props' into sail2Brian Campbell
2020-01-17Keep track of source locations for all IR branchesAlasdair
2020-01-16Allow effects on mappingsAlasdair Armstrong
2020-01-16Cleanup type-checking rule for LEXP_fieldAlasdair Armstrong
2020-01-16Keep track of (non-bit) vectors known to be fixed size in JibAlasdair Armstrong
2020-01-14Basic support to track uncaught exceptions in Sail->CAlasdair
2020-01-10Don't do any C specific name mangling for the cons operator in jib_compileAlasdair Armstrong
2020-01-04Coq: change record field update notation to avoid duplicating termsBrian Campbell
2020-01-03Add Sail pretty-printing of bitfieldsThomas Bauereiss
2019-12-18Make sure we generate literals of precisely the right length for symbolic exe...Alasdair Armstrong
2019-12-13move ott pp to different Makefile rulePeter Sewell
2019-12-13experiment in ott-generated ppPeter Sewell
2019-12-12Fix a little bit of inconsistency in the command line argumentsAlasdair Armstrong
2019-12-10Introduce new bitfield syntax for ASL translationAlasdair Armstrong
2019-12-06Don't introduce uneccesary control flow when compilingAlasdair Armstrong
2019-12-03Prover backends: Expand Int type synonyms in type definitionsThomas Bauereiss
2019-12-01Coq: remove last use and definition of doc_nc_propBrian Campbell
2019-11-29Merge branch 'word-numerals' into sail2Thomas Bauereiss
2019-11-29Tweak generated register_value typeThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:19:11 +0000