Michael Petter

Strange overflow behaviour

4

The following issue popped up when doing intensive sv-comp tests: ```c //SKIP PARAM: --enable ana.int.interval --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none int a; int main() { a = 5; a...

SV-Comp incorrect result in no-overflow tasks

1

Straight from `no-overflow`  on `ldv-regression/test_overflow.i` ; we are not flagging any overflow here. ```c #include #include void __blast_assert() { ERROR: {reach_error();abort();} } ssize_t getService(); int globalSize; int main(int argc, char*...

Both branches dead in char_generic_nvram_read_nvram_write_nvram.i with octagon enabled analysis

5

The following popped up when doing extensive benchmarking, so by creduce we get: ```c //SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain octagon --set sem.int.signed_overflow assume_none #include #include long *a; pthread_t...

This is intended to become a proposal PR for #1459 , exploring if we can come up with performance improvements by switching to sparse representations for affine equalities.

Setting up a post-analysis count of the share of elements in a matrix that are equal to 0, we come to the following histogram:  - the x-axis is the...

Housekeeping relational analyses

8

During #1412 we encountered several legacy problems in the current state of relational analysis, in `relationDomain.apron.ml` and `sharedFunctions.apron.ml` to be taken care of in some PR: - [x] `relationDomain.apron.ml` module...

Narrowing gas

6

Closes #1494 by providing a domain lifter, that applies ```meet``` until the gas depletes. In a first application, we get a new parameter ```ana.apron.narrowing_gas``` to specify the amount of gas...

Essentially we implement [Podelski/Rybalchenko](https://www.cs.cmu.edu/~hzarnani/fm-rg/cmuonly/podelski04complete.pdf)

sparseOctagons: a new sparse implementation of Miné's Octagons

1

This PR is for experimenting with a re-implementation of [Miné's Octagons](https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf) in Ocaml with a focus on sparsity. For now we are just interested, how this re-implementation does perform in...