secure-compilation / SECOMP

SECOMP formally secure compiler for compartmentalized C programs (based on CompCert)
Other
6 stars 2 forks source link

`printf` displaying `<missing argument>` with `-interp-dasm` #5

Closed catalin-hritcu closed 4 months ago

catalin-hritcu commented 5 months ago

In the ASM interpreter (-interp-dasm), printf displays <missing argument> instead of the actual data to be printed. This is related to printf being a variadic function.

jeremyThibault commented 4 months ago

@AndrewTolmach pointed me to a location in C2C.ml where the signature in calls to printf is modified when interpreting.