Set array sizes from bounds #599
coq-archlinux.yml
on: pull_request
Annotations
5 errors
archlinux:
src/Assembly/EquivalenceProofs.v#L1007
Cannot infer the implicit parameter bytes_per_element of
build_merge_array_addresses whose type is "N" in
environment:
build_merge_base_addresses_G :
symbolic_options_computed_opt ->
description ->
bool ->
list (idx + list idx) -> list REG -> list Z -> G.M (list (REG + idx + idx))
opts : symbolic_options_computed_opt
descr : description
dereference_scalar : bool
items : list (idx + list idx)
reg_available0 : list REG
runtime_reg0 : list Z
s : idx + list idx
xs : list (idx + list idx)
idxs : list idx
r : REG
reg_available : list REG
rv : Z
runtime_reg : list Z
base : idx
|
archlinux
Makefile.coq:818: src/Assembly/EquivalenceProofs.v
|
archlinux
Makefile.coq:818: src/Assembly/EquivalenceProofs.v
|
archlinux
Process completed with exit code 2.
|
archlinux-check-all
Process completed with exit code 1.
|
Artifacts
Produced during runtime
Name | Size | Digest | |
---|---|---|---|
ExtractionHaskell-archlinux
|
6.29 KB |
sha256:b93e70ccba3f2425de74b403d2b04f2688d9fe354c29f182d1fc9810520d0018
|
|
ExtractionOCaml-archlinux
|
5.86 KB |
sha256:89d8b0fd17f079db55bb347aba7a46d028a3186f75a28d8bef43f87d80f07ce7
|
|
generated-files-archlinux
|
4.88 MB |
sha256:a3990a2dea7454cafdf5de94a9ac6d4ecc3f0ee97b12ec40167c89ecfc6329cf
|
|
timing-files-archlinux
|
1.8 MB |
sha256:648df5690749e4e351abcf878af83bc830265999408c98cc7248d524e7bc06b1
|
|