Skip to content

Commit

Permalink
Add svcomp-validate conf for next SV-COMP
Browse files Browse the repository at this point in the history
Compared to svcomp24-validate:
1. Enables abortUnless (like svcomp over svcomp24).
2. Enables YAML violation_sequence validation.
  • Loading branch information
sim642 committed Jun 14, 2024
1 parent 1bdb1ae commit c546f2d
Showing 1 changed file with 142 additions and 0 deletions.
142 changes: 142 additions & 0 deletions conf/svcomp-validate.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,142 @@
{
"ana": {
"sv-comp": {
"enabled": true,
"functions": true
},
"int": {
"def_exc": true,
"enums": false,
"interval": true
},
"float": {
"interval": true
},
"activated": [
"base",
"threadid",
"threadflag",
"threadreturn",
"mallocWrapper",
"mutexEvents",
"mutex",
"access",
"race",
"escape",
"expRelation",
"mhp",
"assert",
"var_eq",
"symb_locks",
"region",
"thread",
"threadJoins",
"abortUnless",
"unassume"
],
"path_sens": [
"mutex",
"malloc_null",
"uninit",
"expsplit",
"activeSetjmp",
"memLeak",
"threadflag"
],
"context": {
"widen": false
},
"malloc": {
"wrappers": [
"kmalloc",
"__kmalloc",
"usb_alloc_urb",
"__builtin_alloca",
"kzalloc",

"ldv_malloc",

"kzalloc_node",
"ldv_zalloc",
"kmalloc_array",
"kcalloc",

"ldv_xmalloc",
"ldv_xzalloc",
"ldv_calloc",
"ldv_kzalloc"
]
},
"base": {
"arrays": {
"domain": "partitioned"
}
},
"race": {
"free": false,
"call": false
},
"autotune": {
"enabled": true,
"activated": [
"singleThreaded",
"mallocWrappers",
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
"termination",
"tmpSpecialAnalysis"
]
},
"widen": {
"tokens": true
}
},
"exp": {
"region-offsets": true
},
"solver": "td3",
"sem": {
"unknown_function": {
"spawn": false
},
"int": {
"signed_overflow": "assume_none"
},
"null-pointer": {
"dereference": "assume_none"
}
},
"witness": {
"graphml": {
"enabled": false
},
"yaml": {
"enabled": false,
"strict": true,
"format-version": "2.0",
"entry-types": [
"location_invariant",
"loop_invariant",
"invariant_set",
"violation_sequence"
],
"invariant-types": [
"location_invariant",
"loop_invariant"
]
},
"invariant": {
"loop-head": true,
"after-lock": true,
"other": true
}
},
"pre": {
"enabled": false
}
}

0 comments on commit c546f2d

Please sign in to comment.