General

Profile

Mikhail Mandrykin

Issues

Projects

Activity

12/05/2019

03:15 PM Deductive Verification Tools for Linux Kernel Revision cfe407fa (astraver): Proper behavior renaming -- tentative!
Mikhail Mandrykin
02:04 PM Deductive Verification Tools for Linux Kernel Revision 97291933 (astraver): Fix benavior renaming (avoiding keyword clashes): should not do functional updates as this causes inadvertent re-registration of properties!
Mikhail Mandrykin

11/18/2019

02:50 PM Deductive Verification Tools for Linux Kernel Revision 8ded7349 (framac): Exposed option -print-cil-as-is as a command line flag
Mikhail Mandrykin

11/15/2019

09:41 PM Deductive Verification Tools for Linux Kernel Revision 18b9546c (framac): Removed implicit -print-cil-as-is from -print-lines option (assuming it is the desirable behavior)
Mikhail Mandrykin
09:40 PM Deductive Verification Tools for Linux Kernel Revision 9daea0b5 (framac): Added option to minimize initializers by relying on implicit initialization
Mikhail Mandrykin
06:31 PM Deductive Verification Tools for Linux Kernel Revision 2d014831 (framac): Lift additional restriction on function pointer type casts
Mikhail Mandrykin

11/01/2019

06:20 PM Deductive Verification Tools for Linux Kernel Bug #9894 (Resolved): Frama-C (CIL) cannot represent an integer
Changed integral type selection for constants when in GCC compatibility mode (@-machdep gcc_x86_@*) (commit "c0d393e8... Mikhail Mandrykin
06:02 PM Deductive Verification Tools for Linux Kernel Feature #9895 (Open): Disabling single exit point
Added an experimental option "@-no-single-return@" that disables single-return transformation in commit "df584314":ht... Mikhail Mandrykin
05:53 PM Deductive Verification Tools for Linux Kernel Revision df584314 (framac): Added -no-single-return option to disable Oneret transformation (to be used in the Klever setting with possibly no plugins involved)
Mikhail Mandrykin

10/28/2019

06:59 PM Deductive Verification Tools for Linux Kernel Revision c0d393e8 (framac): More GCC compatibility in treating large integer constants
Mikhail Mandrykin

Also available in: Atom