summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-04-23Add isla builtin testing and update coq scriptsail2Brian Campbell
(both off by default)
2021-03-24Fix lemma for current HOL4Brian Campbell
(should also work for older versions)
2021-03-18add else as keywordjp
2021-03-12coq-bbv dependency should be a lower boundBrian Campbell
2021-03-12Add even more conservative version bound to omdAlasdair
2021-03-12Add upper version bound on omdAlasdair
2021-03-05Add more location information to IRAlasdair
2021-02-25Remove accidental use of too-recent Option moduleBrian Campbell
Also drop a related bit of dead code
2021-02-25Add -infer_effects optionBrian Campbell
2021-02-24Fill out some missing cases in free variable calculationBrian Campbell
In particular, some of these affected the topological sorting.
2021-02-24sailcov: fix usage informationBrian Campbell
2021-02-17Make sure :step_function appears in :commandsAlasdair
2021-02-17Check if an unbound identifier is bound as a function identifierAlasdair
Give a hint in the error message if this is the case
2021-01-07Update version number in opam fileAlasdair
2021-01-06Don't use x86 intrinsicsAlasdair
2021-01-05Fix some cases when monomorphising vectors containing variable-length bitvectorsAlasdair
2021-01-05Enum value feature request for AlexandreAlasdair
2021-01-05Don't allow type synonyms with the same name as existing typesAlasdair
2020-11-25Remove bogus pattern completeness warning on singleton enums and unionsBrian Campbell
2020-11-25Fix Lem output for single element enumBrian Campbell
2020-11-25Fix BLRShaked Flur
Reorder the read and write of registers to allow MP+dmb.sy+blr-addr.
2020-11-25Make WFE, SEV and SEVL effectively NOPsShaked Flur
2020-11-21Make coverage support look a little harder for location informationBrian Campbell
2020-11-20Add coverage output to short-circuiting operatorsBrian Campbell
2020-11-19Add write tag primitiveBrian Campbell
2020-11-19Make mono rewrites be more careful to produce constant-sized typesBrian Campbell
While the backends will usually manage to find the constant size anyway, this ensures that implicit arguments will be filled in with the constant value too. (For example, this was affecting isla execution in one corner case because the slice_mask primitive didn't see that the size was constant.)
2020-11-19Specifically note that Ubuntu 18.04 needs a new opamBrian Campbell
2020-11-18Fix coverage information in case branches that immediately returnBrian Campbell
2020-11-13sailcov: Correct ordering for cumulative coverage outputBrian Campbell
2020-11-09Update README.mdAlasdair Armstrong
2020-11-01Fix interpreter pattern matching bugAlasdair
2020-10-29Update INSTALL.mdAlasdair Armstrong
2020-10-29Update BUILDING.mdAlasdair Armstrong
2020-10-23sailcov: fix zero width branches in --colour-by-count modeBrian Campbell
2020-10-22sailcov: correct histogram table headingBrian Campbell
2020-10-22sailcov: Add cumulative histogram CSV outputBrian Campbell
2020-10-21Merge pull request #106 from jrtc27/latex-abbrevs-spacingAlasdair Armstrong
latex: Guard abbreviations with \@
2020-10-20sailcov: add alternative colouring using the file count for each spanBrian Campbell
2020-10-19sailcov: Make meaning of the histogram clearerBrian Campbell
2020-10-19sailcov: add basic histogramBrian Campbell
2020-10-19sailcov: Rearrange span data per fileBrian Campbell
2020-10-14Add multiple coverage file support to sailcovBrian Campbell
2020-10-14Support C coverage when sail_exit is usedBrian Campbell
2020-10-07latex: Guard abbreviations with \@Jessica Clarke
Otherwise they will be typeset as if the end of a sentence, causing additional spacing after the '.' when not using \frenchspacing.
2020-10-01Merge pull request #105 from capt-hb/load-elf-fixAlasdair Armstrong
Load ELF: pass pointer to g_elf_entry to get the ELF entry
2020-10-01Merge pull request #102 from Trolldemorted/bennidockerAlasdair Armstrong
Add Dockerfile that builds sail from source
2020-10-01Add ast_defs to libsailAlasdair
2020-10-01pass pointer to g_elf_entry to get the ELF entrySander Huyghebaert
2020-09-30Add Dockerfile that builds sail from sourceBenedikt Radtke
2020-09-30Tweak Coq proof to avoid incompatibility with IrisBrian Campbell
(in the previous proof script the intuition tactic found a strange proof involving a type-level dependent pair that imposed an unnecessary universe constraint, this doesn't)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 06:44:43 +0000