Forked from
pub / frama-c
12233 commits behind the upstream repository.
-
Virgile Prevosto authoredVirgile Prevosto authored
with-libc.sarif 264.99 KiB
{
"$schema":
"https://github.com/oasis-tcs/sarif-spec/blob/master/Documents/CommitteeSpecificationDrafts/v2.1.0-CSD.1/sarif-schema-2.1.0.json",
"version": "2.1.0",
"runs": [
{
"tool": {
"driver": {
"name": "frama-c",
"fullName": "frama-c-0+omitted-for-deterministic-output",
"version": "0+omitted-for-deterministic-output",
"downloadUri": "https://frama-c.com/download.html",
"informationUri": "https://frama-c.com"
}
},
"invocations": [
{
"commandLine":
"frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-out tests/sarif/result/with-libc.sarif",
"arguments": [
"-check", "tests/sarif/libc.c", "-no-autoload-plugins",
"-load-module", "eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
"-mdr-sarif-deterministic", "-mdr-out",
"tests/sarif/result/with-libc.sarif"
],
"exitCode": 0,
"executionSuccessful": true
}
],
"originalUriBaseIds": {
"FRAMAC_SHARE": {
"uri": "file:///omitted-for-deterministic-output/"
},
"FRAMAC_LIB": { "uri": "file:///omitted-for-deterministic-output/" },
"FRAMAC_PLUGIN": {
"uri": "file:///omitted-for-deterministic-output/"
},
"PWD": { "uri": "file:///omitted-for-deterministic-output/" }
},
"artifacts": [
{
"location": { "uri": "tests/sarif/libc.c", "uriBaseId": "PWD" },
"roles": [ "analysisTarget" ],
"mimeType": "text/x-csrc"
}
],
"results": [
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "MemChr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 57,
"startColumn": 4,
"endLine": 59,
"endColumn": 62,
"byteLength": 134
}
}
}
] },
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "MemCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 39,
"startColumn": 4,
"endLine": 42,
"endColumn": 70,
"byteLength": 170
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "MemSet." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 68,
"startColumn": 4,
"endLine": 70,
"endColumn": 63,
"byteLength": 135
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "StrChr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 168,
"startColumn": 4,
"endLine": 170,
"endColumn": 75,
"byteLength": 132
}
}
}
]
}, {
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "StrCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 143,
"startColumn": 4,
"endLine": 147,
"endColumn": 63,
"byteLength": 170
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "StrLen." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 132,
"startColumn": 4,
"endLine": 135,
"endColumn": 38,
"byteLength": 185
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "StrNCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 155,
"startColumn": 4,
"endLine": 159,
"endColumn": 53,
"byteLength": 191
}
}
}
]
},
{ "ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "WMemChr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 183,
"startColumn": 4,
"endLine": 185,
"endColumn": 63,
"byteLength": 143
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "WcsChr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 266,
"startColumn": 4,
"endLine": 269,
"endColumn": 29,
"byteLength": 153
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "WcsCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 240,
"startColumn": 4,
"endLine": 244,
"endColumn": 63,
"byteLength": 173
}
}
}
]
},
{
"ruleId": "user-spec", "kind": "pass",
"level": "none",
"message": { "text": "WcsLen." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 230,
"startColumn": 4,
"endLine": 232,
"endColumn": 63,
"byteLength": 147
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "WcsNCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 252,
"startColumn": 4,
"endLine": 256,
"endColumn": 53,
"byteLength": 194
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "dynamic_allocation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_alloc_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 39,
"startColumn": 4,
"endLine": 41,
"endColumn": 61,
"byteLength": 110
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "memchr_def." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 57,
"startColumn": 4,
"endLine": 59,
"endColumn": 62,
"byteLength": 134
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "memcmp_strlen_left." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 119,
"startColumn": 4,
"endLine": 121,
"endColumn": 77,
"byteLength": 148
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "memcmp_strlen_right." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 123,
"startColumn": 4,
"endLine": 125,
"endColumn": 77,
"byteLength": 149
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": { "text": "memcmp_strlen_shift_left." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 127,
"startColumn": 4,
"endLine": 130,
"endColumn": 38,
"byteLength": 184
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "memcmp_strlen_shift_right." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 132,
"startColumn": 4,
"endLine": 135,
"endColumn": 38,
"byteLength": 185
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "memcmp_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 39,
"startColumn": 4,
"endLine": 42,
"endColumn": 70,
"byteLength": 170
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "memset_def." }, "locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 68,
"startColumn": 4,
"endLine": 70,
"endColumn": 63,
"byteLength": 135
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "never_allocable." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_alloc_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 39,
"startColumn": 4,
"endLine": 41,
"endColumn": 61,
"byteLength": 110
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strchr_def." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 168,
"startColumn": 4,
"endLine": 170,
"endColumn": 75,
"byteLength": 132
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strcmp_zero." },
"locations": [ {
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 143,
"startColumn": 4,
"endLine": 147,
"endColumn": 63,
"byteLength": 170
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_at_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 92,
"startColumn": 4,
"endLine": 93,
"endColumn": 61,
"byteLength": 86
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_before_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 89,
"startColumn": 4,
"endLine": 90,
"endColumn": 72,
"byteLength": 101
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_create." },
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 111,
"startColumn": 4,
"endLine": 113,
"endColumn": 51,
"byteLength": 111
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_create_shift." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 115,
"startColumn": 4,
"endLine": 117,
"endColumn": 62,
"byteLength": 143
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_neg." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 84,
"startColumn": 4,
"endLine": 87,
"endColumn": 22,
"byteLength": 109
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_not_zero." },
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 95,
"startColumn": 4,
"endLine": 97,
"endColumn": 58,
"byteLength": 120
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_pos_or_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 78,
"startColumn": 4,
"endLine": 82,
"endColumn": 40,
"byteLength": 169
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_shift." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 107,
"startColumn": 4,
"endLine": 109,
"endColumn": 59,
"byteLength": 118
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_sup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 103,
"startColumn": 4,
"endLine": 105,
"endColumn": 51,
"byteLength": 108
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strlen_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 99,
"startColumn": 4,
"endLine": 101,
"endColumn": 59,
"byteLength": 117
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "strncmp_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 155,
"startColumn": 4,
"endLine": 159,
"endColumn": 53,
"byteLength": 191
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcschr_def." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h", "uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 266,
"startColumn": 4,
"endLine": 269,
"endColumn": 29,
"byteLength": 153
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcscmp_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 240,
"startColumn": 4,
"endLine": 244,
"endColumn": 63,
"byteLength": 173
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_at_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 207,
"startColumn": 4,
"endLine": 208,
"endColumn": 65,
"byteLength": 90
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_before_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE" },
"region": {
"startLine": 204,
"startColumn": 4,
"endLine": 205,
"endColumn": 76,
"byteLength": 105
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_create." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 226,
"startColumn": 4,
"endLine": 228,
"endColumn": 52,
"byteLength": 115
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_create_shift." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 230,
"startColumn": 4,
"endLine": 232,
"endColumn": 63,
"byteLength": 147
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_neg." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
}, "region": {
"startLine": 199,
"startColumn": 4,
"endLine": 202,
"endColumn": 22,
"byteLength": 113
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_not_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 210,
"startColumn": 4,
"endLine": 212,
"endColumn": 59,
"byteLength": 124
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_pos_or_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 193,
"startColumn": 4,
"endLine": 197,
"endColumn": 41,
"byteLength": 174
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_shift." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 222,
"startColumn": 4,
"endLine": 224,
"endColumn": 55,
"byteLength": 117
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_sup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 218,
"startColumn": 4,
"endLine": 220,
"endColumn": 52,
"byteLength": 112
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcslen_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 214,
"startColumn": 4,
"endLine": 216,
"endColumn": 60,
"byteLength": 121
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wcsncmp_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 252, "startColumn": 4,
"endLine": 256,
"endColumn": 53,
"byteLength": 194
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "wmemchr_def." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 183,
"startColumn": 4,
"endLine": 185,
"endColumn": 63,
"byteLength": 143
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function bzero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 40,
"startColumn": 12,
"endLine": 40,
"endColumn": 17,
"byteLength": 5
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_memory_area." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 36,
"startColumn": 32, "endLine": 36,
"endColumn": 63,
"byteLength": 31
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "s_initialized." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 38,
"startColumn": 39,
"endLine": 38,
"endColumn": 75,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "zero_initialized." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 39,
"startColumn": 28,
"endLine": 39,
"endColumn": 63,
"byteLength": 35
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function bzero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 37,
"startColumn": 10,
"endLine": 37, "endColumn": 31,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *((char *)s + (0 .. n - 1)) in function bzero."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 37,
"startColumn": 10,
"endLine": 37,
"endColumn": 31,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "specialization of valid_string_s at stmt 2."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "tests/sarif/libc.c",
"uriBaseId": "PWD"
},
"region": {
"startLine": 13,
"startColumn": 10,
"endLine": 13,
"endColumn": 19,
"byteLength": 9
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function memchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
}, "region": {
"startLine": 88,
"startColumn": 12,
"endLine": 88,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior found in function memchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 88,
"startColumn": 12,
"endLine": 88,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior not_found in function memchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 88,
"startColumn": 12,
"endLine": 88,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 68,
"startColumn": 9,
"endLine": 69,
"endColumn": 74,
"byteLength": 100
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 71,
"startColumn": 8,
"endLine": 72,
"endColumn": 71,
"byteLength": 116
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "danglingness." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 74,
"startColumn": 8,
"endLine": 75,
"endColumn": 61,
"byteLength": 80
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "char_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 78, "startColumn": 24,
"endLine": 78,
"endColumn": 44,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "char_not_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 85,
"startColumn": 28,
"endLine": 85,
"endColumn": 49,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_same_base." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 79,
"startColumn": 30,
"endLine": 79,
"endColumn": 66,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_char." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 80,
"startColumn": 25, "endLine": 80,
"endColumn": 45,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_in_str." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 81,
"startColumn": 27,
"endLine": 83,
"endColumn": 54,
"byteLength": 120
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 86,
"startColumn": 25,
"endLine": 86,
"endColumn": 41,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function memchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 88,
"startColumn": 12,
"endLine": 88, "endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function memchr."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 76,
"startColumn": 12,
"endLine": 76,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function memcmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 65,
"startColumn": 11,
"endLine": 65,
"endColumn": 17,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 55,
"startColumn": 23, "endLine": 55,
"endColumn": 49,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 56,
"startColumn": 23,
"endLine": 56,
"endColumn": 49,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 57,
"startColumn": 32,
"endLine": 57,
"endColumn": 68,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 58,
"startColumn": 32,
"endLine": 58, "endColumn": 68,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "danglingness." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 59,
"startColumn": 30,
"endLine": 59,
"endColumn": 49,
"byteLength": 19
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "danglingness." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 60,
"startColumn": 30,
"endLine": 60,
"endColumn": 49,
"byteLength": 19
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "logic_spec." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 63,
"startColumn": 24,
"endLine": 63,
"endColumn": 73, "byteLength": 49
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function memcmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 65,
"startColumn": 11,
"endLine": 65,
"endColumn": 17,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function memcmp."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 61,
"startColumn": 12,
"endLine": 61,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function memcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 101,
"startColumn": 12,
"endLine": 101, "endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_dest." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 92,
"startColumn": 25,
"endLine": 92,
"endColumn": 48,
"byteLength": 23
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 93,
"startColumn": 24,
"endLine": 93,
"endColumn": 51,
"byteLength": 27
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 95,
"startColumn": 4,
"endLine": 95,
"endColumn": 62, "byteLength": 58
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "copied_contents." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 98,
"startColumn": 29,
"endLine": 98,
"endColumn": 76,
"byteLength": 47
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 99,
"startColumn": 24,
"endLine": 99,
"endColumn": 39,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function memcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 96,
"startColumn": 12,
"endLine": 96,
"endColumn": 35,
"byteLength": 23 }
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *((char *)dest + (0 .. n - 1)) in function memcpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 96,
"startColumn": 12,
"endLine": 96,
"endColumn": 35,
"byteLength": 23
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function memcpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 97,
"startColumn": 12,
"endLine": 97,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function memmove." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 111, "startColumn": 12,
"endLine": 111,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_dest." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 104,
"startColumn": 25,
"endLine": 104,
"endColumn": 48,
"byteLength": 23
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 105,
"startColumn": 24,
"endLine": 105,
"endColumn": 51,
"byteLength": 27
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "copied_contents." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 108,
"startColumn": 29, "endLine": 108,
"endColumn": 76,
"byteLength": 47
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 109,
"startColumn": 24,
"endLine": 109,
"endColumn": 39,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function memmove." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 106,
"startColumn": 12,
"endLine": 106,
"endColumn": 35,
"byteLength": 23
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *((char *)dest + (0 .. n - 1)) in function memmove."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 106,
"startColumn": 12,
"endLine": 106,
"endColumn": 35,
"byteLength": 23
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function memmove."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 107,
"startColumn": 12,
"endLine": 107,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function memset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 121,
"startColumn": 12,
"endLine": 121,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
}, "region": {
"startLine": 115,
"startColumn": 22,
"endLine": 115,
"endColumn": 42,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "acsl_c_equiv." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 118,
"startColumn": 26,
"endLine": 118,
"endColumn": 46,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 119,
"startColumn": 24,
"endLine": 119,
"endColumn": 36,
"byteLength": 12
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function memset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 116,
"startColumn": 12,
"endLine": 116,
"endColumn": 32,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *((char *)s + (0 .. n - 1)) in function memset."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 116,
"startColumn": 12,
"endLine": 116,
"endColumn": 32,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function memset."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 117,
"startColumn": 12,
"endLine": 117,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function stpcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 405,
"startColumn": 12,
"endLine": 405,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 396,
"startColumn": 31,
"endLine": 396,
"endColumn": 53,
"byteLength": 22
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 397,
"startColumn": 26,
"endLine": 397,
"endColumn": 55,
"byteLength": 29
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h", "uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 399,
"startColumn": 4,
"endLine": 399,
"endColumn": 59,
"byteLength": 55
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "equal_contents." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 402,
"startColumn": 28,
"endLine": 402,
"endColumn": 49,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "points_to_end." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 403,
"startColumn": 27,
"endLine": 403,
"endColumn": 57,
"byteLength": 30
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function stpcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE" },
"region": {
"startLine": 400,
"startColumn": 12,
"endLine": 400,
"endColumn": 32,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(dest + (0 .. strlen{Old}(src))) in function stpcpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 400,
"startColumn": 12,
"endLine": 400,
"endColumn": 32,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function stpcpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 401,
"startColumn": 12,
"endLine": 401,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strcasecmp." },
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 50,
"startColumn": 11,
"endLine": 50,
"endColumn": 21,
"byteLength": 10
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 46,
"startColumn": 28,
"endLine": 46,
"endColumn": 49,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 47,
"startColumn": 28,
"endLine": 47,
"endColumn": 49,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strcasecmp." },
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 50,
"startColumn": 11,
"endLine": 50,
"endColumn": 21,
"byteLength": 10
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strcasecmp."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 48,
"startColumn": 10,
"endLine": 48,
"endColumn": 17,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strcasestr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 239,
"startColumn": 12,
"endLine": 239,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_haystack." },
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 231,
"startColumn": 36,
"endLine": 231,
"endColumn": 63,
"byteLength": 27
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_needle." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 232,
"startColumn": 34,
"endLine": 232,
"endColumn": 59,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_null_or_in_haystack." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 236,
"startColumn": 4,
"endLine": 237,
"endColumn": 65,
"byteLength": 82
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strcasestr." },
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 239,
"startColumn": 12,
"endLine": 239,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strcasestr."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 233,
"startColumn": 12,
"endLine": 233,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strcat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 420,
"startColumn": 12,
"endLine": 420,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_src." },
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 408,
"startColumn": 31,
"endLine": 408,
"endColumn": 53,
"byteLength": 22
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_dest." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 409,
"startColumn": 32,
"endLine": 409,
"endColumn": 50,
"byteLength": 18
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 410,
"startColumn": 26,
"endLine": 410,
"endColumn": 70,
"byteLength": 44
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "sum_of_lengths." },
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 413,
"startColumn": 28,
"endLine": 413,
"endColumn": 76,
"byteLength": 48
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 416,
"startColumn": 4,
"endLine": 416,
"endColumn": 60,
"byteLength": 56
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "dest_null_terminated." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 417,
"startColumn": 34,
"endLine": 417,
"endColumn": 77,
"byteLength": 43
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 418,
"startColumn": 24,
"endLine": 418,
"endColumn": 39,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strcat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 411,
"startColumn": 12,
"endLine": 411,
"endColumn": 58,
"byteLength": 46
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strcat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 411,
"startColumn": 12,
"endLine": 411,
"endColumn": 58,
"byteLength": 46
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strcat."
}, "locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 414,
"startColumn": 12,
"endLine": 414,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default in function strchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 173,
"startColumn": 12,
"endLine": 173,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 173,
"startColumn": 12,
"endLine": 173,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior found in function strchr." },
"locations": [ {
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 173,
"startColumn": 12,
"endLine": 173,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior not_found in function strchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 173,
"startColumn": 12,
"endLine": 173,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 157,
"startColumn": 29,
"endLine": 157,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "char_found." },
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 160,
"startColumn": 24,
"endLine": 160,
"endColumn": 35,
"byteLength": 11
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "char_not_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 167,
"startColumn": 28,
"endLine": 167,
"endColumn": 40,
"byteLength": 12
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_char." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 161,
"startColumn": 25,
"endLine": 161,
"endColumn": 44,
"byteLength": 19
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_same_base." },
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 162,
"startColumn": 30,
"endLine": 162,
"endColumn": 66,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_in_length." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 163,
"startColumn": 30,
"endLine": 163,
"endColumn": 59,
"byteLength": 29
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_valid_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 164,
"startColumn": 33,
"endLine": 164,
"endColumn": 59,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_first_occur." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 165,
"startColumn": 32,
"endLine": 165,
"endColumn": 79,
"byteLength": 47
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 168,
"startColumn": 25,
"endLine": 168,
"endColumn": 41,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_null_or_same_base." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 171,
"startColumn": 4,
"endLine": 171,
"endColumn": 60,
"byteLength": 56
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h", "uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 173,
"startColumn": 12,
"endLine": 173,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strchr."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 158,
"startColumn": 12,
"endLine": 158,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strchrnul." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 179,
"startColumn": 12,
"endLine": 179,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 175,
"startColumn": 29,
"endLine": 175,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_same_base." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 177,
"startColumn": 30,
"endLine": 177,
"endColumn": 64,
"byteLength": 34
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strchrnul." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 179,
"startColumn": 12,
"endLine": 179,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strchrnul."
},
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 176,
"startColumn": 12,
"endLine": 176,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strcmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 142,
"startColumn": 11,
"endLine": 142,
"endColumn": 17,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 137,
"startColumn": 30,
"endLine": 137,
"endColumn": 51,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 138,
"startColumn": 30,
"endLine": 138,
"endColumn": 51,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "acsl_c_equiv." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 140,
"startColumn": 26,
"endLine": 140,
"endColumn": 50,
"byteLength": 24
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strcmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 142,
"startColumn": 11,
"endLine": 142,
"endColumn": 17,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strcmp."
},
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 139,
"startColumn": 12,
"endLine": 139,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strcoll." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 155,
"startColumn": 11,
"endLine": 155,
"endColumn": 18,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 151,
"startColumn": 30,
"endLine": 151,
"endColumn": 51,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 152,
"startColumn": 30,
"endLine": 152,
"endColumn": 51,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strcoll." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 155,
"startColumn": 11,
"endLine": 155,
"endColumn": 18,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strcoll."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 153,
"startColumn": 12,
"endLine": 153,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strcpy." },
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 360,
"startColumn": 12,
"endLine": 360,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 351,
"startColumn": 31,
"endLine": 351,
"endColumn": 53,
"byteLength": 22
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 352,
"startColumn": 26,
"endLine": 352,
"endColumn": 55,
"byteLength": 29
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 354,
"startColumn": 4,
"endLine": 354,
"endColumn": 59,
"byteLength": 55
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "equal_contents." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 357,
"startColumn": 28,
"endLine": 357,
"endColumn": 49,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 358,
"startColumn": 24,
"endLine": 358,
"endColumn": 39,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h", "uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 355,
"startColumn": 12,
"endLine": 355,
"endColumn": 32,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(dest + (0 .. strlen{Old}(src))) in function strcpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 355,
"startColumn": 12,
"endLine": 355,
"endColumn": 32,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strcpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 356,
"startColumn": 12,
"endLine": 356,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strcspn." },
"locations": [ {
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 202,
"startColumn": 14,
"endLine": 202,
"endColumn": 21,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 197,
"startColumn": 29,
"endLine": 197,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_reject." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 198,
"startColumn": 34,
"endLine": 198,
"endColumn": 59,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_bounded." },
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 200,
"startColumn": 28,
"endLine": 200,
"endColumn": 53,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strcspn." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 202,
"startColumn": 14,
"endLine": 202,
"endColumn": 21,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strcspn."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 199,
"startColumn": 12,
"endLine": 199,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior allocation in function strdup." },
"locations": [ {
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 484,
"startColumn": 12,
"endLine": 484,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strdup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 484,
"startColumn": 12,
"endLine": 484,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior no_allocation in function strdup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 484,
"startColumn": 12,
"endLine": 484,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 468,
"startColumn": 29,
"endLine": 468,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "can_allocate." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 472,
"startColumn": 26,
"endLine": 472,
"endColumn": 49,
"byteLength": 23
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "cannot_allocate." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 479,
"startColumn": 29,
"endLine": 479,
"endColumn": 53,
"byteLength": 24
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "allocation." },
"locations": [
{
"physicalLocation": { "artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 475,
"startColumn": 24,
"endLine": 475,
"endColumn": 49,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_valid_string_and_same_contents." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 477,
"startColumn": 4,
"endLine": 477,
"endColumn": 51,
"byteLength": 47
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 482,
"startColumn": 25,
"endLine": 482,
"endColumn": 41,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strdup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": { "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 473,
"startColumn": 12,
"endLine": 473,
"endColumn": 28,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strdup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 484,
"startColumn": 12,
"endLine": 484,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strdup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 484,
"startColumn": 12,
"endLine": 484,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term __fc_heap_status in function strdup."
},
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 473,
"startColumn": 12,
"endLine": 473,
"endColumn": 28,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strdup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 474,
"startColumn": 12,
"endLine": 474,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strdup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 470,
"startColumn": 12,
"endLine": 470,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": {
"text": "from clause of term \\result in function strdup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 480,
"startColumn": 12,
"endLine": 480,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "allocates/frees clause in function strdup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 469,
"startColumn": 14,
"endLine": 469,
"endColumn": 21,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "allocates/frees clause in function strdup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 484,
"startColumn": 12,
"endLine": 484,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "behavior default! in function strerror." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 347,
"startColumn": 12,
"endLine": 347,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_internal_str." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 343,
"startColumn": 33,
"endLine": 343,
"endColumn": 59,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_nul_terminated." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 344,
"startColumn": 35,
"endLine": 344,
"endColumn": 51,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": { "text": "result_valid_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 345,
"startColumn": 33,
"endLine": 345,
"endColumn": 59,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strerror." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 347,
"startColumn": 12,
"endLine": 347,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strerror."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 342,
"startColumn": 12,
"endLine": 342,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "behavior default! in function strlcat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 455,
"startColumn": 14,
"endLine": 455,
"endColumn": 21,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 448,
"startColumn": 31,
"endLine": 448,
"endColumn": 53,
"byteLength": 22
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_dest." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 449,
"startColumn": 32,
"endLine": 449,
"endColumn": 50,
"byteLength": 18
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": { "text": "room_nstring." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 450,
"startColumn": 27,
"endLine": 450,
"endColumn": 48,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "bounded_result." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 453,
"startColumn": 28,
"endLine": 453,
"endColumn": 65,
"byteLength": 37
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strlcat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 451,
"startColumn": 12,
"endLine": 451,
"endColumn": 33,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text":
"from clause of term *(dest + (strlen{Old}(dest) .. n)) in function strlcat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 451,
"startColumn": 12,
"endLine": 451,
"endColumn": 33,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strlcat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 452,
"startColumn": 12,
"endLine": 452,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strlcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 393,
"startColumn": 7,
"endLine": 393,
"endColumn": 14,
"byteLength": 7
}
}
}
]
},
{ "ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 384,
"startColumn": 31,
"endLine": 384,
"endColumn": 53,
"byteLength": 22
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "room_nstring." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 385,
"startColumn": 27,
"endLine": 385,
"endColumn": 48,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 387,
"startColumn": 4,
"endLine": 387,
"endColumn": 61,
"byteLength": 57
}
}
}
]
},
{
"ruleId": "user-spec", "kind": "pass",
"level": "none",
"message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 390,
"startColumn": 28,
"endLine": 390,
"endColumn": 73,
"byteLength": 45
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "bounded_result." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 391,
"startColumn": 28,
"endLine": 391,
"endColumn": 50,
"byteLength": 22
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strlcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 388,
"startColumn": 12,
"endLine": 388,
"endColumn": 24,
"byteLength": 12
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": {
"text":
"from clause of term *(dest + (0 .. n - 1)) in function strlcpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 388,
"startColumn": 12,
"endLine": 388,
"endColumn": 24,
"byteLength": 12
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strlcpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 389,
"startColumn": 12,
"endLine": 389,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strlen." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 129,
"startColumn": 14,
"endLine": 129,
"endColumn": 20,
"byteLength": 6
}
}
}
] },
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 125,
"startColumn": 29,
"endLine": 125,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "acsl_c_equiv." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 127,
"startColumn": 26,
"endLine": 127,
"endColumn": 46,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strlen." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 129,
"startColumn": 14,
"endLine": 129,
"endColumn": 20,
"byteLength": 6
}
}
}
]
}, {
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strlen."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 126,
"startColumn": 12,
"endLine": 126,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strncasecmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 57,
"startColumn": 11,
"endLine": 57,
"endColumn": 22,
"byteLength": 11
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 53,
"startColumn": 28,
"endLine": 53,
"endColumn": 53,
"byteLength": 25
}
}
}
] },
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 54,
"startColumn": 28,
"endLine": 54,
"endColumn": 53,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strncasecmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 57,
"startColumn": 11,
"endLine": 57,
"endColumn": 22,
"byteLength": 11
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strncasecmp."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 55,
"startColumn": 10,
"endLine": 55,
"endColumn": 17,
"byteLength": 7
}
}
} ]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior complete in function strncat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 444,
"startColumn": 12,
"endLine": 444,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strncat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 444,
"startColumn": 12,
"endLine": 444,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior partial in function strncat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 444,
"startColumn": 12,
"endLine": 444,
"endColumn": 13,
"byteLength": 1
}
}
}
] },
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_nstring_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 423,
"startColumn": 32,
"endLine": 423,
"endColumn": 58,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_dest." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 424,
"startColumn": 32,
"endLine": 424,
"endColumn": 50,
"byteLength": 18
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 430,
"startColumn": 26,
"endLine": 430,
"endColumn": 74,
"byteLength": 48
}
}
}
]
}, {
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 438,
"startColumn": 26,
"endLine": 438,
"endColumn": 64,
"byteLength": 38
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_src_fits." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 429,
"startColumn": 35,
"endLine": 429,
"endColumn": 77,
"byteLength": 42
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_src_too_large." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 437,
"startColumn": 4,
"endLine": 437,
"endColumn": 49,
"byteLength": 45
}
}
}
]
},
{ "ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 427,
"startColumn": 24,
"endLine": 427,
"endColumn": 39,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "sum_of_lengths." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 434,
"startColumn": 28,
"endLine": 434,
"endColumn": 76,
"byteLength": 48
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "sum_of_bounded_lengths." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 442,
"startColumn": 36,
"endLine": 442,
"endColumn": 74,
"byteLength": 38
}
}
}
]
},
{
"ruleId": "user-spec", "kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strncat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 431,
"startColumn": 12,
"endLine": 431,
"endColumn": 58,
"byteLength": 46
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strncat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 425,
"startColumn": 12,
"endLine": 425,
"endColumn": 50,
"byteLength": 38
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strncat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 439,
"startColumn": 12,
"endLine": 439,
"endColumn": 48,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": {
"text":
"from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strncat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 431,
"startColumn": 12,
"endLine": 431,
"endColumn": 58,
"byteLength": 46
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strncat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 433,
"startColumn": 12,
"endLine": 433,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) in function strncat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 425,
"startColumn": 12,
"endLine": 425,
"endColumn": 50,
"byteLength": 38
} }
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strncat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 426,
"startColumn": 12,
"endLine": 426,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) in function strncat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 439,
"startColumn": 12,
"endLine": 439,
"endColumn": 48,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strncat."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 441,
"startColumn": 12,
"endLine": 441,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strncmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 149,
"startColumn": 11,
"endLine": 149,
"endColumn": 18,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 144,
"startColumn": 30,
"endLine": 144,
"endColumn": 55,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 145, "startColumn": 30,
"endLine": 145,
"endColumn": 55,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "acsl_c_equiv." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 147,
"startColumn": 26,
"endLine": 147,
"endColumn": 53,
"byteLength": 27
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strncmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 149,
"startColumn": 11,
"endLine": 149,
"endColumn": 18,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strncmp."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 146,
"startColumn": 12,
"endLine": 146,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior complete in function strncpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 378,
"startColumn": 12,
"endLine": 378,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strncpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 378,
"startColumn": 12,
"endLine": 378,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior partial in function strncpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 378, "startColumn": 12,
"endLine": 378,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_nstring_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 363,
"startColumn": 32,
"endLine": 363,
"endColumn": 58,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "room_nstring." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 364,
"startColumn": 27,
"endLine": 364,
"endColumn": 50,
"byteLength": 23
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 366,
"startColumn": 4, "endLine": 366,
"endColumn": 43,
"byteLength": 39
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "src_fits." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 372,
"startColumn": 22,
"endLine": 372,
"endColumn": 37,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "src_too_long." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 375,
"startColumn": 26,
"endLine": 375,
"endColumn": 42,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 369,
"startColumn": 24,
"endLine": 369, "endColumn": 39,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 370,
"startColumn": 28,
"endLine": 370,
"endColumn": 57,
"byteLength": 29
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "equal_after_copy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 373,
"startColumn": 30,
"endLine": 373,
"endColumn": 51,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "equal_prefix." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 376,
"startColumn": 26,
"endLine": 376,
"endColumn": 60, "byteLength": 34
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strncpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 367,
"startColumn": 12,
"endLine": 367,
"endColumn": 26,
"byteLength": 14
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(dest + (0 .. n - 1)) in function strncpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 367,
"startColumn": 12,
"endLine": 367,
"endColumn": 26,
"byteLength": 14
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strncpy."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 368,
"startColumn": 12,
"endLine": 368,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior allocation in function strndup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 506,
"startColumn": 12,
"endLine": 506,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strndup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 506,
"startColumn": 12,
"endLine": 506,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "behavior no_allocation in function strndup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
}, "region": {
"startLine": 506,
"startColumn": 12,
"endLine": 506,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 486,
"startColumn": 29,
"endLine": 486,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "can_allocate." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 491,
"startColumn": 26,
"endLine": 491,
"endColumn": 60,
"byteLength": 34
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "cannot_allocate." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 501,
"startColumn": 29,
"endLine": 501,
"endColumn": 64,
"byteLength": 35
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "allocation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 495,
"startColumn": 24,
"endLine": 495,
"endColumn": 60,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "result_valid_string_bounded_and_same_prefix."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 497,
"startColumn": 4,
"endLine": 499,
"endColumn": 29,
"byteLength": 124
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
}, "region": {
"startLine": 504,
"startColumn": 25,
"endLine": 504,
"endColumn": 41,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strndup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 492,
"startColumn": 12,
"endLine": 492,
"endColumn": 28,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strndup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 506,
"startColumn": 12,
"endLine": 506,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strndup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 506,
"startColumn": 12,
"endLine": 506,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term __fc_heap_status in function strndup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 492,
"startColumn": 12,
"endLine": 492,
"endColumn": 28,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strndup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 493,
"startColumn": 12,
"endLine": 493,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strndup."
},
"locations": [
{ "physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 488,
"startColumn": 12,
"endLine": 488,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strndup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 502,
"startColumn": 12,
"endLine": 502,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "allocates/frees clause in function strndup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 487,
"startColumn": 14,
"endLine": 487,
"endColumn": 21,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": {
"text": "allocates/frees clause in function strndup."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 506,
"startColumn": 12,
"endLine": 506,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strnlen." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 135,
"startColumn": 14,
"endLine": 135,
"endColumn": 21,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 131,
"startColumn": 29,
"endLine": 131,
"endColumn": 53,
"byteLength": 24
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "result_bounded." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 133,
"startColumn": 28,
"endLine": 133,
"endColumn": 64,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strnlen." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 135,
"startColumn": 14,
"endLine": 135,
"endColumn": 21,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strnlen."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 132,
"startColumn": 12,
"endLine": 132,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec", "kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strpbrk." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 218,
"startColumn": 12,
"endLine": 218,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 212,
"startColumn": 29,
"endLine": 212,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_accept." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 213,
"startColumn": 34,
"endLine": 213,
"endColumn": 59,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "result_null_or_same_base." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 216,
"startColumn": 4,
"endLine": 216,
"endColumn": 60,
"byteLength": 56
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strpbrk." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 218,
"startColumn": 12,
"endLine": 218,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strpbrk."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 214,
"startColumn": 12,
"endLine": 214,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec", "kind": "pass",
"level": "none",
"message": { "text": "behavior default in function strrchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 195,
"startColumn": 12,
"endLine": 195,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strrchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 195,
"startColumn": 12,
"endLine": 195,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior found in function strrchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 195,
"startColumn": 12,
"endLine": 195,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "behavior not_found in function strrchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 195,
"startColumn": 12,
"endLine": 195,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 181,
"startColumn": 29,
"endLine": 181,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "char_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 184,
"startColumn": 24,
"endLine": 184,
"endColumn": 35,
"byteLength": 11
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": { "text": "char_not_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 189,
"startColumn": 28,
"endLine": 189,
"endColumn": 40,
"byteLength": 12
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_char." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 185,
"startColumn": 25,
"endLine": 185,
"endColumn": 38,
"byteLength": 13
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_same_base." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 186,
"startColumn": 30,
"endLine": 186,
"endColumn": 66,
"byteLength": 36
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_valid_string." }, "locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 187,
"startColumn": 33,
"endLine": 187,
"endColumn": 59,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 190,
"startColumn": 25,
"endLine": 190,
"endColumn": 41,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_null_or_same_base." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 193,
"startColumn": 4,
"endLine": 193,
"endColumn": 60,
"byteLength": 56
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strrchr." },
"locations": [ {
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 195,
"startColumn": 12,
"endLine": 195,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strrchr."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 182,
"startColumn": 12,
"endLine": 182,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strsep." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 334,
"startColumn": 12,
"endLine": 334,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_stringp." }, "locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 329,
"startColumn": 35,
"endLine": 329,
"endColumn": 76,
"byteLength": 41
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_delim." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 330,
"startColumn": 33,
"endLine": 330,
"endColumn": 57,
"byteLength": 24
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strsep." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 331,
"startColumn": 12,
"endLine": 331,
"endColumn": 20,
"byteLength": 8
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term *stringp in function strsep." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 331,
"startColumn": 12,
"endLine": 331,
"endColumn": 20,
"byteLength": 8
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strsep."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 332,
"startColumn": 12,
"endLine": 332,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strsignal." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 523,
"startColumn": 12,
"endLine": 523,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "result_internal_str." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 519,
"startColumn": 33,
"endLine": 519,
"endColumn": 60,
"byteLength": 27
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_nul_terminated." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 520,
"startColumn": 35,
"endLine": 520,
"endColumn": 51,
"byteLength": 16
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_valid_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 521,
"startColumn": 33,
"endLine": 521,
"endColumn": 59,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": { "text": "assigns clause in function strsignal." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 523,
"startColumn": 12,
"endLine": 523,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strsignal."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 518,
"startColumn": 12,
"endLine": 518,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strspn." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 210,
"startColumn": 14,
"endLine": 210,
"endColumn": 20,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 204,
"startColumn": 29,
"endLine": 204,
"endColumn": 49,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_accept." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 205,
"startColumn": 34,
"endLine": 205,
"endColumn": 59,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_bounded." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 208,
"startColumn": 28,
"endLine": 208,
"endColumn": 53,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": { "text": "assigns clause in function strspn." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 206,
"startColumn": 12,
"endLine": 206,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strspn."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 206,
"startColumn": 12,
"endLine": 206,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strspn."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 207,
"startColumn": 12,
"endLine": 207,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{ "ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strstr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 229,
"startColumn": 12,
"endLine": 229,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_haystack." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 220,
"startColumn": 36,
"endLine": 220,
"endColumn": 63,
"byteLength": 27
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_needle." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 221,
"startColumn": 34,
"endLine": 221,
"endColumn": 59,
"byteLength": 25
}
}
}
]
},
{
"ruleId": "user-spec", "kind": "pass",
"level": "none",
"message": { "text": "result_null_or_in_haystack." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 225,
"startColumn": 4,
"endLine": 227,
"endColumn": 59,
"byteLength": 141
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strstr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 229,
"startColumn": 12,
"endLine": 229,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strstr."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 222,
"startColumn": 12,
"endLine": 222,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{ "ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 283,
"startColumn": 12,
"endLine": 283,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior new_str in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 283,
"startColumn": 12,
"endLine": 283,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior resume_str in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 283,
"startColumn": 12,
"endLine": 283,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec", "kind": "pass",
"level": "none",
"message": { "text": "valid_string_delim." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 245,
"startColumn": 31,
"endLine": 245,
"endColumn": 55,
"byteLength": 24
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s_or_delim_not_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 258,
"startColumn": 6,
"endLine": 260,
"endColumn": 70,
"byteLength": 120
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "not_first_call." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 268,
"startColumn": 29,
"endLine": 268,
"endColumn": 53,
"byteLength": 24
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass", "level": "none",
"message": { "text": "s_not_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 256,
"startColumn": 24,
"endLine": 256,
"endColumn": 34,
"byteLength": 10
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "s_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 267,
"startColumn": 20,
"endLine": 267,
"endColumn": 30,
"byteLength": 10
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 264,
"startColumn": 27,
"endLine": 264,
"endColumn": 72,
"byteLength": 45
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none", "message": { "text": "ptr_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 265,
"startColumn": 24,
"endLine": 265,
"endColumn": 57,
"byteLength": 33
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 277,
"startColumn": 27,
"endLine": 278,
"endColumn": 72,
"byteLength": 92
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "ptr_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 279,
"startColumn": 24,
"endLine": 279,
"endColumn": 77,
"byteLength": 53
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strtok." }, "locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 246,
"startColumn": 10,
"endLine": 246,
"endColumn": 16,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 261,
"startColumn": 12,
"endLine": 261,
"endColumn": 27,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 269,
"startColumn": 12,
"endLine": 269,
"endColumn": 32,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term *(s + (0 ..)) in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 246,
"startColumn": 10,
"endLine": 246,
"endColumn": 16,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(__fc_strtok_ptr + (0 ..)) in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 248,
"startColumn": 10,
"endLine": 248,
"endColumn": 30,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 250,
"startColumn": 10,
"endLine": 250,
"endColumn": 17,
"byteLength": 7
}
}
}
]
}, {
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term __fc_strtok_ptr in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 252,
"startColumn": 10,
"endLine": 252,
"endColumn": 25,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term __fc_strtok_ptr in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 261,
"startColumn": 12,
"endLine": 261,
"endColumn": 27,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term *(s + (0 ..)) in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 262,
"startColumn": 12,
"endLine": 262,
"endColumn": 18,
"byteLength": 6 }
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 263,
"startColumn": 12,
"endLine": 263,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(__fc_strtok_ptr + (0 ..)) in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 269,
"startColumn": 12,
"endLine": 269,
"endColumn": 32,
"byteLength": 20
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term __fc_strtok_ptr in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
}, "region": {
"startLine": 272,
"startColumn": 12,
"endLine": 272,
"endColumn": 27,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strtok."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 275,
"startColumn": 12,
"endLine": 275,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "complete clause in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 283,
"startColumn": 12,
"endLine": 283,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "disjoint clause in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE" },
"region": {
"startLine": 283,
"startColumn": 12,
"endLine": 283,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 327,
"startColumn": 12,
"endLine": 327,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior new_str in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 327,
"startColumn": 12,
"endLine": 327,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior resume_str in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
}, "region": {
"startLine": 327,
"startColumn": 12,
"endLine": 327,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_delim." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 286,
"startColumn": 31,
"endLine": 286,
"endColumn": 55,
"byteLength": 24
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_saveptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 287,
"startColumn": 26,
"endLine": 287,
"endColumn": 41,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_s_or_delim_not_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": { "startLine": 300,
"startColumn": 6,
"endLine": 302,
"endColumn": 70,
"byteLength": 120
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "not_first_call." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 311,
"startColumn": 29,
"endLine": 311,
"endColumn": 46,
"byteLength": 17
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 312,
"startColumn": 37,
"endLine": 312,
"endColumn": 58,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "s_not_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 298, "startColumn": 24,
"endLine": 298,
"endColumn": 34,
"byteLength": 10
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "s_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 310,
"startColumn": 20,
"endLine": 310,
"endColumn": 30,
"byteLength": 10
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 306,
"startColumn": 27,
"endLine": 306,
"endColumn": 72,
"byteLength": 45
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 307,
"startColumn": 28, "endLine": 307,
"endColumn": 49,
"byteLength": 21
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "saveptr_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 308,
"startColumn": 28,
"endLine": 308,
"endColumn": 54,
"byteLength": 26
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "result_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 321,
"startColumn": 27,
"endLine": 322,
"endColumn": 65,
"byteLength": 85
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "saveptr_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 323,
"startColumn": 28,
"endLine": 323, "endColumn": 67,
"byteLength": 39
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 288,
"startColumn": 10,
"endLine": 288,
"endColumn": 16,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 303,
"startColumn": 12,
"endLine": 303,
"endColumn": 20,
"byteLength": 8
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 313,
"startColumn": 12,
"endLine": 313,
"endColumn": 27, "byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term *(s + (0 ..)) in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 288,
"startColumn": 10,
"endLine": 288,
"endColumn": 16,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(*saveptr + (0 ..)) in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 290,
"startColumn": 10,
"endLine": 290,
"endColumn": 25,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE" },
"region": {
"startLine": 292,
"startColumn": 10,
"endLine": 292,
"endColumn": 17,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term *saveptr in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 294,
"startColumn": 10,
"endLine": 294,
"endColumn": 18,
"byteLength": 8
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term *saveptr in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 303,
"startColumn": 12,
"endLine": 303,
"endColumn": 20,
"byteLength": 8
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term *(s + (0 ..)) in function strtok_r."
},
"locations": [ {
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 304,
"startColumn": 12,
"endLine": 304,
"endColumn": 18,
"byteLength": 6
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 305,
"startColumn": 12,
"endLine": 305,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(*saveptr + (0 ..)) in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 313,
"startColumn": 12,
"endLine": 313,
"endColumn": 27,
"byteLength": 15
}
}
}
]
},
{
"ruleId": "user-spec", "kind": "pass",
"level": "none",
"message": {
"text": "from clause of term *saveptr in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 316,
"startColumn": 12,
"endLine": 316,
"endColumn": 20,
"byteLength": 8
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strtok_r."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 319,
"startColumn": 12,
"endLine": 319,
"endColumn": 19,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "complete clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 327,
"startColumn": 12,
"endLine": 327,
"endColumn": 13,
"byteLength": 1
}
}
}
] },
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "disjoint clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 327,
"startColumn": 12,
"endLine": 327,
"endColumn": 13,
"byteLength": 1
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "behavior default! in function strxfrm." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 463,
"startColumn": 14,
"endLine": 463,
"endColumn": 21,
"byteLength": 7
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_dest." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 458,
"startColumn": 25,
"endLine": 458,
"endColumn": 48,
"byteLength": 23
}
}
}
]
}, {
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 459,
"startColumn": 31,
"endLine": 459,
"endColumn": 53,
"byteLength": 22
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": { "text": "assigns clause in function strxfrm." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 460,
"startColumn": 12,
"endLine": 460,
"endColumn": 26,
"byteLength": 14
}
}
}
]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
"from clause of term *(dest + (0 .. n - 1)) in function strxfrm."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 460,
"startColumn": 12,
"endLine": 460,
"endColumn": 26,
"byteLength": 14
}
}
} ]
},
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text": "from clause of term \\result in function strxfrm."
},
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 461,
"startColumn": 12,
"endLine": 461,
"endColumn": 19,
"byteLength": 7
}
}
}
]
}
],
"defaultSourceLanguage": "C",
"taxonomies": [
{
"name": "frama-c",
"rules": [
{
"id": "user-spec",
"shortDescription": {
"text": "User-written ACSL specification."
}
}
],
"contents": [ "nonLocalizedData" ]
}
]
}
]
}