Raphaël Monat

Use `dates_calc` library

1

This is a WIP. Current version 0.0.2 of `dates_calc` is in the process of being published, so I guess the CI should fail currently. - [ ] Test current implementation...

When are shortcuts taken into account?

3

Hi, I've been using `cvise` for a few weeks now and must say it's been extremely helpful, thanks a lot for developing it! I have a question regarding the `S`...

Integer division of `n/d` where `n = [-1, 1], d = -1` yields bottom

4

Originally encountered by @svenkeidel, I'm providing an OCaml MWE. We found that integer division of `n/d` yields bottom when `-1

Following a [discussion](https://gitlab.com/mopsa/mopsa-analyzer/-/merge_requests/172#note_1675805572) with @jboillot in the Mopsa static analyzer, I believe `bound_texpr` could be more precise. Consider the case where `x >= y` and `z >= 0`. Currently, `bound_texpr`...

Let us consider this simple program: ``` int m = rand(2, 9); int y = rand(0, 2020); int y2 = y + ((m + 1) / 12); ``` The relational...

Is there a way to have precise assignments on PPL Grid?

1

I'd like the assignment `m = n % 12` to be handled precisely by `assign_texpr` in the PPL Grid domain. It currently does not work precisely, while a similar code...

I tested an assignment creating an overflow in Elina's internal representation, starting from top. The polyhedra domain signals an overflows and returns top. However, the octagon domain does not appear...

Unexpected bottom after meeting constraints using elina_poly

1

I have an edge case were adding constraint `x - (-9223372036854775808) >= 0` and then adding constraint `-9223372036854775808 - x >= 0` yields bottom for elina_poly, which is unsound. Would...

REPL demo

4

Hi, I would like to run a demo in a REPL, such as the interactive python shell. My issue is that `pe` will wait for the end of the current...

Concolic testing engine

3

This contains the work of @pierregoutagny done during his internship. I spent a few hours merging with master, I'm opening a PR to track upcoming breaking changes.