Martin Karup Jensen

Anomaly as a result of extraction in CertiCoq (assertion fails in ml code)

13

I apologize if this is not the right place to report this, I admit I haven't investigated it thoroughly. Using the [CertiCoq project](https://github.com/CertiCoq/certicoq) to try to extract the parsing of...

wasm-opt -O2 seg faults on large binary with many nested if-then-else instructions

1

I have a somewhat large binary (1.9 mb) that contains a function with a lot of nested if-then-else instructions, and running `wasm-opt -O2 --enable-tail-call --enable-mutable-globals --output ` causes a segmentation...

Too many local (according to nodejs) in generated Wasm module

1

I have some C code generated through the [CertiCoq project](https://github.com/CertiCoq/certicoq), specifically a verified implementation of sha256. Emscripten produces a Wasm module that contains a function that fails when trying to...

Generated Wasm module fails with "stack overflow" / "memory access out of bounds" (nodejs runtime error)

1

I have some C code generated through the [CertiCoq project](https://github.com/CertiCoq/certicoq). Emscripten produces a Wasm module that fails with a stack overflow/ memory access out of bounds runtime error when trying...

Behavior differs from x86-64 binary

1

I have some C code generated through the [CertiCoq project](https://github.com/CertiCoq/certicoq) and the behavior (printed result) of running the Wasm module via the generated js scaffolding (w/ node v.20.12.2) differs from...

Question: Compiling to OCaml byte code?

7

Is it possible to use malfunction to compile a .mlf file to OCaml byte code?

wasm-opt segmentation fault with, but not with --debug

1

I have a binary wasm file demo1 [(zipped here)](https://github.com/WebAssembly/binaryen/files/15373320/demo1.zip). If I use the binary of binaryen/ `wasm-opt` available on the releases page, version 117, and I call ``` wasm-opt -O2...

Bugs in implementation of primitive operations

1

I'm aware that the primitive operations are not verified, but I believe that there are some bugs in the C code for the Coq primitive `Uint63` operations (in `plugin/runtime/prim_int63.c`) The...

Possible discrepancy between wasmcert and official webassembly specification

1

I have found something that might have been missed in the WasmCert-Coq mechanization related to left/ right shifts. In the official WebAssembly spec (both 1.0 and 2.0), the left/ right...

Remotely spawning a process on an untrusted node when in a sensitive context causes a javascript runtime error. ## Small example Code for `node1`: ```sml let fun foo () =...