General

Profile

Grigoriy Volkov

Issues

Projects

Activity

08/10/2018

05:54 PM Deductive Verification Tools for Linux Kernel Revision bba3a153 (framac): Add support for declaring logic variables in C
+ fix error related to ALogicType pattern match
Making a temporary variable and using 'assume' with it allows e.g.
l...
05:54 PM Deductive Verification Tools for Linux Kernel Revision 24684d95 (framac): Untrack more aorai generated configs
05:05 PM Deductive Verification Tools for Linux Kernel Revision c66f4188 (jessie2): Add support for 'assume' pragma
05:04 PM Deductive Verification Tools for Linux Kernel Revision 0d22c0ad (jessie2): Add support for using logic types in C (lemma) functions
By extracting from LType annotation
05:03 PM Deductive Verification Tools for Linux Kernel Revision 994427a6 (framac): Add 'assume' annotation (parsed into a Jessie pragma)
04:08 PM Deductive Verification Tools for Linux Kernel Revision c40f8bab (framac): Delete aorai makefile
02:11 PM Deductive Verification Tools for Linux Kernel Revision 27a32124 (framac): Add support for using logic types in C (lemma) functions
Logic types are mapped into the C world as char pointers with
an attribute that contains the logic type.
Converting t...

08/03/2018

05:58 PM Deductive Verification Tools for Linux Kernel Revision 52e99de8 (framac): Add support for using logic types in C (lemma) functions
Logic types are mapped into the C world as char pointers with
an attribute that contains the logic type.
Converting t...

07/17/2018

05:36 PM Deductive Verification Tools for Linux Kernel Revision b7471bff (framac): Use original location for lemma-functions
05:29 PM Deductive Verification Tools for Linux Kernel Revision 9579c247 (framac): Allow Here label in lemma-functions
- Add Here label to generated axioms
- Error if other labels found

Also available in: Atom