Maxime Derri
Maxime Derri
It appears that the precision has decreased compared to previous versions that did not use a separated domain for types. I observed a case where, for the same program, type...
I encountered a case where the widening operator returns an empty abstract state (bottom), leading the verifier to loop indefinitely. A test is provided [ex_widening.zip](https://github.com/user-attachments/files/23799972/ex_widening.zip): - section: xdp - function:...
The instructions of each function are stored in a single instruction vector, which is passed as a parameter to from_sequence. Initially, a basic block is created for each instruction. Then,...
The WTO is computed both during the CFG computation (in case loop counters are inserted into Bourdoncle components) and before generating pre- and post-invariants. When loop counters are inserted in...
Assertions are computed during CFG computation, but they are only used for printing and checking pre-invariants. They remain stored in memory until PREVAIL terminates. They could be generated only when...
Compared to the Linux verifier, which distinguishes between global functions (verified once) and static functions (verified at each call), PREVAIL verifies all subprograms at every call. This is more precise,...
Improving execution time and memory consumption of invariant computation and assertion verification
In this issue, I discuss possible ways to enhance the performance of invariant computation and assertion verification. 1) In recent versions, PREVAIL has been updated to verify assertions during the...