Lucas C. Cordeiro

[counterexample] missing assignment to the function parameters

11

Consider the following C program: ````C #include void foo(unsigned int x) { x++; if((10 * x - 1) == 1001) assert(0); } ```` If we call ESBMC as $ esbmc...

An ESBMC user asked whether we can change how we print our messages to the output. In particular, this user claims we should output our messages to the stdout instead...

[Coverage] Assertion Instances Coverage: 1100%

2

$ esbmc main.c --assertion-coverage --unwind 10 ````C #include int main () { int a , x , y = 0 , z; a = nondet_int(); x = nondet_int(); z =...

[Coverage] ESBMC does not generate test case with coversBanch="true"

2

$ esbmc foo.c --branch-coverage --generate-testcase ````C #include int a; void foo(int x) { if (x > 7) a = a*4; printf("a: %i", a); } int main() { int x =...

````CPP #include #include #include void testCreateUniquePtr() { std::unique_ptr ptr = std::make_unique(10); assert(ptr != nullptr); // Check that the pointer is not null assert(*ptr == 10); // Check that the value...

[Vector OM] error: no matching constructor for initialization

3

````CPP #include #include #include #include // Define a struct for User (equivalent to interface in TypeScript) struct User { int id; std::string name; std::string email; bool isAdmin; // Since C++...

[Python library] Reintegrate the Python API to call ESBMC's functions

2

@mikhailramalho: Do you remember the commit where you removed the Python API developed by @jmorse in ESBMC? @brcfarias needs to have this back to ESBMC.

[HTML Report] std::filesystem::__cxx11::filesystem_error

1

$ esbmc fuzzing.py --incremental-bmc --compact-trace --generate-html-report ````Python a : int = nondet_int() x : int = nondet_int() y : int = 0 z : int = nondet_int() if a >...

From https://github.com/esbmc/esbmc/pull/1944: > You probably don't need to pass the cmd.options_map, as optionst already reads all the data in that map and fills it's own option_map > Please follow the...

```` $ esbmc teste2.py ESBMC version 7.6.1 64-bit x86_64 linux Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc Parsing teste2.py Converting Loading model: range.py Loading model: int.py terminate called after throwing an...