Mikhail R. Gadelha

A quick look at these and it seems only the one in goto-programs/goto_sideeffects.cpp is worth checking out: we create a new symbol for the return of a function_call, but I...

Well, the sanitizers don't complain about it

Oh I see, I was not calling the binary with the arg On Tue, 19 Dec 2023, 20:28 Franz Brauße, ***@***.***> wrote: > This is independent of string literals, though:...

Can't we just delete them?

My first suggestion is to check what cbmc does... Also, how do we handle virtual inheritance? Is `A` marked somehow? Do we inherit its member variables more than once in...

and what exactly is the error? I can't get esbmc to verify it with the ToT: ``` $ esbmc main.cpp ESBMC version 7.1.0 64-bit x86_64 linux Target: 64-bit little-endian x86_64-unknown-linux...

why A's member isn't initialized? Em ter., 21 de mar. de 2023 às 10:06, KSong ***@***.***> escreveu: > and what exactly is the error? > > It should be verification...

And why are B's and C's constructors are not responsible for constructing A, since the constructors that take x as argument call A?

I guess you have the answer for your algorithm then :) What's preventing you from implementing the rules you just explained? Em ter., 21 de mar. de 2023 às 10:44,...

Reduced test-case: ``` a, c; double b = 63.75; main() { while (1) { if (b < 1.85) a = 6; b = c = b < 1.85 ? a...