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

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 16/07/23 18:50, Julien Grall wrote:
> Hi,
>
> On 16/07/2023 10:20, Luca Fancellu wrote:
> > > On 14 Jul 2023, at 14:05, Julien Grall <julien@xxxxxxx> wrote:
> > >
> > > Hi,
> > >
> > > 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.
> > Hi Julien,
> >
> > Yes I agree that it’s strange, do you think that that if at line 97 we 
> > initialize oldbit to zero, it would solve the issue?
> At the moment, I am not entirely happy to zero oldbit because we have 
> other places in Xen where we need assembly instructions to read a value 
> (e.g. READ_SYSREG()).
> So I would first like to understand why Eclair can't cope with it.
>
> Cheers,
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)