General

Profile

Grigoriy Volkov

Issues

Projects

Activity

06/05/2018

01:19 AM Deductive Verification Tools for Linux Kernel Revision 67eb461b (framac): Check return type in substitutions
01:18 AM Deductive Verification Tools for Linux Kernel Revision b22c7ba7 (framac): Disallow abrupt termination for lemma-functions

05/24/2018

05:05 PM Deductive Verification Tools for Linux Kernel Revision 3bee33e9 (jessie2): Fixes for compatibility with Frama-C changes

05/14/2018

09:57 PM Deductive Verification Tools for Linux Kernel Revision 0fd06d88 (framac): Set location in included lemmas
03:33 PM Deductive Verification Tools for Linux Kernel Revision 7b8fa69e (framac): Register lemmas

05/11/2018

04:45 PM Deductive Verification Tools for Linux Kernel Revision 623b8d0b (jessie2): Compatibility with abstract lemmas
04:44 PM Deductive Verification Tools for Linux Kernel Revision eda7e02f (jessie2): Fix typing error/warning
04:41 PM Deductive Verification Tools for Linux Kernel Revision bb7d3320 (framac): Implement 'abstract lemma' / 'abstract axiom'
The abstract keyword makes it change between lemma/axiom on inclusion.

05/09/2018

06:12 PM Deductive Verification Tools for Linux Kernel Revision 1d28c1f8 (framac): Do the logic var use substitution correctly (fixes AST Integrity Check)
vlogic_info_use is what we *want*, substitute the whole thing there.
vlogic_var_use is required to prevent the caller...
04:43 PM Deductive Verification Tools for Linux Kernel Revision 7f9e2a36 (framac): Save funcs/preds with substitutions applied into a separate list
Instead of keeping renamed copies in the destination axiomatic

Also available in: Atom