Adapted islaris to the latest isla and to the (currently under review) latest isla-lang #25
Conversation
…ems-project-main
… values produced by the new isla-footprint - Changed Makefile instructions for coq-bbv for `make deps`: use coq-bbv.1.4 instead of 1.3 and install via opam
Update README instructions
.github/workflows/ci.yml
Outdated
| @@ -22,7 +22,7 @@ jobs: | |||
|
|
|||
| env: | |||
| OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda" | |||
| OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc" | |||
| OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://github.com/ric-almeida/isla-lang.git" | |||
There was a problem hiding this comment.
I assume this is just pinning to same comment as the linked PR for isla-lang? We should make sure to change this back when that's merged.
There was a problem hiding this comment.
Yes, it's linking to the same commit. I'll update it once it's merged.
| | Ast.AbstractPrimop(r,v,args,a) -> | ||
| pp "AbstractPrimop %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a | ||
| | Call (_, _) -> () (* TODO: fill in here? *) | ||
| | Return (_, _) -> () (* TODO: fill in here? *) |
There was a problem hiding this comment.
Probably we should output the Coq constructors for these and filter them somewhere else if we don't want them, but it's not very important.
frontend/decomp.ml
Outdated
| @@ -84,7 +84,7 @@ let event_filter : Arch.t -> int -> event -> bool = fun arch i e -> | |||
| | Smt(Assert(_), _) -> i = 0 | |||
| | Cycle(_) | |||
| | MarkReg(_, _, _) | |||
| | Smt(DefineEnum(_), _) -> false | |||
| | Smt(DefineEnum(_,_,_), _) -> false | |||
There was a problem hiding this comment.
Maybe we should be retaining this now that it contains a little useful information? (With nop operational semantics, presumably)
There was a problem hiding this comment.
Ok. We're not using this now, but I've set this to true now in case we will use it in the future.
But in general I open the PRs after checking that they're building. Thanks for reviewing. |
To be reviewed in combination with this PR on isla-lang: rems-project/isla-lang#10