Mikhail R. Gadelha
Mikhail R. Gadelha
> So I was just taking a look at this for you, and I noticed this: > > * [`getBVInt`](https://github.com/stp/stp/blob/master/lib/Interface/c_interface.cpp#L1607) calls `GetUnsignedConst` > * [`getBVUnsigned`](https://github.com/stp/stp/blob/master/lib/Interface/c_interface.cpp#L1621) calls `GetUnsignedConst` > > The...
Em seg., 23 de ago. de 2021 às 16:18, Daniel-yrm ***@***.***> escreveu: > Hey Daniel, we can actually improve the implementation by not using models > at all: since these...
> Also studying some basic concepts used in model checkers implementations. Anyway, I have some questions on it. > - I saw that some of the functions in symex_main.cpp are...
Are the new wrong results a result of the patch or is it noise? Are the new unknowns crashes or timeout? On Mon, 9 May 2022, 08:40 Rafael Sá Menezes,...
> The difference between signed and unsigned overflow is that according to the C standard unsigned overflow is defined as wrap-around while signed overflow is undefined behaviour (UB). And compilers...
Em qua., 29 de jun. de 2022 às 10:22, Franz Brauße ***@***.***> escreveu: > Does ESBMC support input files from different languages at the same time? > Not really. >...
@rafaelsamenezes could you test that on the 2 memory categories: valid-memcleanup and valid-memsafety. You could use the same parameters of the try-runs: 90s, 7GB.
I'm not a big fan of ini files, how about yaml?
Toml looks like ini... Anyway, let's not waste more time with this discussion, toml seems more expressive than ini, so I'm fine with it. Em qua., 13 de jul. de...
I wonder if we can simply the implementation by using concats + bitcasts. On Wed, 16 Feb 2022, 08:29 Fedor Shmarov, ***@***.***> wrote: > ESBMC uses intrinsic memset implementation (__ESBMC_memset(ptr,...