doubtful placement of attributes when introducing proxy symbols
Consider the small code below
val ref x : int
let f () = [@attrib] x <- 0
val g (x:int) : int
let h () = x <- [@attrib] g 0
when visualising the internal modules using
why3 prove --debug=print_modules,print_attributes f.mlw
one can see that the attribute [@attrib]
is placed inside the let
introducing proxy symbols:
[...]
let o [@mlw:proxy_symbol] = 0 in
[@attrib] (x [@mlw:reference_var]:ref int).contents <- o
[...]
let o [@mlw:proxy_symbol] = let o1 [@mlw:proxy_symbol] = 0 in
[@attrib] g o1 in
(x [@mlw:reference_var]:ref int).contents <- o
Is it intentional to put the attribute after the introduction of the let o ...
and not on the let o ...
expression itself?
For information, the impact is visible when using bddinfer: the abstract state computed before the statements annotated by [@attrib]
contains a value for the proxy variable, which is meaningless "before" the statement in question.
Changing that could have an impact elsewhere though, e.g. on CE generation. Investigation and clarification needed.