index
:
sail
sail2
Formal specification language for ISAs
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
Age
Commit message (
Expand
)
Author
2019-03-14
Report when the SMT solver fails badly
Brian Campbell
2019-03-13
C: Improve Jib IR, add SSA representation
Alasdair Armstrong
2019-03-13
Tell Lem that records parametrised over Ints need the len typeclass annotations
Brian Campbell
2019-03-12
Coq: fix parametrized record types
Brian Campbell
2019-03-12
Coq: fix some boolean issues seen in arm
Brian Campbell
2019-03-11
Improve ocamldoc comments
Alasdair Armstrong
2019-03-09
C: Fix miscompilation of constrained struct field access
Alasdair
2019-03-09
Adds missing bits for DC/IC
Shaked Flur
2019-03-08
Rewriter: Cleanup old sizeof rewrites
Alasdair Armstrong
2019-03-08
C: Refactor C backend
Alasdair Armstrong
2019-03-08
Fix: Never consider single variable types to be ambiguous
Alasdair
2019-03-07
Remove more dead branches
Thomas Bauereiss
2019-03-07
Also remove impossible if-branches
Thomas Bauereiss
2019-03-07
Fix bug in a mono rewrite helper function
Thomas Bauereiss
2019-03-07
C: Make instrs_graph return just control flow graph
Alasdair Armstrong
2019-03-07
Add a rewrite to remove impossible cases on integer literals
Brian Campbell
2019-03-07
Simplify handling of referenced variables in constant propagation
Brian Campbell
2019-03-07
Extract constant propagation and related functions from monomorphisation.
Brian Campbell
2019-03-06
Add an -ir option to print the intermediate representation of a file
Alasdair Armstrong
2019-03-06
Improve AST slicing
Alasdair Armstrong
2019-03-06
Add option to slice out printing and tracing functions when generating C
Alasdair Armstrong
2019-03-05
Fix missing case in specialization
Alasdair
2019-03-05
More optimizations and improvments for C generation
Alasdair Armstrong
2019-03-05
Coq: use more local type information when constructing tuples
Brian Campbell
2019-03-05
Coq: some debugging messages
Brian Campbell
2019-03-05
Coq: output type-level Int definitions
Brian Campbell
2019-03-05
Additional optimizations for C compilation
Alasdair
2019-03-04
Fix aarch64_small test XML for jenkins
Alasdair Armstrong
2019-03-04
Fix execute splitting to work when constructors have constraints.
Alasdair Armstrong
2019-03-04
Do not store type synonyms as functions in the environment
Alasdair Armstrong
2019-03-04
Add location to warning in pattern completeness check
Alasdair Armstrong
2019-03-01
WIP: Start working on being able to slice single instructions out of specs
Alasdair Armstrong
2019-03-01
Add some tricky test cases for quantified Sail AST types
Alasdair Armstrong
2019-03-01
Coq: some library compatibility changes
Brian Campbell
2019-03-01
Add a test case for previous commit
Alasdair Armstrong
2019-03-01
Fix bug with naturals in quantified constructors
Alasdair Armstrong
2019-03-01
Make Sail more flexible with existentials in union types
Alasdair Armstrong
2019-03-01
Fill in some edge cases in monomorphisation
Brian Campbell
2019-03-01
Coq tidying: remove old definition, complete a pattern match
Brian Campbell
2019-03-01
Coq: make iff `iff`
Brian Campbell
2019-02-28
Handle implicits in destruct_atom_nexp
Brian Campbell
2019-02-28
Coq: Clean up rich boolean handling in backend
Brian Campbell
2019-02-28
Coq: more for informative booleans
Brian Campbell
2019-02-28
Coq: update tyvar merge information at other binders
Brian Campbell
2019-02-28
Turn off some debugging messages
Brian Campbell
2019-02-28
Coq: merge tyvars with corresponding variables
Brian Campbell
2019-02-28
Coq: strip informative bools back to more uniform types
Brian Campbell
2019-02-28
Coq: some work on bool simplification
Brian Campbell
2019-02-28
Allow user-specified state to be passed through generated C
Alasdair Armstrong
2019-02-27
Provide more access to the ELF symbols in the OCaml ELF-loader.
Prashanth Mundkur
[next]