Mikhail R. Gadelha

Folks, alloca **can** lead to unsafe memory accesses. See: ``` mgadelha@labtop ~ $ cat main.c #include #include #include char *foo(size_t buf_size) { char *buffer; buffer = (char *) alloca(buf_size); memset(buffer,...

How about we use a global variable? From the documentation, we are not allowed to free the get_env return string anyway. Em qui., 3 de ago. de 2023 às 11:58,...

> That could work for `get_env` but the main use case is for users having to initialize structs and buffers in their harness. I see. ~ @lucasccordeiro and @fbrausse given...

> Another one: > > https://github.com/esbmc/esbmc/blob/589b1880df82014034c249ad6a9ede9928173ed6/src/goto-programs/builtin_functions.cpp#L36 > > It smells like a bug but I don't understand the function it's inside of. Yeah, this looks wrong

> According to the git history the two functions get_alloc_type_rec() and get_alloc_type() have been there since the beginning. Anyone has a clue what they're supposed to do? IIRC, this is...

> Hi, > > Sorry it's taken a while to get back to you. I have a theory as to what the problem is. My guess is that valgrind is...

Interesting work! Any reason why use_count is no longer atomic? I guess is not a problem currently since we fork the process instead of using threads in k-induction parallel

what about that witness validator that compiled the test + witness into a program? Does it validate our cex? Is it still participating on sv-comp?

Nitwit is part of sv-comp 24, right? On Thu, 16 Nov 2023, 19:30 Franz Brauße, ***@***.***> wrote: > @fbrausse : are you going to submit a PR for > this...

I don't think we generate return_value___VERIFIER_nondet_double assignments; IIRC this was introduced in cbmc to handle variable lifetime checks, which we solved in a different way. I don't think we generate...