esbmc
esbmc copied to clipboard
esbmc
The efficient SMT-based context-bounded model checker (ESBMC)
`member_call.getType()` does not take into account references. Just as is done for [CallExpr](https://github.com/esbmc/esbmc/blob/80c4e3b48bbd7bdf7ceb7b58d2458e68ddc917f7/src/clang-c-frontend/clang_c_convert.cpp#L1781) and [CXXOperatorCall](https://github.com/esbmc/esbmc/blob/80c4e3b48bbd7bdf7ceb7b58d2458e68ddc917f7/src/clang-cpp-frontend/clang_cpp_convert.cpp#L650), we use `getCallReturnType` instead. Before: ``` struct a * return_value$_e$1; // 27 no location FUNCTION_CALL:...
While investigating https://github.com/esbmc/esbmc/pull/2003#issuecomment-2314559356 I reduced the test case to something like this: ```cpp #include #include char *a = new char; int main() { 0 == realloc(a, 0); a[0] = 'a';...
```cpp #include struct aaaa { int a; int b; }; int main() { void *foo = operator new(8); // void *bar = new char; // void *aaa = malloc(sizeof(char)); //...
When the `true` and `false` expressions in the conditional operator are `string` type, we need to cast them to pointer types. This happens in AST when both StringLiterals are of...
While trying esbmc on a small code on windows ```c #include #include int main() { // Declare a string variable std::string inputString; // Prompt user for input std::cout
I've built ESBMC on Fedora successfully and I've noticed there are 2 libraries which are not specified to be linked causing the build process to fail. * maths (-lm) *...
This PR adds the flag `--goto-ssa-promotion` which will introduce phi-nodes into the goto program for all program variables. It consists in: 1. Computing dominator information about the CFG. 2. Computing...
In `merge_goto`, it seems that the `cur->state.guard` is updated in the wrong place. See below codes. ```c++ void goto_symext::merge_gotos() { ... for (auto list_it = state_list.rbegin(); list_it != state_list.rend(); list_it++)...
The test cases come from https://github.com/esbmc/esbmc/issues/397, this issue was fixed by using a global guard to prevent assertions from being executed https://github.com/esbmc/esbmc/pull/399. But this fix comes with another problem: assertions...