extraction to C of function without argument
When extracting the following to C
type t = { mutable a : bool }
let g () = { a = true }
type u = { b: t }
let f () = { b = g () }
(for instance with command line why3 extract -D c --modular test.mlw -o .
) we get a C code where
f is not a function anymore:
...
struct t f = g();