General

Profile

Grigoriy Volkov

Issues

Projects

Activity

09/21/2018

02:43 PM Deductive Verification Tools for Linux Kernel Revision 8d617d80 (framac): Add 'introduce' statement for creating logical variables in C code
This construct allows declaring logical variables like so:
//@ introduce ℤ aaa; aaa > 123;
This is useful for rec...

09/17/2018

03:35 PM Deductive Verification Tools for Linux Kernel Bug #9284 (New): jingoo 1.2.18 падает generate.ml
В версии 1.2.18 jingoo стали убираться пробелы (trim).
В шаблоне lib/why3/z3_enum есть конструкции типа...
01:30 PM Deductive Verification Tools for Linux Kernel Wiki edit: Wiki (#15)
jingoo 1.2.18 seems to have a bug, add temporary workaround instructions

08/16/2018

02:45 PM Deductive Verification Tools for Linux Kernel Revision 1c54ed04 (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...
02:45 PM Deductive Verification Tools for Linux Kernel Revision e1dd303f (framac): Add 'assume' annotation (parsed into a Jessie pragma)
02:45 PM Deductive Verification Tools for Linux Kernel Revision 999cd3b1 (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/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

Also available in: Atom