Boris Yakobowski
Boris Yakobowski
The current state of `master` does not compile on my Windows environment. Here is the patch that I had to apply ``` diff --git a/src/dune b/src/dune index 01bf123..f36bc09 100644 ---...
Yes I'm compiling with Mingw. And you're right of course, the change in the dune file must be conditional. I will try to refine it.
We noticed the same thing here, and have an alternative patch. I will try to compare the two approaches, and report there.
Fixup commits merged, as discussed.
Thanks for the info! As it happens, we are trying to merge to last-week's main branch 😅 . (And so we did not see this commit.) I will check whether...
The changes in `/biabduction` are only in `Errdesc`, to capture cases where a closure was used instead of a regular function. So it should be very safe. But we have...
Note that we will of course fix the merge conflict(s) if you are interest in the patch.
I would suggest you think twice about implementing this. This is basically what Frama-C/Value used to do for trace partitioning and loop unrolling, under the name `-slevel`. The argument of...
I can confirm that this kind of code would trigger the equality domain of Frama-C/Eva. We are also helped by the fact that we control our front-end (which would not...
Hi Maxime, I forgot to answer to this message, sorry about that. The equality domain of Eva is in `src/plugins/value/domain/equality`. Feel free to ask high-level questions, I should still be...