On 17/07/23 16:06, Jan Beulich wrote:
On 17.07.2023 14:16, Nicola Vetrini wrote:
On 16/07/23 18:50, Julien Grall wrote:
On 16/07/2023 10:20, Luca Fancellu wrote:
On 14 Jul 2023, at 14:05, Julien Grall <jul...@xen.org> wrote:
On 14/07/2023 12:49, Nicola Vetrini wrote:
The macro 'testop' expands to a function that declares the local
variable 'oldbit', which is written before being set, but is such a
way that is not amenable to automatic checking.
The code is pretty straightforward. So I am not entirely sure why
Eclair is not happy. Is it because the value is set by assembly code?
Exactly. The reason why I didn't just state that oldbit is always
written or never read before being written in that function is that I
was unsure about the meaning of the assembly.
So I'm pretty sure the tool wouldn't take apart the string literal passed
first to the asm(). Instead I expect it goes from the operands specified,
which for oldbit is "=&r". There's nothing conditional here, so if the
tool didn't trust that outputs are written, it would need to flag such an
issue on about any asm() having outputs.
I hope the issue isn't that the tool doesn't properly deal with the
do/while.
In any event: I may misremember earlier discussions, but isn't this a
pretty obvious false positive? In which case didn't we mean to flag
those as such (because really an improved checking tool could avoid them)?
Jan
Actually, given that the function indeed always writes oldbit in the asm
instruction, I can state that this post-condition holds for the function.
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)
