Rafael Sá Menezes
Rafael Sá Menezes
We need a list of every intrinsic function that we have and how to use it. This would be useful for users and developers.
This PR will optimize memset operations by initializing the entire object with the result of the memset. This should avoid unrolling and speed up for memset of known bounds. Closes...
This PR should close #652 The idea here is mainly to provide users with a stable way to use our intrinsic functions. As discussed in the issue this can be...
The definition of `SOFTFP` was preventing `fenv.h` to be parsed correctly. Although this is a fix for M1, it should be fine on every macOS.
AFAIK we do not have any plans on adding XML output.
ESBMC options have grown a lot. We could have an input configuration file (such as config.json) which sets all the options and architectures for users.
The above is for the large array https://github.com/esbmc/esbmc/blob/c7191cda390244cabca0285d0c41a7ad2ffa673e/regression/esbmc/github_732-2-2/main.c Other solvers do the `--smt-formula-only` much quicker and with less memory: - Boolector 7.2s 144M - CVC4 0.77s 152M - Yices 7.1s...
Currently, there is no proper way to add globals in ESBMC. And some of those could even be removed. I propose: 1. Creating a singleton to hold global objects; 2....
Following the discussion from #755 The main idea is: 1. Config will still be global 2. Configt will hold: message state, command-line and architecture. 3. Add support to a configuration...
Right now is very hard to check (and understand) the symex flow. We should backport some of the CBMC tests here.