General

Profile

Grigoriy Volkov

  • Registered on: 09/19/2017
  • Last connection: 05/10/2019

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...
Grigoriy Volkov

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 есть конструкции типа...
Grigoriy Volkov
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 Grigoriy Volkov

08/16/2018

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

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...
Grigoriy Volkov
05:54 PM Deductive Verification Tools for Linux Kernel Revision 24684d95 (framac): Untrack more aorai generated configs
Grigoriy Volkov
05:03 PM Deductive Verification Tools for Linux Kernel Revision 994427a6 (framac): Add 'assume' annotation (parsed into a Jessie pragma)
Grigoriy Volkov

05/24/2018

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

Also available in: Atom