| Age | Commit message (Collapse) | Author |
|---|
|
Also fix bug in mono analysis with generated variables
Breaks lots of typechecking tests because it generates unnecessary
equality tests on units (and the tests don't have generic equality),
which I'll fix next.
|
|
|
|
Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard.
|
|
# Conflicts:
# src/lem_interp/interp.lem
# src/lem_interp/interp_inter_imp.lem
# src/lem_interp/interp_interface.lem
# src/parser.mly
# src/pretty_print_lem.ml
|
|
|
|
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
|
|
|
|
|
|
unknown conditions.
Does not merge if one path has resulted in an exit
|
|
|
|
|
|
theorem provers, use structural (in)equality for Isabelle and HOL for literals and values
|
|
being very power-specific.
Note: slight interface change to instruction_extractor
|
|
|
|
Also fix type checker bug in not reporting modifications to parameter values
|
|
increasing while supporting inc and dec views to the interpreter and in printing
Fix bugs exposed by running idlarm several instructions (after fixing above)
|
|
Split out specification specific memory and external functions
Reduce the presence of big_int
Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction
Also some bug fixes exposed by above and running ARM second instruction
|
|
and I *think* that I'm making vectors of unknowns in all the necessary places now.
|
|
|
|
|
