Rafael Sá Menezes

Activated IPO optimization globally

4

This should add `-lto` flags to all targets. Closes https://github.com/esbmc/esbmc/issues/125

Contributing

1

This PR will add some rules for contributing to ESBMC Closes #502

This PR is for issue #718 # TODO: - [ ] Create a classification system for every internal assertion - [ ] Scope based assertions (look at the issue)

Pointer arithmetic for non-pointer operands

7

This PR should close #695

Running `esbmc file.c --no-pointer-check --no-slice` fails on the following C code. ```c #include #include #include typedef struct { int raw; } struct1; typedef struct { uint64_t struct1_ref; } struct2; void...

Fix Z3 build with the Ubuntu APT packages

5

The String that comes from Z3_VERSION on apt is different from the pre-built packages. This also sets the arm debug build to use the version from the system.

This should close #481

Caching Infrastructure

1

Note: This is the same as the old PR, but it was simpler to recreate it than to to rebase everything This PR isn't a full-blown caching framework implemented, just...

We need a way to disable groups of assertions during a flow, e.g. initialization. This could make users skip verification of code parts (specially initialization). I was thinking of something...

Print "alive" messages during Decision Procedure

1

Some users are asking for ESBMC print a message during long decision procedures (e.g. 24h) so that they know that it is still working properly. I think we can: 1....