Rafael Sá Menezes

Issues including algorithm with cpp 11

6

The following program is failing with `--cppstd 11` ```cpp #include int main() { return 0; } ``` Fails with: ``` Parsing main.cpp In file included from main.cpp:1: /tmp/esbmc-cpp-headers-88a1-0b31-4ee7/algorithm:1169:12: error: no...

Update the Build Environment for Ubuntu 24.04

11

Since we are having demand for newer solvers and library updates. Let's update our docker image to the recent Ubuntu 23.04. @lucasccordeiro Let me know which solvers are needed. @fbrausse...

This should close #1905. The issue was that this intrinsic was generating the wrong return value, this PR corrects this. I am not adding the same test case from #1905...

ESBMC fails on smmintrin.h

1

The header was fine on version 7.5 and is no longer working since 7.6.0: ```c #include int main() { } ``` Fails with: `ERROR: function must return value` Relevant expression:...

This PR constructs a class to be used as an abstraction of the goto program as a CFG. This can be used for us to apply more classic compiler algorithms...

Push to newer Clang

5

Clang 11 is becoming too old. Shall we move towards Clang 14 (Ubuntu 22.04 LTS) or shall we go to the latest (15)?

Add trivial explicit after-loop invariant in k-induction

4

ESBMC fails to prove the `/loops/trex02-1.c` (from sv-comp) with k-induction: ```c //x is an input variable int x; void foo() { x--; } int main() { x=__VERIFIER_nondet_int(); while (x >...

Remove heap allocation from netrecv_from

8

## Feature Request ### What feature are you suggesting? #### Overview: - Remove the heap allocation from the [netrecv_from](https://github.com/devkitPro/libogc/blob/master/libogc/network_wii.c#L945C2-L945C32 ) method or expose a function that skips the allocation. ####...

HTML output

11

This PR adds support to generate html bug trace by using the flag `--generate-html-report`