Open-Source Projects

04/14/2022

05:48 PM Klever Feature #11444: Update CPAchecker SMG

Problem with definitions of mem*() functions is solved with new configuration options for SMGCPA:
cpa.smg.allocaFunc... Anton Vasilyev

04/13/2022

02:07 PM Klever Feature #11444: Update CPAchecker SMG

SMGCPA will provide ability to specify names of functions with behavior of mem*() functions to solve problem with def... Anton Vasilyev

03/29/2022

08:22 PM Klever Feature #11513 (Closed): Add pattern search to error traces comparison functions

It will be good for verification tool research to have ability to specify error marks by pattern search within witnes... Anton Vasilyev

12/09/2021

03:47 PM Klever Revision 93763fa2: Add checks to strcmp on end of second string to avoid false positive verdicts

Anton Vasilyev

11/30/2021

05:55 PM Klever Bug #11019 (Closed): Can't create new tags with 3d nesting level

Warning "Tag name can't contains '-'" is thrown on creation of 3d nesting level tag.
Probably symbol '-' is taken fr... Anton Vasilyev

10/26/2021

11:14 AM Klever Revision 0a76cd8d: Add preset mark for recursion

Anton Vasilyev

09/10/2021

04:31 PM Klever Feature #10933: Add configuration for CPAchecker SMG to disable uncertain environment behavior

Added support of pattern search for safe functions to CPAchecker on branch klever_fixes:38277 as an option:
cpa.smg.s... Anton Vasilyev

06/30/2021

03:10 PM C Instrumentation Framework Bug #10871 (Closed): Incorrect line directives on struct with union

Incorrect line directives on struct with union
struct fxregs_state is located from line 34 in /arch/x86/include/asm/... Anton Vasilyev

03/12/2021

05:48 PM Klever Feature #10750: Update CPAchecker (SMG)

New SMG with several improvements for witness representation and fixes bugs is on branch klever_fixes:36955 Anton Vasilyev

12/18/2020

06:07 PM Klever Revision 9a3ef70c: Add preset mark for recursion

Anton Vasilyev