Re: [RFC PATCH 2/4] xen/arm64: bitops: justify uninitialized variable inside a macro

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

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 <julien@xxxxxxx> 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)