Add support for movsx #586
JasonGrosscoq-archlinux.yml
on: pull_request
Annotations
5 errors
|
archlinux
Process completed with exit code 2.
|
|
archlinux
Makefile.coq:818: src/Assembly/Symbolic.v
|
|
archlinux
Makefile.coq:818: src/Assembly/Symbolic.v
|
|
archlinux:
./src/Assembly/Symbolic.v#L4211
In environment
opts : symbolic_options_computed_opt
descr : description
instr : NormalInstruction
stack_addr_size := 64%N : AddressSize
sa := 64%N : AddressSize
s : N
resize_reg :=
fun r : REG =>
some_or
(fun _ : symbolic_state =>
reg_of_index_and_shift_and_bitcount_opt (reg_index r, 0%N, s)%zrange)
(fun _ : symbolic_state => error.unimplemented_instruction instr) :
REG -> M REG
dst : ARG
l : list ARG
src : ARG
l0 : list ARG
v : idx
src_size : N
The term "v" has type "idx" while it is expected to have type "Z".
|
|
archlinux-check-all
Process completed with exit code 1.
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
ExtractionHaskell-archlinux
|
6.29 KB |
sha256:3a7221fbcd3c90faf3bccbcefe559ffafdd2cf9f420f99f30a3492e1b00b7237
|
|
|
ExtractionOCaml-archlinux
|
5.86 KB |
sha256:9b662cc72d72c4eec4fdd5a8f4a54c274b9321d81f46763fb02aed98ca31618e
|
|
|
generated-files-archlinux
|
4.85 MB |
sha256:f0f95307d4ea2f9f8048a6ffb318636fce810d2d040ea337a85866280a180151
|
|
|
timing-files-archlinux
|
1.72 MB |
sha256:f8a1bef78696e204f8a0d87749da35b6a113d0468f2c574d1cd6c25660529695
|
|