Rafael Sá Menezes

We should have the option to print some statistics during the run. Those statics could include: - Number of simplifications - Number of GOTO loops - etc... We could then...

ESBMC fails with the following program: ```c #define PRESENT 0x01 #define _4KB 0x1000 #define _32KB 0x8000 #define _4KB_MASK (~(_4KB - 1)) #include #define UINT32 unsigned long #define UINT64 unsigned long...

Casting pointer through integer fails

4

The following program: ```c #include #define _4KB 0x1000 #define _32KB 0x8000 #define _4KB_MASK (~(_4KB - 1)) #define UINT32 uint32_t #define UINT64 uint64_t void Test() { void *Heap = __ESBMC_alloca(_32KB); __ESBMC_assume((UINT64)Heap...

ESBMC does not use message system for verbose clang

1

When esbmc on this branch is run with `--verbosity 7` (to enable debug output), we currently pass the flag `-v` to clang resulting in output to stderr, which should probably...

Add an attribute to not cut a variable during slicing

4

Tracing the counter example back is not always easy. Some users want to be able to use some intermediate variables to understand the flow better. One suggestion was to create...

This PR intend to add caching for matching and simplifying expressions that were already seen (in the same formula). For example, the program: ```c int main() { int a,b,c; //...

This is the first algorithm for the canonization (normalization and renaming are missing for now) process of expr2t, which is based on this [paper](https://dl.acm.org/doi/abs/10.1145/2393596.2393665). The idea is that given an...

# Description Closes #45 - More info on the issue

**Is your feature request related to a problem? Please describe.** FuseBMC is trying to use map2check to create coverage for C programs. However, its targets consists in functions named GOAL_N...

# Description This adds an option to specify a nondet-generator. If the flag is not set then the combination will be used. Closes #43 ## Type of change - [X]...