search

AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
21 stars 1 forks source link

Constant multidimensional array #15

Closed franziskuskiefer closed 3 months ago

franziskuskiefer commented 3 months ago

Constant multidimensional arrays can't be extracted.

const TABLE: [[u8; 1]; 1] = [[1]];

The following however, works.

const V: [u8; 1] = [1];
const TABLE: [[u8; 1]; 1] = [V];

See the changes here

https://github.com/cryspen/libcrux/commit/a84d517beea0b7917385b41367e495c869549496#diff-09cfc883c6f418b0a41211e39ad4ff0f5f1d2bbfbcc970667007eadc8353fec3R7