summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-14Coq: tidy up scope in libraryBrian Campbell
Helps with Coq 8.11. Also fix BBVDIR default in test script.
2020-06-12Coq: fix matching bug in solverBrian Campbell
2020-06-12Update sailcov readme for option changeAlasdair Armstrong
2020-06-12Merge pull request #70 from rems-project/branch-info-output-fileAlasdair Armstrong
Use output file for generated branch information.
2020-06-12Use output file for generated branch information.Prashanth Mundkur
2020-06-12Remove remove field from opam fileAlasdair
As per https://github.com/ocaml/opam-repository/pull/16573
2020-06-11Coq: specialise the andor solvers to avoid excessive search and solve more goalsBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
- rename files to get rid of prefix - use -Q to get package name right - add Base.v to make package imports simpler - add opam file for coq package
2020-06-09Add splice.ml to libsailThomas Bauereiss
2020-06-05Generate nice error messages for patterns woth duplicate bindingsAlasdair
2020-06-03Update CHANGELOGAlasdair
2020-06-03Correct compiler version in CI scriptAlasdair
2020-06-03Add a workflow for latest released ocamlAlasdair
2020-06-03Update opam file to opam 2Alasdair
2020-06-03add docker makefile targetjp
2020-06-02Add m4 to 18.04 installAlasdair
It previously installed fine via the build-essential package, so no idea what changed! Plus 20.04 works fine with just build-essential
2020-06-02Add ubuntu 20.04 workflowAlasdair
2020-05-27Try to fix Github CIThomas Bauereiss
Add opam PPA when building on Ubuntu to get opam v2.
2020-05-27Update base64 and yojson dependenciesThomas Bauereiss
2020-05-22Fix atomicity of register field writesAlasdair
Previous merge commit caused some code that was generating register.field = value to instead generate temp = register temp.field = value register = temp This was caused by rewriter changes affecting the ANF form, and the Jib compilation was sensitive to small changes in the ANF form when compiling l-expressions. Rather than applying a band-aid fix in the rewriter this commit re-factors the ANF translation of l-expressions to ensure that the jib compilation is more robust and able to consistently generate the correct l-expressions without introducing additional read-modify-write expressions in the code.
2020-05-21Merge branch 'mono-tweaks' into sail2Alasdair
2020-05-21Merge branch 'mono-tweaks' of github.com:rems-project/sail into mono-tweaksAlasdair
2020-05-21Merge branch 'sail2' into mono-tweaksAlasdair
2020-05-19Update readme with min OCaml versionAlasdair Armstrong
2020-05-18Add a prefix option for generated coverage filesAlasdair
2020-05-18Add a header and a default page to the index in coverage reportsAlasdair
2020-05-15Merge pull request #67 from arichardson/add-staticAlasdair Armstrong
Add static to more C functions
2020-05-15Remove some left over debug statementsAlasdair
2020-05-15Generate index for coverageAlasdair
2020-05-15C backend: Only add static to model_{init,fini} if -static is passedAlex Richardson
Otherwise the C emulator doesn't build.
2020-05-15C backend: Add a static () helperAlex Richardson
This simplifies some of the code.
2020-05-15Fix more typosAlasdair
2020-05-15Tweak readmeAlasdair
2020-05-15Add colour options to sailcovAlasdair
Colours can be tweaked for aesthetics by setting hue and saturation individually or there is an --alt-colo[u]rs flag which switches to a yellow/blue mode that should be better for red/green colourblindness.
2020-05-15Add static to registers if -static is passedAlex Richardson
This was the final missing step for me to link two almost identical C files generated from sail into the same library.
2020-05-15Also make the letbinding C variables staticAlex Richardson
I was getting run-time failures when code generate from cheri128 and cheri64 in the same process. This was caused because my compiler defaults to -fcommon so it merged multiple variables (with conflicting types!). When initializing the second set of letbindings, the first one was overwritten (first variable was lbits, the other was uint64_t). Compiling with -fno-common exposes this problem.
2020-05-15Also allow adding static to model_{init,fini,main}()Alex Richardson
Without this I get the following linker error when trying to include both 64 and 128 bit sail-riscv code in the same binary: duplicate symbol '_model_init' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) duplicate symbol '_model_main' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) duplicate symbol '_model_fini' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) # Conflicts: # src/jib/c_backend.ml
2020-05-15Add static to more C functionsAlex Richardson
This allows me to compile sail-riscv64 and sail-riscv128 code in the same static library.
2020-05-15Add --tab-width option to sailcovAlasdair
2020-05-15Update type error messages for jenkinsAlasdair
Location info fixes changed the location reported for an expected type error very slightly
2020-05-15Move riscv_vmem_sv39 example to a separate page so it renders nicelyAlasdair
2020-05-15Add example output for coverage visualisationAlasdair
2020-05-15Add coverage headerAlasdair
2020-05-15Fix linksAlasdair
2020-05-15Add sailcov readmeAlasdair
2020-05-15Add coverage tracking toolAlasdair
See sailcov/README.md for a short description Fix many location info bugs discovered by eyeballing output
2020-05-14Output INT64_MIN in code generator for min 64-bit integer literalAlasdair
Fixes the warning generated because in C -X where X is the minimum integer is parsed as a positive integer which is then negated. This causes a (I believe spurious) warning that the integer literal is too large for the type. Also using INT64_C so we get either long or long long depending on platform
2020-05-14Merge remote-tracking branch 'origin' into codegenAlasdair
2020-05-14Re-activate some testsAlasdair
2020-05-14Attempt to fix CI errorAlasdair
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 17:19:09 +0000