summaryrefslogtreecommitdiff
path: root/src/lem_interp/run_interp_model.ml
diff options
context:
space:
mode:
authorThomas Bauereiss2018-02-01 17:57:36 +0000
committerThomas Bauereiss2018-02-01 18:01:20 +0000
commita2d505a0e7e01efbfd24cacc6ea0f74918ba31f8 (patch)
tree9be75ac5376ba02bc6fae67b49c3ef4742a780b0 /src/lem_interp/run_interp_model.ml
parentc7e8709e3de85d398ee9fa99317defd8c6a2756b (diff)
Comment out special casing of execute function in Lem pretty-printer
It assumes that execute is non-recursive, which is not the case for RISC-V with compressed instructions. Splitting execute into different auxiliary functions for each clause is probably still useful, as Isabelle is likely to parse many small functions faster than one big (potentially recursive) function, but this splitting should be done in the rewriter instead of the pretty-printer, in order to properly deal with recursion.
Diffstat (limited to 'src/lem_interp/run_interp_model.ml')
0 files changed, 0 insertions, 0 deletions