| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
build_context val spec which was out of dated although lem did not complain for some reason...
|
|
|
|
|
|
|
|
|
|
Footprint exhaustive evaluation fixes
Approved-by: Jonathan French <me@jonathanfrench.net>
|
|
|
|
exiting due to one of them being unknown; fixes incorrect exhaustive analysis for footprints
|
|
node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node
|
|
|
|
|
|
|
|
|
|
|
|
overflow.
|
|
xml for jenkins.
|
|
Library in need of rationalisation.
|
|
dubious types but will wait for library rationalisation to fix.
|
|
to ocaml version. TODO: also fix copies in sail_values.lem and sail_values_word.lem.
|
|
|
|
|
|
have correct rounding behaviour. Missed these when changing quot and mod functions.
|
|
|
|
optimisation went wrong.
|
|
|
|
|
|
handling unsealed capabilities by clearing tag and setting cursor to -1. Also CCSeal got an encoding.
|
|
performance bug or infinite loop. Add some missing shallow embedding funcitons.
|
|
|
|
trucation towards zero. Previous version was incorrect if result was exact and a<0 and b>0.
|
|
|
|
comparison instead of unsigned.
|
|
instead of using magic value if unsealed. Also corresponding CCSeal instruction which degrades to a cmove if ct.tag is unset.
|
|
|
|
|
|
|
|
|
|
that uses the new Lem machine words library.
|
|
|
|
Instead of abusing patterns as expressions, bind patterns to names (if they are
more complex than an identifier or literal and don't have a name already) and
generate expressions referring to those names (which we then pass as arguments
to the auxiliary functions).
|
|
Before, wildcards sometimes ended up in the arguments to the function call on
the RHS, in particular when using vector patterns (which implicitly introduce
wildcards for the order and index parameters).
|
|
|
|
|
|
|
|
|
|
that cb is not sealed as per ISAv6.
|
|
|
