diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 37fd6b824e300ae8820e6581f6eea17ac26aa84a..7c9df870307d17843e20bd6ecbdb3cc6163cf751 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -206,6 +206,7 @@ let gen_status ip =
Sarif_result.create ~ruleId:user_annot_id ~level ~locations ~message ()
let gen_statuses () =
+ let cmp = Property.Ordered_by_function.compare in
let f ip content =
let exclude =
is_alarm ip ||
@@ -213,7 +214,7 @@ let gen_statuses () =
in
if exclude then content else (gen_status ip) :: content
in
- List.rev (Property_status.fold f [])
+ List.rev (Property_status.fold_sorted ~cmp f [])
let gen_artifacts () =
let add_src_file f =
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
index 5855585658f0d7aee1f680420db13842a321ca1f..01038bb8a72d1d607ca386bebf1c5ed0289b8063 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
@@ -120,7 +120,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function printf." },
+ "message": {
+ "text": "reachability of stmt line 27 in getValueFromArray."
+ },
"locations": [
{
"physicalLocation": {
@@ -131,8 +133,8 @@
"region": {
"startLine": 27,
"endLine": 27,
- "endColumn": 6,
- "byteLength": 6
+ "endColumn": 38,
+ "byteLength": 38
}
}
}
@@ -165,9 +167,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function printf."
- },
+ "message": { "text": "behavior default! in function printf." },
"locations": [
{
"physicalLocation": {
@@ -189,7 +189,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function printf." },
+ "message": { "text": "assigns clause in function printf." },
"locations": [
{
"physicalLocation": {
@@ -212,7 +212,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "reachability of stmt line 27 in getValueFromArray."
+ "text": "from clause of term \\result in function printf."
},
"locations": [
{
@@ -224,8 +224,8 @@
"region": {
"startLine": 27,
"endLine": 27,
- "endColumn": 38,
- "byteLength": 38
+ "endColumn": 6,
+ "byteLength": 6
}
}
}
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
index fa8798f3f64f7402378d14b6c3f03f0c37f49400..f9bed3f4deea0fcb4cbf40cb71c14458a221fb72 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
@@ -50,22 +50,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term __fc_strtok_ptr in function strtok."
- },
+ "message": { "text": "MemChr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 261,
- "startColumn": 12,
- "endLine": 261,
- "endColumn": 27,
- "byteLength": 15
+ "startLine": 57,
+ "startColumn": 4,
+ "endLine": 59,
+ "endColumn": 62,
+ "byteLength": 134
}
}
}
@@ -75,22 +73,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strcpy."
- },
+ "message": { "text": "MemCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 356,
- "startColumn": 12,
- "endLine": 356,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 39,
+ "startColumn": 4,
+ "endLine": 42,
+ "endColumn": 70,
+ "byteLength": 170
}
}
}
@@ -100,20 +96,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strnlen." },
+ "message": { "text": "MemSet." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 135,
- "startColumn": 14,
- "endLine": 135,
- "endColumn": 21,
- "byteLength": 7
+ "startLine": 68,
+ "startColumn": 4,
+ "endLine": 70,
+ "endColumn": 63,
+ "byteLength": 135
}
}
}
@@ -123,20 +119,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strcasecmp." },
+ "message": { "text": "StrChr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 50,
- "startColumn": 11,
- "endLine": 50,
- "endColumn": 21,
- "byteLength": 10
+ "startLine": 168,
+ "startColumn": 4,
+ "endLine": 170,
+ "endColumn": 75,
+ "byteLength": 132
}
}
}
@@ -146,22 +142,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strpbrk."
- },
+ "message": { "text": "StrCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 214,
- "startColumn": 12,
- "endLine": 214,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 143,
+ "startColumn": 4,
+ "endLine": 147,
+ "endColumn": 63,
+ "byteLength": 170
}
}
}
@@ -171,22 +165,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strncat."
- },
+ "message": { "text": "StrLen." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 433,
- "startColumn": 12,
- "endLine": 433,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 132,
+ "startColumn": 4,
+ "endLine": 135,
+ "endColumn": 38,
+ "byteLength": 185
}
}
}
@@ -196,22 +188,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term *(s + (0 ..)) in function strtok_r."
- },
+ "message": { "text": "StrNCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 288,
- "startColumn": 10,
- "endLine": 288,
- "endColumn": 16,
- "byteLength": 6
+ "startLine": 155,
+ "startColumn": 4,
+ "endLine": 159,
+ "endColumn": 53,
+ "byteLength": 191
}
}
}
@@ -221,20 +211,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior partial in function strncpy." },
+ "message": { "text": "WMemChr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 378,
- "startColumn": 12,
- "endLine": 378,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 183,
+ "startColumn": 4,
+ "endLine": 185,
+ "endColumn": 63,
+ "byteLength": 143
}
}
}
@@ -244,22 +234,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strcat."
- },
+ "message": { "text": "WcsChr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 414,
- "startColumn": 12,
- "endLine": 414,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 266,
+ "startColumn": 4,
+ "endLine": 269,
+ "endColumn": 29,
+ "byteLength": 153
}
}
}
@@ -269,20 +257,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default in function strrchr." },
+ "message": { "text": "WcsCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 195,
- "startColumn": 12,
- "endLine": 195,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 240,
+ "startColumn": 4,
+ "endLine": 244,
+ "endColumn": 63,
+ "byteLength": 173
}
}
}
@@ -292,20 +280,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "dest_null_terminated." },
+ "message": { "text": "WcsLen." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 417,
- "startColumn": 34,
- "endLine": 417,
- "endColumn": 77,
- "byteLength": 43
+ "startLine": 230,
+ "startColumn": 4,
+ "endLine": 232,
+ "endColumn": 63,
+ "byteLength": 147
}
}
}
@@ -315,20 +303,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function bzero." },
+ "message": { "text": "WcsNCmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 40,
- "startColumn": 12,
- "endLine": 40,
- "endColumn": 17,
- "byteLength": 5
+ "startLine": 252,
+ "startColumn": 4,
+ "endLine": 256,
+ "endColumn": 53,
+ "byteLength": 194
}
}
}
@@ -338,20 +326,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior new_str in function strtok_r." },
+ "message": { "text": "dynamic_allocation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_alloc_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 327,
- "startColumn": 12,
- "endLine": 327,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 39,
+ "startColumn": 4,
+ "endLine": 41,
+ "endColumn": 61,
+ "byteLength": 110
}
}
}
@@ -361,22 +349,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term __fc_strtok_ptr in function strtok."
- },
+ "message": { "text": "memchr_def." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 272,
- "startColumn": 12,
- "endLine": 272,
- "endColumn": 27,
- "byteLength": 15
+ "startLine": 57,
+ "startColumn": 4,
+ "endLine": 59,
+ "endColumn": 62,
+ "byteLength": 134
}
}
}
@@ -386,23 +372,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) in function strncat."
- },
+ "message": { "text": "memcmp_strlen_left." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 439,
- "startColumn": 12,
- "endLine": 439,
- "endColumn": 48,
- "byteLength": 36
+ "startLine": 119,
+ "startColumn": 4,
+ "endLine": 121,
+ "endColumn": 77,
+ "byteLength": 148
}
}
}
@@ -412,20 +395,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": { "text": "memcmp_strlen_right." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 486,
- "startColumn": 29,
- "endLine": 486,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 123,
+ "startColumn": 4,
+ "endLine": 125,
+ "endColumn": 77,
+ "byteLength": 149
}
}
}
@@ -435,20 +418,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "room_string." },
+ "message": { "text": "memcmp_strlen_shift_left." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 438,
- "startColumn": 26,
- "endLine": 438,
- "endColumn": 64,
- "byteLength": 38
+ "startLine": 127,
+ "startColumn": 4,
+ "endLine": 130,
+ "endColumn": 38,
+ "byteLength": 184
}
}
}
@@ -458,20 +441,43 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s_or_delim_not_found." },
+ "message": { "text": "memcmp_strlen_shift_right." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 258,
- "startColumn": 6,
- "endLine": 260,
+ "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": 120
+ "byteLength": 170
}
}
}
@@ -481,7 +487,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_create_shift." },
+ "message": { "text": "memset_def." },
"locations": [
{
"physicalLocation": {
@@ -490,11 +496,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 230,
+ "startLine": 68,
"startColumn": 4,
- "endLine": 232,
+ "endLine": 70,
"endColumn": 63,
- "byteLength": 147
+ "byteLength": 135
}
}
}
@@ -504,7 +510,30 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "StrChr." },
+ "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": {
@@ -527,22 +556,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function memmove."
- },
+ "message": { "text": "strcmp_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 107,
- "startColumn": 12,
- "endLine": 107,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 143,
+ "startColumn": 4,
+ "endLine": 147,
+ "endColumn": 63,
+ "byteLength": 170
}
}
}
@@ -552,20 +579,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strchr." },
+ "message": { "text": "strlen_at_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 173,
- "startColumn": 12,
- "endLine": 173,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 92,
+ "startColumn": 4,
+ "endLine": 93,
+ "endColumn": 61,
+ "byteLength": 86
}
}
}
@@ -575,7 +602,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcscmp_zero." },
+ "message": { "text": "strlen_before_null." },
"locations": [
{
"physicalLocation": {
@@ -584,11 +611,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 240,
+ "startLine": 89,
"startColumn": 4,
- "endLine": 244,
- "endColumn": 63,
- "byteLength": 173
+ "endLine": 90,
+ "endColumn": 72,
+ "byteLength": 101
}
}
}
@@ -598,20 +625,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_valid_string." },
+ "message": { "text": "strlen_create." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 164,
- "startColumn": 33,
- "endLine": 164,
- "endColumn": 59,
- "byteLength": 26
+ "startLine": 111,
+ "startColumn": 4,
+ "endLine": 113,
+ "endColumn": 51,
+ "byteLength": 111
}
}
}
@@ -621,20 +648,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "equal_prefix." },
+ "message": { "text": "strlen_create_shift." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 376,
- "startColumn": 26,
- "endLine": 376,
- "endColumn": 60,
- "byteLength": 34
+ "startLine": 115,
+ "startColumn": 4,
+ "endLine": 117,
+ "endColumn": 62,
+ "byteLength": 143
}
}
}
@@ -644,20 +671,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_ptr." },
+ "message": { "text": "strlen_neg." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 358,
- "startColumn": 24,
- "endLine": 358,
- "endColumn": 39,
- "byteLength": 15
+ "startLine": 84,
+ "startColumn": 4,
+ "endLine": 87,
+ "endColumn": 22,
+ "byteLength": 109
}
}
}
@@ -667,20 +694,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_same_base." },
+ "message": { "text": "strlen_not_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 177,
- "startColumn": 30,
- "endLine": 177,
- "endColumn": 64,
- "byteLength": 34
+ "startLine": 95,
+ "startColumn": 4,
+ "endLine": 97,
+ "endColumn": 58,
+ "byteLength": 120
}
}
}
@@ -690,20 +717,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nstring_src." },
+ "message": { "text": "strlen_pos_or_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 423,
- "startColumn": 32,
- "endLine": 423,
- "endColumn": 58,
- "byteLength": 26
+ "startLine": 78,
+ "startColumn": 4,
+ "endLine": 82,
+ "endColumn": 40,
+ "byteLength": 169
}
}
}
@@ -713,20 +740,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strtok." },
+ "message": { "text": "strlen_shift." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 246,
- "startColumn": 10,
- "endLine": 246,
- "endColumn": 16,
- "byteLength": 6
+ "startLine": 107,
+ "startColumn": 4,
+ "endLine": 109,
+ "endColumn": 59,
+ "byteLength": 118
}
}
}
@@ -736,20 +763,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "equal_after_copy." },
+ "message": { "text": "strlen_sup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 373,
- "startColumn": 30,
- "endLine": 373,
+ "startLine": 103,
+ "startColumn": 4,
+ "endLine": 105,
"endColumn": 51,
- "byteLength": 21
+ "byteLength": 108
}
}
}
@@ -759,20 +786,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_same_base." },
+ "message": { "text": "strlen_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 79,
- "startColumn": 30,
- "endLine": 79,
- "endColumn": 66,
- "byteLength": 36
+ "startLine": 99,
+ "startColumn": 4,
+ "endLine": 101,
+ "endColumn": 59,
+ "byteLength": 117
}
}
}
@@ -782,22 +809,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strsignal."
- },
+ "message": { "text": "strncmp_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 518,
- "startColumn": 12,
- "endLine": 518,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 155,
+ "startColumn": 4,
+ "endLine": 159,
+ "endColumn": 53,
+ "byteLength": 191
}
}
}
@@ -807,20 +832,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_src." },
+ "message": { "text": "wcschr_def." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 459,
- "startColumn": 31,
- "endLine": 459,
- "endColumn": 53,
- "byteLength": 22
+ "startLine": 266,
+ "startColumn": 4,
+ "endLine": 269,
+ "endColumn": 29,
+ "byteLength": 153
}
}
}
@@ -830,22 +855,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strdup."
- },
+ "message": { "text": "wcscmp_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 480,
- "startColumn": 12,
- "endLine": 480,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 240,
+ "startColumn": 4,
+ "endLine": 244,
+ "endColumn": 63,
+ "byteLength": 173
}
}
}
@@ -855,20 +878,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strcoll." },
+ "message": { "text": "wcslen_at_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 155,
- "startColumn": 11,
- "endLine": 155,
- "endColumn": 18,
- "byteLength": 7
+ "startLine": 207,
+ "startColumn": 4,
+ "endLine": 208,
+ "endColumn": 65,
+ "byteLength": 90
}
}
}
@@ -878,20 +901,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null_or_same_base." },
+ "message": { "text": "wcslen_before_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 171,
+ "startLine": 204,
"startColumn": 4,
- "endLine": 171,
- "endColumn": 60,
- "byteLength": 56
+ "endLine": 205,
+ "endColumn": 76,
+ "byteLength": 105
}
}
}
@@ -901,20 +924,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": { "text": "wcslen_create." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 131,
- "startColumn": 29,
- "endLine": 131,
- "endColumn": 53,
- "byteLength": 24
+ "startLine": 226,
+ "startColumn": 4,
+ "endLine": 228,
+ "endColumn": 52,
+ "byteLength": 115
}
}
}
@@ -924,22 +947,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strndup."
- },
+ "message": { "text": "wcslen_create_shift." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 493,
- "startColumn": 12,
- "endLine": 493,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 230,
+ "startColumn": 4,
+ "endLine": 232,
+ "endColumn": 63,
+ "byteLength": 147
}
}
}
@@ -949,20 +970,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "not_first_call." },
+ "message": { "text": "wcslen_neg." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 268,
- "startColumn": 29,
- "endLine": 268,
- "endColumn": 53,
- "byteLength": 24
+ "startLine": 199,
+ "startColumn": 4,
+ "endLine": 202,
+ "endColumn": 22,
+ "byteLength": 113
}
}
}
@@ -972,20 +993,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function memchr." },
+ "message": { "text": "wcslen_not_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 88,
- "startColumn": 12,
- "endLine": 88,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 210,
+ "startColumn": 4,
+ "endLine": 212,
+ "endColumn": 59,
+ "byteLength": 124
}
}
}
@@ -995,22 +1016,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term *saveptr in function strtok_r."
- },
+ "message": { "text": "wcslen_pos_or_null." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 316,
- "startColumn": 12,
- "endLine": 316,
- "endColumn": 20,
- "byteLength": 8
+ "startLine": 193,
+ "startColumn": 4,
+ "endLine": 197,
+ "endColumn": 41,
+ "byteLength": 174
}
}
}
@@ -1020,20 +1039,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "separation." },
+ "message": { "text": "wcslen_shift." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 95,
- "startColumn": 4,
- "endLine": 95,
- "endColumn": 62,
- "byteLength": 58
+ "startLine": 222,
+ "startColumn": 4,
+ "endLine": 224,
+ "endColumn": 55,
+ "byteLength": 117
}
}
}
@@ -1043,20 +1062,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "room_nstring." },
+ "message": { "text": "wcslen_sup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 364,
- "startColumn": 27,
- "endLine": 364,
- "endColumn": 50,
- "byteLength": 23
+ "startLine": 218,
+ "startColumn": 4,
+ "endLine": 220,
+ "endColumn": 52,
+ "byteLength": 112
}
}
}
@@ -1066,20 +1085,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "acsl_c_equiv." },
+ "message": { "text": "wcslen_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 127,
- "startColumn": 26,
- "endLine": 127,
- "endColumn": 46,
- "byteLength": 20
+ "startLine": 214,
+ "startColumn": 4,
+ "endLine": 216,
+ "endColumn": 60,
+ "byteLength": 121
}
}
}
@@ -1089,23 +1108,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *(dest + (0 .. n - 1)) in function strncpy."
- },
+ "message": { "text": "wcsncmp_zero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 367,
- "startColumn": 12,
- "endLine": 367,
- "endColumn": 26,
- "byteLength": 14
+ "startLine": 252,
+ "startColumn": 4,
+ "endLine": 256,
+ "endColumn": 53,
+ "byteLength": 194
}
}
}
@@ -1115,20 +1131,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "initialization." },
+ "message": { "text": "wmemchr_def." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/__fc_string_axiomatic.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 370,
- "startColumn": 28,
- "endLine": 370,
- "endColumn": 57,
- "byteLength": 29
+ "startLine": 183,
+ "startColumn": 4,
+ "endLine": 185,
+ "endColumn": 63,
+ "byteLength": 143
}
}
}
@@ -1138,20 +1154,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "memcmp_strlen_left." },
+ "message": { "text": "behavior default! in function bzero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 119,
- "startColumn": 4,
- "endLine": 121,
- "endColumn": 77,
- "byteLength": 148
+ "startLine": 40,
+ "startColumn": 12,
+ "endLine": 40,
+ "endColumn": 17,
+ "byteLength": 5
}
}
}
@@ -1161,20 +1177,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strlcat." },
+ "message": { "text": "valid_memory_area." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 451,
- "startColumn": 12,
- "endLine": 451,
- "endColumn": 33,
- "byteLength": 21
+ "startLine": 36,
+ "startColumn": 32,
+ "endLine": 36,
+ "endColumn": 63,
+ "byteLength": 31
}
}
}
@@ -1184,20 +1200,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "danglingness." },
+ "message": { "text": "s_initialized." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 74,
- "startColumn": 8,
- "endLine": 75,
- "endColumn": 61,
- "byteLength": 80
+ "startLine": 38,
+ "startColumn": 39,
+ "endLine": 38,
+ "endColumn": 75,
+ "byteLength": 36
}
}
}
@@ -1207,20 +1223,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_delim." },
+ "message": { "text": "zero_initialized." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 245,
- "startColumn": 31,
- "endLine": 245,
- "endColumn": 55,
- "byteLength": 24
+ "startLine": 39,
+ "startColumn": 28,
+ "endLine": 39,
+ "endColumn": 63,
+ "byteLength": 35
}
}
}
@@ -1230,20 +1246,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "allocation." },
+ "message": { "text": "assigns clause in function bzero." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 475,
- "startColumn": 24,
- "endLine": 475,
- "endColumn": 49,
- "byteLength": 25
+ "startLine": 37,
+ "startColumn": 10,
+ "endLine": 37,
+ "endColumn": 31,
+ "byteLength": 21
}
}
}
@@ -1253,20 +1269,23 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "memcmp_strlen_right." },
+ "message": {
+ "text":
+ "from clause of term *((char *)s + (0 .. n - 1)) in function bzero."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 123,
- "startColumn": 4,
- "endLine": 125,
- "endColumn": 77,
- "byteLength": 149
+ "startLine": 37,
+ "startColumn": 10,
+ "endLine": 37,
+ "endColumn": 31,
+ "byteLength": 21
}
}
}
@@ -1276,20 +1295,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null." },
+ "message": {
+ "text": "specialization of valid_string_s at stmt 2."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
- "uriBaseId": "FRAMAC_SHARE"
+ "uri": "tests/sarif/libc.c",
+ "uriBaseId": "PWD"
},
"region": {
- "startLine": 190,
- "startColumn": 25,
- "endLine": 190,
- "endColumn": 41,
- "byteLength": 16
+ "startLine": 13,
+ "startColumn": 10,
+ "endLine": 13,
+ "endColumn": 19,
+ "byteLength": 9
}
}
}
@@ -1299,10 +1320,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *((char *)dest + (0 .. n - 1)) in function memcpy."
- },
+ "message": { "text": "behavior default! in function memchr." },
"locations": [
{
"physicalLocation": {
@@ -1311,11 +1329,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 96,
+ "startLine": 88,
"startColumn": 12,
- "endLine": 96,
- "endColumn": 35,
- "byteLength": 23
+ "endLine": 88,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -1325,7 +1343,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "initialization." },
+ "message": { "text": "behavior found in function memchr." },
"locations": [
{
"physicalLocation": {
@@ -1334,11 +1352,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 71,
- "startColumn": 8,
- "endLine": 72,
- "endColumn": 71,
- "byteLength": 116
+ "startLine": 88,
+ "startColumn": 12,
+ "endLine": 88,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -1348,7 +1366,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s1." },
+ "message": { "text": "behavior not_found in function memchr." },
"locations": [
{
"physicalLocation": {
@@ -1357,11 +1375,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 151,
- "startColumn": 30,
- "endLine": 151,
- "endColumn": 51,
- "byteLength": 21
+ "startLine": 88,
+ "startColumn": 12,
+ "endLine": 88,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -1371,7 +1389,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null." },
+ "message": { "text": "valid." },
"locations": [
{
"physicalLocation": {
@@ -1380,11 +1398,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 168,
- "startColumn": 25,
- "endLine": 168,
- "endColumn": 41,
- "byteLength": 16
+ "startLine": 68,
+ "startColumn": 9,
+ "endLine": 69,
+ "endColumn": 74,
+ "byteLength": 100
}
}
}
@@ -1394,7 +1412,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "danglingness." },
+ "message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
@@ -1403,11 +1421,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 59,
- "startColumn": 30,
- "endLine": 59,
- "endColumn": 49,
- "byteLength": 19
+ "startLine": 71,
+ "startColumn": 8,
+ "endLine": 72,
+ "endColumn": 71,
+ "byteLength": 116
}
}
}
@@ -1417,9 +1435,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strerror."
- },
+ "message": { "text": "danglingness." },
"locations": [
{
"physicalLocation": {
@@ -1428,11 +1444,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 342,
- "startColumn": 12,
- "endLine": 342,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 74,
+ "startColumn": 8,
+ "endLine": 75,
+ "endColumn": 61,
+ "byteLength": 80
}
}
}
@@ -1442,20 +1458,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_shift." },
+ "message": { "text": "char_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
- "uriBaseId": "FRAMAC_SHARE"
- },
- "region": {
- "startLine": 107,
- "startColumn": 4,
- "endLine": 109,
- "endColumn": 59,
- "byteLength": 118
+ "uri": "libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 78,
+ "startColumn": 24,
+ "endLine": 78,
+ "endColumn": 44,
+ "byteLength": 20
}
}
}
@@ -1465,7 +1481,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior not_found in function strrchr." },
+ "message": { "text": "char_not_found." },
"locations": [
{
"physicalLocation": {
@@ -1474,11 +1490,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 195,
- "startColumn": 12,
- "endLine": 195,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 85,
+ "startColumn": 28,
+ "endLine": 85,
+ "endColumn": 49,
+ "byteLength": 21
}
}
}
@@ -1488,7 +1504,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "cannot_allocate." },
+ "message": { "text": "result_same_base." },
"locations": [
{
"physicalLocation": {
@@ -1497,11 +1513,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 501,
- "startColumn": 29,
- "endLine": 501,
- "endColumn": 64,
- "byteLength": 35
+ "startLine": 79,
+ "startColumn": 30,
+ "endLine": 79,
+ "endColumn": 66,
+ "byteLength": 36
}
}
}
@@ -1511,7 +1527,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strcasestr." },
+ "message": { "text": "result_char." },
"locations": [
{
"physicalLocation": {
@@ -1520,11 +1536,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 239,
- "startColumn": 12,
- "endLine": 239,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 80,
+ "startColumn": 25,
+ "endLine": 80,
+ "endColumn": 45,
+ "byteLength": 20
}
}
}
@@ -1534,7 +1550,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "ptr_subset." },
+ "message": { "text": "result_in_str." },
"locations": [
{
"physicalLocation": {
@@ -1543,11 +1559,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 265,
- "startColumn": 24,
- "endLine": 265,
- "endColumn": 57,
- "byteLength": 33
+ "startLine": 81,
+ "startColumn": 27,
+ "endLine": 83,
+ "endColumn": 54,
+ "byteLength": 120
}
}
}
@@ -1557,7 +1573,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strncpy." },
+ "message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
@@ -1566,11 +1582,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 367,
- "startColumn": 12,
- "endLine": 367,
- "endColumn": 26,
- "byteLength": 14
+ "startLine": 86,
+ "startColumn": 25,
+ "endLine": 86,
+ "endColumn": 41,
+ "byteLength": 16
}
}
}
@@ -1580,7 +1596,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_s1." },
+ "message": { "text": "assigns clause in function memchr." },
"locations": [
{
"physicalLocation": {
@@ -1589,11 +1605,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 55,
- "startColumn": 23,
- "endLine": 55,
- "endColumn": 49,
- "byteLength": 26
+ "startLine": 88,
+ "startColumn": 12,
+ "endLine": 88,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -1603,7 +1619,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior complete in function strncat." },
+ "message": {
+ "text": "from clause of term \\result in function memchr."
+ },
"locations": [
{
"physicalLocation": {
@@ -1612,11 +1630,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 444,
+ "startLine": 76,
"startColumn": 12,
- "endLine": 444,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 76,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -1626,7 +1644,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": { "text": "behavior default! in function memcmp." },
"locations": [
{
"physicalLocation": {
@@ -1635,11 +1653,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 125,
- "startColumn": 29,
- "endLine": 125,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 65,
+ "startColumn": 11,
+ "endLine": 65,
+ "endColumn": 17,
+ "byteLength": 6
}
}
}
@@ -1649,9 +1667,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strcoll."
- },
+ "message": { "text": "valid_s1." },
"locations": [
{
"physicalLocation": {
@@ -1660,11 +1676,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 153,
- "startColumn": 12,
- "endLine": 153,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 55,
+ "startColumn": 23,
+ "endLine": 55,
+ "endColumn": 49,
+ "byteLength": 26
}
}
}
@@ -1674,9 +1690,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "result_valid_string_bounded_and_same_prefix."
- },
+ "message": { "text": "valid_s2." },
"locations": [
{
"physicalLocation": {
@@ -1685,11 +1699,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 497,
- "startColumn": 4,
- "endLine": 499,
- "endColumn": 29,
- "byteLength": 124
+ "startLine": 56,
+ "startColumn": 23,
+ "endLine": 56,
+ "endColumn": 49,
+ "byteLength": 26
}
}
}
@@ -1699,7 +1713,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
@@ -1708,11 +1722,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 204,
- "startColumn": 29,
- "endLine": 204,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 57,
+ "startColumn": 32,
+ "endLine": 57,
+ "endColumn": 68,
+ "byteLength": 36
}
}
}
@@ -1722,7 +1736,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior allocation in function strndup." },
+ "message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
@@ -1731,11 +1745,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 506,
- "startColumn": 12,
- "endLine": 506,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 58,
+ "startColumn": 32,
+ "endLine": 58,
+ "endColumn": 68,
+ "byteLength": 36
}
}
}
@@ -1745,10 +1759,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *(__fc_strtok_ptr + (0 ..)) in function strtok."
- },
+ "message": { "text": "danglingness." },
"locations": [
{
"physicalLocation": {
@@ -1757,11 +1768,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 248,
- "startColumn": 10,
- "endLine": 248,
- "endColumn": 30,
- "byteLength": 20
+ "startLine": 59,
+ "startColumn": 30,
+ "endLine": 59,
+ "endColumn": 49,
+ "byteLength": 19
}
}
}
@@ -1771,7 +1782,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "char_not_found." },
+ "message": { "text": "danglingness." },
"locations": [
{
"physicalLocation": {
@@ -1780,11 +1791,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 189,
- "startColumn": 28,
- "endLine": 189,
- "endColumn": 40,
- "byteLength": 12
+ "startLine": 60,
+ "startColumn": 30,
+ "endLine": 60,
+ "endColumn": 49,
+ "byteLength": 19
}
}
}
@@ -1794,7 +1805,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "disjoint clause in function strtok." },
+ "message": { "text": "logic_spec." },
"locations": [
{
"physicalLocation": {
@@ -1803,11 +1814,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 283,
- "startColumn": 12,
- "endLine": 283,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 63,
+ "startColumn": 24,
+ "endLine": 63,
+ "endColumn": 73,
+ "byteLength": 49
}
}
}
@@ -1817,9 +1828,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strndup."
- },
+ "message": { "text": "assigns clause in function memcmp." },
"locations": [
{
"physicalLocation": {
@@ -1828,11 +1837,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 488,
- "startColumn": 12,
- "endLine": 488,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 65,
+ "startColumn": 11,
+ "endLine": 65,
+ "endColumn": 17,
+ "byteLength": 6
}
}
}
@@ -1842,7 +1851,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "s_not_null." },
+ "message": {
+ "text": "from clause of term \\result in function memcmp."
+ },
"locations": [
{
"physicalLocation": {
@@ -1851,11 +1862,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 256,
- "startColumn": 24,
- "endLine": 256,
- "endColumn": 34,
- "byteLength": 10
+ "startLine": 61,
+ "startColumn": 12,
+ "endLine": 61,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -1865,7 +1876,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid." },
+ "message": { "text": "behavior default! in function memcpy." },
"locations": [
{
"physicalLocation": {
@@ -1874,11 +1885,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 68,
- "startColumn": 9,
- "endLine": 69,
- "endColumn": 74,
- "byteLength": 100
+ "startLine": 101,
+ "startColumn": 12,
+ "endLine": 101,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -1888,7 +1899,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_accept." },
+ "message": { "text": "valid_dest." },
"locations": [
{
"physicalLocation": {
@@ -1897,11 +1908,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 213,
- "startColumn": 34,
- "endLine": 213,
- "endColumn": 59,
- "byteLength": 25
+ "startLine": 92,
+ "startColumn": 25,
+ "endLine": 92,
+ "endColumn": 48,
+ "byteLength": 23
}
}
}
@@ -1911,7 +1922,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior not_found in function memchr." },
+ "message": { "text": "valid_src." },
"locations": [
{
"physicalLocation": {
@@ -1920,11 +1931,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 88,
- "startColumn": 12,
- "endLine": 88,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 93,
+ "startColumn": 24,
+ "endLine": 93,
+ "endColumn": 51,
+ "byteLength": 27
}
}
}
@@ -1934,7 +1945,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strspn." },
+ "message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
@@ -1943,11 +1954,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 206,
- "startColumn": 12,
- "endLine": 206,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 95,
+ "startColumn": 4,
+ "endLine": 95,
+ "endColumn": 62,
+ "byteLength": 58
}
}
}
@@ -1957,7 +1968,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "initialization." },
+ "message": { "text": "copied_contents." },
"locations": [
{
"physicalLocation": {
@@ -1966,11 +1977,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 58,
- "startColumn": 32,
- "endLine": 58,
- "endColumn": 68,
- "byteLength": 36
+ "startLine": 98,
+ "startColumn": 29,
+ "endLine": 98,
+ "endColumn": 76,
+ "byteLength": 47
}
}
}
@@ -1980,20 +1991,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_before_null." },
+ "message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 89,
- "startColumn": 4,
- "endLine": 90,
- "endColumn": 72,
- "byteLength": 101
+ "startLine": 99,
+ "startColumn": 24,
+ "endLine": 99,
+ "endColumn": 39,
+ "byteLength": 15
}
}
}
@@ -2003,7 +2014,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strlen." },
+ "message": { "text": "assigns clause in function memcpy." },
"locations": [
{
"physicalLocation": {
@@ -2012,11 +2023,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 129,
- "startColumn": 14,
- "endLine": 129,
- "endColumn": 20,
- "byteLength": 6
+ "startLine": 96,
+ "startColumn": 12,
+ "endLine": 96,
+ "endColumn": 35,
+ "byteLength": 23
}
}
}
@@ -2026,7 +2037,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strlcpy." },
+ "message": {
+ "text":
+ "from clause of term *((char *)dest + (0 .. n - 1)) in function memcpy."
+ },
"locations": [
{
"physicalLocation": {
@@ -2035,11 +2049,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 393,
- "startColumn": 7,
- "endLine": 393,
- "endColumn": 14,
- "byteLength": 7
+ "startLine": 96,
+ "startColumn": 12,
+ "endLine": 96,
+ "endColumn": 35,
+ "byteLength": 23
}
}
}
@@ -2049,7 +2063,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "separation." },
+ "message": {
+ "text": "from clause of term \\result in function memcpy."
+ },
"locations": [
{
"physicalLocation": {
@@ -2058,11 +2074,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 354,
- "startColumn": 4,
- "endLine": 354,
- "endColumn": 59,
- "byteLength": 55
+ "startLine": 97,
+ "startColumn": 12,
+ "endLine": 97,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -2072,7 +2088,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default in function strchr." },
+ "message": { "text": "behavior default! in function memmove." },
"locations": [
{
"physicalLocation": {
@@ -2081,9 +2097,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 173,
+ "startLine": 111,
"startColumn": 12,
- "endLine": 173,
+ "endLine": 111,
"endColumn": 13,
"byteLength": 1
}
@@ -2095,7 +2111,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "complete clause in function strtok_r." },
+ "message": { "text": "valid_dest." },
"locations": [
{
"physicalLocation": {
@@ -2104,11 +2120,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 327,
- "startColumn": 12,
- "endLine": 327,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 104,
+ "startColumn": 25,
+ "endLine": 104,
+ "endColumn": 48,
+ "byteLength": 23
}
}
}
@@ -2118,10 +2134,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."
- },
+ "message": { "text": "valid_src." },
"locations": [
{
"physicalLocation": {
@@ -2130,11 +2143,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 425,
- "startColumn": 12,
- "endLine": 425,
- "endColumn": 50,
- "byteLength": 38
+ "startLine": 105,
+ "startColumn": 24,
+ "endLine": 105,
+ "endColumn": 51,
+ "byteLength": 27
}
}
}
@@ -2144,7 +2157,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior no_allocation in function strdup." },
+ "message": { "text": "copied_contents." },
"locations": [
{
"physicalLocation": {
@@ -2153,11 +2166,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 484,
- "startColumn": 12,
- "endLine": 484,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 108,
+ "startColumn": 29,
+ "endLine": 108,
+ "endColumn": 76,
+ "byteLength": 47
}
}
}
@@ -2167,7 +2180,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strcat." },
+ "message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
@@ -2176,11 +2189,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 420,
- "startColumn": 12,
- "endLine": 420,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 109,
+ "startColumn": 24,
+ "endLine": 109,
+ "endColumn": 39,
+ "byteLength": 15
}
}
}
@@ -2190,20 +2203,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "StrCmp." },
+ "message": { "text": "assigns clause in function memmove." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 143,
- "startColumn": 4,
- "endLine": 147,
- "endColumn": 63,
- "byteLength": 170
+ "startLine": 106,
+ "startColumn": 12,
+ "endLine": 106,
+ "endColumn": 35,
+ "byteLength": 23
}
}
}
@@ -2213,20 +2226,23 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_at_null." },
+ "message": {
+ "text":
+ "from clause of term *((char *)dest + (0 .. n - 1)) in function memmove."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 92,
- "startColumn": 4,
- "endLine": 93,
- "endColumn": 61,
- "byteLength": 86
+ "startLine": 106,
+ "startColumn": 12,
+ "endLine": 106,
+ "endColumn": 35,
+ "byteLength": 23
}
}
}
@@ -2237,8 +2253,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text":
- "from clause of term *(*saveptr + (0 ..)) in function strtok_r."
+ "text": "from clause of term \\result in function memmove."
},
"locations": [
{
@@ -2248,11 +2263,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 290,
- "startColumn": 10,
- "endLine": 290,
- "endColumn": 25,
- "byteLength": 15
+ "startLine": 107,
+ "startColumn": 12,
+ "endLine": 107,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -2262,7 +2277,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strspn." },
+ "message": { "text": "behavior default! in function memset." },
"locations": [
{
"physicalLocation": {
@@ -2271,11 +2286,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 210,
- "startColumn": 14,
- "endLine": 210,
- "endColumn": 20,
- "byteLength": 6
+ "startLine": 121,
+ "startColumn": 12,
+ "endLine": 121,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -2285,7 +2300,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s2." },
+ "message": { "text": "valid_s." },
"locations": [
{
"physicalLocation": {
@@ -2294,11 +2309,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 138,
- "startColumn": 30,
- "endLine": 138,
- "endColumn": 51,
- "byteLength": 21
+ "startLine": 115,
+ "startColumn": 22,
+ "endLine": 115,
+ "endColumn": 42,
+ "byteLength": 20
}
}
}
@@ -2308,7 +2323,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_char." },
+ "message": { "text": "acsl_c_equiv." },
"locations": [
{
"physicalLocation": {
@@ -2317,10 +2332,10 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 80,
- "startColumn": 25,
- "endLine": 80,
- "endColumn": 45,
+ "startLine": 118,
+ "startColumn": 26,
+ "endLine": 118,
+ "endColumn": 46,
"byteLength": 20
}
}
@@ -2331,7 +2346,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strlcpy." },
+ "message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
@@ -2340,10 +2355,10 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 388,
- "startColumn": 12,
- "endLine": 388,
- "endColumn": 24,
+ "startLine": 119,
+ "startColumn": 24,
+ "endLine": 119,
+ "endColumn": 36,
"byteLength": 12
}
}
@@ -2354,23 +2369,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *((char *)s + (0 .. n - 1)) in function bzero."
- },
+ "message": { "text": "assigns clause in function memset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 37,
- "startColumn": 10,
- "endLine": 37,
- "endColumn": 31,
- "byteLength": 21
+ "startLine": 116,
+ "startColumn": 12,
+ "endLine": 116,
+ "endColumn": 32,
+ "byteLength": 20
}
}
}
@@ -2380,7 +2392,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_in_str." },
+ "message": {
+ "text":
+ "from clause of term *((char *)s + (0 .. n - 1)) in function memset."
+ },
"locations": [
{
"physicalLocation": {
@@ -2389,11 +2404,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 81,
- "startColumn": 27,
- "endLine": 83,
- "endColumn": 54,
- "byteLength": 120
+ "startLine": 116,
+ "startColumn": 12,
+ "endLine": 116,
+ "endColumn": 32,
+ "byteLength": 20
}
}
}
@@ -2403,7 +2418,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "char_found." },
+ "message": {
+ "text": "from clause of term \\result in function memset."
+ },
"locations": [
{
"physicalLocation": {
@@ -2412,11 +2429,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 78,
- "startColumn": 24,
- "endLine": 78,
- "endColumn": 44,
- "byteLength": 20
+ "startLine": 117,
+ "startColumn": 12,
+ "endLine": 117,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -2426,20 +2443,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "MemChr." },
+ "message": { "text": "behavior default! in function stpcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 57,
- "startColumn": 4,
- "endLine": 59,
- "endColumn": 62,
- "byteLength": 134
+ "startLine": 405,
+ "startColumn": 12,
+ "endLine": 405,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -2449,9 +2466,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strtok_r."
- },
+ "message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
@@ -2460,11 +2475,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 319,
- "startColumn": 12,
- "endLine": 319,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 396,
+ "startColumn": 31,
+ "endLine": 396,
+ "endColumn": 53,
+ "byteLength": 22
}
}
}
@@ -2474,7 +2489,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "char_found." },
+ "message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
@@ -2483,11 +2498,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 184,
- "startColumn": 24,
- "endLine": 184,
- "endColumn": 35,
- "byteLength": 11
+ "startLine": 397,
+ "startColumn": 26,
+ "endLine": 397,
+ "endColumn": 55,
+ "byteLength": 29
}
}
}
@@ -2497,9 +2512,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strtok."
- },
+ "message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
@@ -2508,11 +2521,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 250,
- "startColumn": 10,
- "endLine": 250,
- "endColumn": 17,
- "byteLength": 7
+ "startLine": 399,
+ "startColumn": 4,
+ "endLine": 399,
+ "endColumn": 59,
+ "byteLength": 55
}
}
}
@@ -2522,7 +2535,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_src." },
+ "message": { "text": "equal_contents." },
"locations": [
{
"physicalLocation": {
@@ -2531,11 +2544,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 396,
- "startColumn": 31,
- "endLine": 396,
- "endColumn": 53,
- "byteLength": 22
+ "startLine": 402,
+ "startColumn": 28,
+ "endLine": 402,
+ "endColumn": 49,
+ "byteLength": 21
}
}
}
@@ -2545,7 +2558,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strtok." },
+ "message": { "text": "points_to_end." },
"locations": [
{
"physicalLocation": {
@@ -2554,11 +2567,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 269,
- "startColumn": 12,
- "endLine": 269,
- "endColumn": 32,
- "byteLength": 20
+ "startLine": 403,
+ "startColumn": 27,
+ "endLine": 403,
+ "endColumn": 57,
+ "byteLength": 30
}
}
}
@@ -2568,20 +2581,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_at_null." },
+ "message": { "text": "assigns clause in function stpcpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 207,
- "startColumn": 4,
- "endLine": 208,
- "endColumn": 65,
- "byteLength": 90
+ "startLine": 400,
+ "startColumn": 12,
+ "endLine": 400,
+ "endColumn": 32,
+ "byteLength": 20
}
}
}
@@ -2591,7 +2604,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_valid_string." },
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. strlen{Old}(src))) in function stpcpy."
+ },
"locations": [
{
"physicalLocation": {
@@ -2600,11 +2616,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 187,
- "startColumn": 33,
- "endLine": 187,
- "endColumn": 59,
- "byteLength": 26
+ "startLine": 400,
+ "startColumn": 12,
+ "endLine": 400,
+ "endColumn": 32,
+ "byteLength": 20
}
}
}
@@ -2614,7 +2630,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_src_fits." },
+ "message": {
+ "text": "from clause of term \\result in function stpcpy."
+ },
"locations": [
{
"physicalLocation": {
@@ -2623,11 +2641,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 429,
- "startColumn": 35,
- "endLine": 429,
- "endColumn": 77,
- "byteLength": 42
+ "startLine": 401,
+ "startColumn": 12,
+ "endLine": 401,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -2637,20 +2655,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null_or_in_haystack." },
+ "message": { "text": "behavior default! in function strcasecmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 236,
- "startColumn": 4,
- "endLine": 237,
- "endColumn": 65,
- "byteLength": 82
+ "startLine": 50,
+ "startColumn": 11,
+ "endLine": 50,
+ "endColumn": 21,
+ "byteLength": 10
}
}
}
@@ -2660,20 +2678,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function memset." },
+ "message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 121,
- "startColumn": 12,
- "endLine": 121,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 46,
+ "startColumn": 28,
+ "endLine": 46,
+ "endColumn": 49,
+ "byteLength": 21
}
}
}
@@ -2683,20 +2701,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_first_occur." },
+ "message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 165,
- "startColumn": 32,
- "endLine": 165,
- "endColumn": 79,
- "byteLength": 47
+ "startLine": 47,
+ "startColumn": 28,
+ "endLine": 47,
+ "endColumn": 49,
+ "byteLength": 21
}
}
}
@@ -2706,20 +2724,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strtok_r." },
+ "message": { "text": "assigns clause in function strcasecmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 313,
- "startColumn": 12,
- "endLine": 313,
- "endColumn": 27,
- "byteLength": 15
+ "startLine": 50,
+ "startColumn": 11,
+ "endLine": 50,
+ "endColumn": 21,
+ "byteLength": 10
}
}
}
@@ -2729,20 +2747,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "room_string." },
+ "message": {
+ "text": "from clause of term \\result in function strcasecmp."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 430,
- "startColumn": 26,
- "endLine": 430,
- "endColumn": 74,
- "byteLength": 48
+ "startLine": 48,
+ "startColumn": 10,
+ "endLine": 48,
+ "endColumn": 17,
+ "byteLength": 7
}
}
}
@@ -2752,7 +2772,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "initialization." },
+ "message": { "text": "behavior default! in function strcasestr." },
"locations": [
{
"physicalLocation": {
@@ -2761,11 +2781,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 312,
- "startColumn": 37,
- "endLine": 312,
- "endColumn": 58,
- "byteLength": 21
+ "startLine": 239,
+ "startColumn": 12,
+ "endLine": 239,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -2775,20 +2795,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "WMemChr." },
+ "message": { "text": "valid_string_haystack." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 183,
- "startColumn": 4,
- "endLine": 185,
+ "startLine": 231,
+ "startColumn": 36,
+ "endLine": 231,
"endColumn": 63,
- "byteLength": 143
+ "byteLength": 27
}
}
}
@@ -2798,7 +2818,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strcmp." },
+ "message": { "text": "valid_string_needle." },
"locations": [
{
"physicalLocation": {
@@ -2807,11 +2827,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 142,
- "startColumn": 11,
- "endLine": 142,
- "endColumn": 17,
- "byteLength": 6
+ "startLine": 232,
+ "startColumn": 34,
+ "endLine": 232,
+ "endColumn": 59,
+ "byteLength": 25
}
}
}
@@ -2821,20 +2841,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s1." },
+ "message": { "text": "result_null_or_in_haystack." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 46,
- "startColumn": 28,
- "endLine": 46,
- "endColumn": 49,
- "byteLength": 21
+ "startLine": 236,
+ "startColumn": 4,
+ "endLine": 237,
+ "endColumn": 65,
+ "byteLength": 82
}
}
}
@@ -2844,20 +2864,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function bzero." },
+ "message": { "text": "assigns clause in function strcasestr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 37,
- "startColumn": 10,
- "endLine": 37,
- "endColumn": 31,
- "byteLength": 21
+ "startLine": 239,
+ "startColumn": 12,
+ "endLine": 239,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -2868,8 +2888,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text":
- "from clause of term *(dest + (0 .. strlen{Old}(src))) in function strcpy."
+ "text": "from clause of term \\result in function strcasestr."
},
"locations": [
{
@@ -2879,11 +2898,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 355,
+ "startLine": 233,
"startColumn": 12,
- "endLine": 355,
- "endColumn": 32,
- "byteLength": 20
+ "endLine": 233,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -2893,7 +2912,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_delim." },
+ "message": { "text": "behavior default! in function strcat." },
"locations": [
{
"physicalLocation": {
@@ -2902,11 +2921,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 286,
- "startColumn": 31,
- "endLine": 286,
- "endColumn": 55,
- "byteLength": 24
+ "startLine": 420,
+ "startColumn": 12,
+ "endLine": 420,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -2916,7 +2935,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior partial in function strncat." },
+ "message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
@@ -2925,11 +2944,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 444,
- "startColumn": 12,
- "endLine": 444,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 408,
+ "startColumn": 31,
+ "endLine": 408,
+ "endColumn": 53,
+ "byteLength": 22
}
}
}
@@ -2939,7 +2958,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_ptr." },
+ "message": { "text": "valid_string_dest." },
"locations": [
{
"physicalLocation": {
@@ -2948,11 +2967,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 418,
- "startColumn": 24,
- "endLine": 418,
- "endColumn": 39,
- "byteLength": 15
+ "startLine": 409,
+ "startColumn": 32,
+ "endLine": 409,
+ "endColumn": 50,
+ "byteLength": 18
}
}
}
@@ -2962,7 +2981,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_ptr." },
+ "message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
@@ -2971,11 +2990,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 109,
- "startColumn": 24,
- "endLine": 109,
- "endColumn": 39,
- "byteLength": 15
+ "startLine": 410,
+ "startColumn": 26,
+ "endLine": 410,
+ "endColumn": 70,
+ "byteLength": 44
}
}
}
@@ -2985,7 +3004,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strdup." },
+ "message": { "text": "sum_of_lengths." },
"locations": [
{
"physicalLocation": {
@@ -2994,11 +3013,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 484,
- "startColumn": 12,
- "endLine": 484,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 413,
+ "startColumn": 28,
+ "endLine": 413,
+ "endColumn": 76,
+ "byteLength": 48
}
}
}
@@ -3008,7 +3027,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "equal_contents." },
+ "message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
@@ -3017,11 +3036,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 357,
- "startColumn": 28,
- "endLine": 357,
- "endColumn": 49,
- "byteLength": 21
+ "startLine": 416,
+ "startColumn": 4,
+ "endLine": 416,
+ "endColumn": 60,
+ "byteLength": 56
}
}
}
@@ -3031,7 +3050,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strstr." },
+ "message": { "text": "dest_null_terminated." },
"locations": [
{
"physicalLocation": {
@@ -3040,11 +3059,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 229,
- "startColumn": 12,
- "endLine": 229,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 417,
+ "startColumn": 34,
+ "endLine": 417,
+ "endColumn": 77,
+ "byteLength": 43
}
}
}
@@ -3054,9 +3073,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strchrnul."
- },
+ "message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
@@ -3065,11 +3082,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 176,
- "startColumn": 12,
- "endLine": 176,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 418,
+ "startColumn": 24,
+ "endLine": 418,
+ "endColumn": 39,
+ "byteLength": 15
}
}
}
@@ -3079,7 +3096,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_src." },
+ "message": { "text": "assigns clause in function strcat." },
"locations": [
{
"physicalLocation": {
@@ -3088,11 +3105,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 93,
- "startColumn": 24,
- "endLine": 93,
- "endColumn": 51,
- "byteLength": 27
+ "startLine": 411,
+ "startColumn": 12,
+ "endLine": 411,
+ "endColumn": 58,
+ "byteLength": 46
}
}
}
@@ -3102,7 +3119,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_src." },
+ "message": {
+ "text":
+ "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strcat."
+ },
"locations": [
{
"physicalLocation": {
@@ -3111,11 +3131,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 384,
- "startColumn": 31,
- "endLine": 384,
- "endColumn": 53,
- "byteLength": 22
+ "startLine": 411,
+ "startColumn": 12,
+ "endLine": 411,
+ "endColumn": 58,
+ "byteLength": 46
}
}
}
@@ -3126,7 +3146,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function strcmp."
+ "text": "from clause of term \\result in function strcat."
},
"locations": [
{
@@ -3136,9 +3156,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 139,
+ "startLine": 414,
"startColumn": 12,
- "endLine": 139,
+ "endLine": 414,
"endColumn": 19,
"byteLength": 7
}
@@ -3150,7 +3170,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strdup." },
+ "message": { "text": "behavior default in function strchr." },
"locations": [
{
"physicalLocation": {
@@ -3159,9 +3179,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 484,
+ "startLine": 173,
"startColumn": 12,
- "endLine": 484,
+ "endLine": 173,
"endColumn": 13,
"byteLength": 1
}
@@ -3173,20 +3193,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "s_initialized." },
+ "message": { "text": "behavior default! in function strchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 38,
- "startColumn": 39,
- "endLine": 38,
- "endColumn": 75,
- "byteLength": 36
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -3196,7 +3216,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "s_null." },
+ "message": { "text": "behavior found in function strchr." },
"locations": [
{
"physicalLocation": {
@@ -3205,11 +3225,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 310,
- "startColumn": 20,
- "endLine": 310,
- "endColumn": 30,
- "byteLength": 10
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -3219,20 +3239,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "WcsLen." },
+ "message": { "text": "behavior not_found in function strchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 230,
- "startColumn": 4,
- "endLine": 232,
- "endColumn": 63,
- "byteLength": 147
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -3242,7 +3262,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_subset." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -3251,11 +3271,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 306,
- "startColumn": 27,
- "endLine": 306,
- "endColumn": 72,
- "byteLength": 45
+ "startLine": 157,
+ "startColumn": 29,
+ "endLine": 157,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -3265,7 +3285,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_dest." },
+ "message": { "text": "char_found." },
"locations": [
{
"physicalLocation": {
@@ -3274,11 +3294,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 424,
- "startColumn": 32,
- "endLine": 424,
- "endColumn": 50,
- "byteLength": 18
+ "startLine": 160,
+ "startColumn": 24,
+ "endLine": 160,
+ "endColumn": 35,
+ "byteLength": 11
}
}
}
@@ -3288,7 +3308,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_subset." },
+ "message": { "text": "char_not_found." },
"locations": [
{
"physicalLocation": {
@@ -3297,11 +3317,34 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 321,
- "startColumn": 27,
- "endLine": 322,
- "endColumn": 65,
- "byteLength": 85
+ "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
}
}
}
@@ -3311,7 +3354,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": { "text": "result_same_base." },
"locations": [
{
"physicalLocation": {
@@ -3320,11 +3363,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 197,
- "startColumn": 29,
- "endLine": 197,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 162,
+ "startColumn": 30,
+ "endLine": 162,
+ "endColumn": 66,
+ "byteLength": 36
}
}
}
@@ -3334,7 +3377,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_ptr." },
+ "message": { "text": "result_in_length." },
"locations": [
{
"physicalLocation": {
@@ -3343,11 +3386,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 99,
- "startColumn": 24,
- "endLine": 99,
- "endColumn": 39,
- "byteLength": 15
+ "startLine": 163,
+ "startColumn": 30,
+ "endLine": 163,
+ "endColumn": 59,
+ "byteLength": 29
}
}
}
@@ -3357,7 +3400,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strlcat." },
+ "message": { "text": "result_valid_string." },
"locations": [
{
"physicalLocation": {
@@ -3366,11 +3409,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 455,
- "startColumn": 14,
- "endLine": 455,
- "endColumn": 21,
- "byteLength": 7
+ "startLine": 164,
+ "startColumn": 33,
+ "endLine": 164,
+ "endColumn": 59,
+ "byteLength": 26
}
}
}
@@ -3380,7 +3423,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "disjoint clause in function strtok_r." },
+ "message": { "text": "result_first_occur." },
"locations": [
{
"physicalLocation": {
@@ -3389,11 +3432,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 327,
- "startColumn": 12,
- "endLine": 327,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 165,
+ "startColumn": 32,
+ "endLine": 165,
+ "endColumn": 79,
+ "byteLength": 47
}
}
}
@@ -3403,10 +3446,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *(__fc_strtok_ptr + (0 ..)) in function strtok."
- },
+ "message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
@@ -3415,11 +3455,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 269,
- "startColumn": 12,
- "endLine": 269,
- "endColumn": 32,
- "byteLength": 20
+ "startLine": 168,
+ "startColumn": 25,
+ "endLine": 168,
+ "endColumn": 41,
+ "byteLength": 16
}
}
}
@@ -3429,7 +3469,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nstring_src." },
+ "message": { "text": "result_null_or_same_base." },
"locations": [
{
"physicalLocation": {
@@ -3438,11 +3478,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 363,
- "startColumn": 32,
- "endLine": 363,
- "endColumn": 58,
- "byteLength": 26
+ "startLine": 171,
+ "startColumn": 4,
+ "endLine": 171,
+ "endColumn": 60,
+ "byteLength": 56
}
}
}
@@ -3452,9 +3492,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term *saveptr in function strtok_r."
- },
+ "message": { "text": "assigns clause in function strchr." },
"locations": [
{
"physicalLocation": {
@@ -3463,11 +3501,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 294,
- "startColumn": 10,
- "endLine": 294,
- "endColumn": 18,
- "byteLength": 8
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -3478,7 +3516,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function stpcpy."
+ "text": "from clause of term \\result in function strchr."
},
"locations": [
{
@@ -3488,9 +3526,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 401,
+ "startLine": 158,
"startColumn": 12,
- "endLine": 401,
+ "endLine": 158,
"endColumn": 19,
"byteLength": 7
}
@@ -3502,9 +3540,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function memset."
- },
+ "message": { "text": "behavior default! in function strchrnul." },
"locations": [
{
"physicalLocation": {
@@ -3513,11 +3549,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 117,
+ "startLine": 179,
"startColumn": 12,
- "endLine": 117,
- "endColumn": 19,
- "byteLength": 7
+ "endLine": 179,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -3527,7 +3563,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_src." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -3536,11 +3572,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 105,
- "startColumn": 24,
- "endLine": 105,
- "endColumn": 51,
- "byteLength": 27
+ "startLine": 175,
+ "startColumn": 29,
+ "endLine": 175,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -3550,20 +3586,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_neg." },
+ "message": { "text": "result_same_base." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 199,
- "startColumn": 4,
- "endLine": 202,
- "endColumn": 22,
- "byteLength": 113
+ "startLine": 177,
+ "startColumn": 30,
+ "endLine": 177,
+ "endColumn": 64,
+ "byteLength": 34
}
}
}
@@ -3573,7 +3609,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_internal_str." },
+ "message": { "text": "assigns clause in function strchrnul." },
"locations": [
{
"physicalLocation": {
@@ -3582,11 +3618,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 519,
- "startColumn": 33,
- "endLine": 519,
- "endColumn": 60,
- "byteLength": 27
+ "startLine": 179,
+ "startColumn": 12,
+ "endLine": 179,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -3596,7 +3632,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strncpy." },
+ "message": {
+ "text": "from clause of term \\result in function strchrnul."
+ },
"locations": [
{
"physicalLocation": {
@@ -3605,11 +3643,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 378,
+ "startLine": 176,
"startColumn": 12,
- "endLine": 378,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 176,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -3619,7 +3657,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_reject." },
+ "message": { "text": "behavior default! in function strcmp." },
"locations": [
{
"physicalLocation": {
@@ -3628,11 +3666,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 198,
- "startColumn": 34,
- "endLine": 198,
- "endColumn": 59,
- "byteLength": 25
+ "startLine": 142,
+ "startColumn": 11,
+ "endLine": 142,
+ "endColumn": 17,
+ "byteLength": 6
}
}
}
@@ -3642,20 +3680,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcschr_def." },
+ "message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 266,
- "startColumn": 4,
- "endLine": 269,
- "endColumn": 29,
- "byteLength": 153
+ "startLine": 137,
+ "startColumn": 30,
+ "endLine": 137,
+ "endColumn": 51,
+ "byteLength": 21
}
}
}
@@ -3665,20 +3703,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_shift." },
+ "message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 222,
- "startColumn": 4,
- "endLine": 224,
- "endColumn": 55,
- "byteLength": 117
+ "startLine": 138,
+ "startColumn": 30,
+ "endLine": 138,
+ "endColumn": 51,
+ "byteLength": 21
}
}
}
@@ -3688,7 +3726,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "not_first_call." },
+ "message": { "text": "acsl_c_equiv." },
"locations": [
{
"physicalLocation": {
@@ -3697,11 +3735,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 311,
- "startColumn": 29,
- "endLine": 311,
- "endColumn": 46,
- "byteLength": 17
+ "startLine": 140,
+ "startColumn": 26,
+ "endLine": 140,
+ "endColumn": 50,
+ "byteLength": 24
}
}
}
@@ -3711,7 +3749,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null_or_in_haystack." },
+ "message": { "text": "assigns clause in function strcmp." },
"locations": [
{
"physicalLocation": {
@@ -3720,11 +3758,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 225,
- "startColumn": 4,
- "endLine": 227,
- "endColumn": 59,
- "byteLength": 141
+ "startLine": 142,
+ "startColumn": 11,
+ "endLine": 142,
+ "endColumn": 17,
+ "byteLength": 6
}
}
}
@@ -3734,7 +3772,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s1." },
+ "message": {
+ "text": "from clause of term \\result in function strcmp."
+ },
"locations": [
{
"physicalLocation": {
@@ -3743,11 +3783,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 144,
- "startColumn": 30,
- "endLine": 144,
- "endColumn": 55,
- "byteLength": 25
+ "startLine": 139,
+ "startColumn": 12,
+ "endLine": 139,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -3757,9 +3797,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strtok."
- },
+ "message": { "text": "behavior default! in function strcoll." },
"locations": [
{
"physicalLocation": {
@@ -3768,10 +3806,10 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 263,
- "startColumn": 12,
- "endLine": 263,
- "endColumn": 19,
+ "startLine": 155,
+ "startColumn": 11,
+ "endLine": 155,
+ "endColumn": 18,
"byteLength": 7
}
}
@@ -3782,7 +3820,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_src." },
+ "message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
@@ -3791,11 +3829,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 351,
- "startColumn": 31,
- "endLine": 351,
- "endColumn": 53,
- "byteLength": 22
+ "startLine": 151,
+ "startColumn": 30,
+ "endLine": 151,
+ "endColumn": 51,
+ "byteLength": 21
}
}
}
@@ -3805,7 +3843,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_bounded." },
+ "message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
@@ -3814,11 +3852,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 133,
- "startColumn": 28,
- "endLine": 133,
- "endColumn": 64,
- "byteLength": 36
+ "startLine": 152,
+ "startColumn": 30,
+ "endLine": 152,
+ "endColumn": 51,
+ "byteLength": 21
}
}
}
@@ -3828,7 +3866,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "acsl_c_equiv." },
+ "message": { "text": "assigns clause in function strcoll." },
"locations": [
{
"physicalLocation": {
@@ -3837,11 +3875,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 147,
- "startColumn": 26,
- "endLine": 147,
- "endColumn": 53,
- "byteLength": 27
+ "startLine": 155,
+ "startColumn": 11,
+ "endLine": 155,
+ "endColumn": 18,
+ "byteLength": 7
}
}
}
@@ -3852,7 +3890,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "allocates/frees clause in function strndup."
+ "text": "from clause of term \\result in function strcoll."
},
"locations": [
{
@@ -3862,11 +3900,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 506,
+ "startLine": 153,
"startColumn": 12,
- "endLine": 506,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 153,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -3876,7 +3914,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_nul_terminated." },
+ "message": { "text": "behavior default! in function strcpy." },
"locations": [
{
"physicalLocation": {
@@ -3885,11 +3923,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 344,
- "startColumn": 35,
- "endLine": 344,
- "endColumn": 51,
- "byteLength": 16
+ "startLine": 360,
+ "startColumn": 12,
+ "endLine": 360,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -3899,7 +3937,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_dest." },
+ "message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
@@ -3908,11 +3946,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 409,
- "startColumn": 32,
- "endLine": 409,
- "endColumn": 50,
- "byteLength": 18
+ "startLine": 351,
+ "startColumn": 31,
+ "endLine": 351,
+ "endColumn": 53,
+ "byteLength": 22
}
}
}
@@ -3922,7 +3960,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strcpy." },
+ "message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
@@ -3931,11 +3969,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 360,
- "startColumn": 12,
- "endLine": 360,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 352,
+ "startColumn": 26,
+ "endLine": 352,
+ "endColumn": 55,
+ "byteLength": 29
}
}
}
@@ -3945,20 +3983,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_not_zero." },
+ "message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 95,
+ "startLine": 354,
"startColumn": 4,
- "endLine": 97,
- "endColumn": 58,
- "byteLength": 120
+ "endLine": 354,
+ "endColumn": 59,
+ "byteLength": 55
}
}
}
@@ -3968,7 +4006,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null_or_same_base." },
+ "message": { "text": "equal_contents." },
"locations": [
{
"physicalLocation": {
@@ -3977,11 +4015,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 216,
- "startColumn": 4,
- "endLine": 216,
- "endColumn": 60,
- "byteLength": 56
+ "startLine": 357,
+ "startColumn": 28,
+ "endLine": 357,
+ "endColumn": 49,
+ "byteLength": 21
}
}
}
@@ -3991,9 +4029,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strncat."
- },
+ "message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
@@ -4002,11 +4038,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 441,
- "startColumn": 12,
- "endLine": 441,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 358,
+ "startColumn": 24,
+ "endLine": 358,
+ "endColumn": 39,
+ "byteLength": 15
}
}
}
@@ -4016,7 +4052,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "danglingness." },
+ "message": { "text": "assigns clause in function strcpy." },
"locations": [
{
"physicalLocation": {
@@ -4025,11 +4061,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 60,
- "startColumn": 30,
- "endLine": 60,
- "endColumn": 49,
- "byteLength": 19
+ "startLine": 355,
+ "startColumn": 12,
+ "endLine": 355,
+ "endColumn": 32,
+ "byteLength": 20
}
}
}
@@ -4041,7 +4077,7 @@
"level": "none",
"message": {
"text":
- "from clause of term *(*saveptr + (0 ..)) in function strtok_r."
+ "from clause of term *(dest + (0 .. strlen{Old}(src))) in function strcpy."
},
"locations": [
{
@@ -4051,11 +4087,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 313,
+ "startLine": 355,
"startColumn": 12,
- "endLine": 313,
- "endColumn": 27,
- "byteLength": 15
+ "endLine": 355,
+ "endColumn": 32,
+ "byteLength": 20
}
}
}
@@ -4065,7 +4101,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "can_allocate." },
+ "message": {
+ "text": "from clause of term \\result in function strcpy."
+ },
"locations": [
{
"physicalLocation": {
@@ -4074,11 +4112,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 491,
- "startColumn": 26,
- "endLine": 491,
- "endColumn": 60,
- "byteLength": 34
+ "startLine": 356,
+ "startColumn": 12,
+ "endLine": 356,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -4088,7 +4126,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": { "text": "behavior default! in function strcspn." },
"locations": [
{
"physicalLocation": {
@@ -4097,11 +4135,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 175,
- "startColumn": 29,
- "endLine": 175,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 202,
+ "startColumn": 14,
+ "endLine": 202,
+ "endColumn": 21,
+ "byteLength": 7
}
}
}
@@ -4111,7 +4149,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_haystack." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -4120,11 +4158,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 231,
- "startColumn": 36,
- "endLine": 231,
- "endColumn": 63,
- "byteLength": 27
+ "startLine": 197,
+ "startColumn": 29,
+ "endLine": 197,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -4134,9 +4172,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function memchr."
- },
+ "message": { "text": "valid_string_reject." },
"locations": [
{
"physicalLocation": {
@@ -4145,11 +4181,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 76,
- "startColumn": 12,
- "endLine": 76,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 198,
+ "startColumn": 34,
+ "endLine": 198,
+ "endColumn": 59,
+ "byteLength": 25
}
}
}
@@ -4159,7 +4195,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strtok_r." },
+ "message": { "text": "result_bounded." },
"locations": [
{
"physicalLocation": {
@@ -4168,11 +4204,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 288,
- "startColumn": 10,
- "endLine": 288,
- "endColumn": 16,
- "byteLength": 6
+ "startLine": 200,
+ "startColumn": 28,
+ "endLine": 200,
+ "endColumn": 53,
+ "byteLength": 25
}
}
}
@@ -4182,7 +4218,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "complete clause in function strtok." },
+ "message": { "text": "assigns clause in function strcspn." },
"locations": [
{
"physicalLocation": {
@@ -4191,11 +4227,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 283,
- "startColumn": 12,
- "endLine": 283,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 202,
+ "startColumn": 14,
+ "endLine": 202,
+ "endColumn": 21,
+ "byteLength": 7
}
}
}
@@ -4206,8 +4242,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text":
- "from clause of term __fc_heap_status in function strdup."
+ "text": "from clause of term \\result in function strcspn."
},
"locations": [
{
@@ -4217,34 +4252,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 473,
+ "startLine": 199,
"startColumn": 12,
- "endLine": 473,
- "endColumn": 28,
- "byteLength": 16
- }
- }
- }
- ]
- },
- {
- "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
+ "endLine": 199,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -4254,7 +4266,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function memset." },
+ "message": { "text": "behavior allocation in function strdup." },
"locations": [
{
"physicalLocation": {
@@ -4263,11 +4275,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 116,
+ "startLine": 484,
"startColumn": 12,
- "endLine": 116,
- "endColumn": 32,
- "byteLength": 20
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -4277,7 +4289,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "logic_spec." },
+ "message": { "text": "behavior default! in function strdup." },
"locations": [
{
"physicalLocation": {
@@ -4286,11 +4298,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 63,
- "startColumn": 24,
- "endLine": 63,
- "endColumn": 73,
- "byteLength": 49
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -4300,7 +4312,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strxfrm." },
+ "message": { "text": "behavior no_allocation in function strdup." },
"locations": [
{
"physicalLocation": {
@@ -4309,11 +4321,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 463,
- "startColumn": 14,
- "endLine": 463,
- "endColumn": 21,
- "byteLength": 7
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -4323,7 +4335,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_accept." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -4332,11 +4344,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 205,
- "startColumn": 34,
- "endLine": 205,
- "endColumn": 59,
- "byteLength": 25
+ "startLine": 468,
+ "startColumn": 29,
+ "endLine": 468,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -4346,10 +4358,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *(dest + (0 .. n - 1)) in function strxfrm."
- },
+ "message": { "text": "can_allocate." },
"locations": [
{
"physicalLocation": {
@@ -4358,11 +4367,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 460,
- "startColumn": 12,
- "endLine": 460,
- "endColumn": 26,
- "byteLength": 14
+ "startLine": 472,
+ "startColumn": 26,
+ "endLine": 472,
+ "endColumn": 49,
+ "byteLength": 23
}
}
}
@@ -4372,7 +4381,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior resume_str in function strtok." },
+ "message": { "text": "cannot_allocate." },
"locations": [
{
"physicalLocation": {
@@ -4381,11 +4390,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 283,
- "startColumn": 12,
- "endLine": 283,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 479,
+ "startColumn": 29,
+ "endLine": 479,
+ "endColumn": 53,
+ "byteLength": 24
}
}
}
@@ -4395,20 +4404,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_create." },
+ "message": { "text": "allocation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 226,
- "startColumn": 4,
- "endLine": 228,
- "endColumn": 52,
- "byteLength": 115
+ "startLine": 475,
+ "startColumn": 24,
+ "endLine": 475,
+ "endColumn": 49,
+ "byteLength": 25
}
}
}
@@ -4418,20 +4427,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "memchr_def." },
+ "message": { "text": "result_valid_string_and_same_contents." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 57,
+ "startLine": 477,
"startColumn": 4,
- "endLine": 59,
- "endColumn": 62,
- "byteLength": 134
+ "endLine": 477,
+ "endColumn": 51,
+ "byteLength": 47
}
}
}
@@ -4441,7 +4450,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "s_null." },
+ "message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
@@ -4450,11 +4459,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 267,
- "startColumn": 20,
- "endLine": 267,
- "endColumn": 30,
- "byteLength": 10
+ "startLine": 482,
+ "startColumn": 25,
+ "endLine": 482,
+ "endColumn": 41,
+ "byteLength": 16
}
}
}
@@ -4464,7 +4473,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function memcmp." },
+ "message": { "text": "assigns clause in function strdup." },
"locations": [
{
"physicalLocation": {
@@ -4473,11 +4482,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 65,
- "startColumn": 11,
- "endLine": 65,
- "endColumn": 17,
- "byteLength": 6
+ "startLine": 473,
+ "startColumn": 12,
+ "endLine": 473,
+ "endColumn": 28,
+ "byteLength": 16
}
}
}
@@ -4487,7 +4496,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strerror." },
+ "message": { "text": "assigns clause in function strdup." },
"locations": [
{
"physicalLocation": {
@@ -4496,9 +4505,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 347,
+ "startLine": 484,
"startColumn": 12,
- "endLine": 347,
+ "endLine": 484,
"endColumn": 13,
"byteLength": 1
}
@@ -4510,7 +4519,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior complete in function strncpy." },
+ "message": { "text": "assigns clause in function strdup." },
"locations": [
{
"physicalLocation": {
@@ -4519,9 +4528,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 378,
+ "startLine": 484,
"startColumn": 12,
- "endLine": 378,
+ "endLine": 484,
"endColumn": 13,
"byteLength": 1
}
@@ -4533,7 +4542,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_dest." },
+ "message": {
+ "text":
+ "from clause of term __fc_heap_status in function strdup."
+ },
"locations": [
{
"physicalLocation": {
@@ -4542,11 +4554,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 92,
- "startColumn": 25,
- "endLine": 92,
- "endColumn": 48,
- "byteLength": 23
+ "startLine": 473,
+ "startColumn": 12,
+ "endLine": 473,
+ "endColumn": 28,
+ "byteLength": 16
}
}
}
@@ -4556,7 +4568,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "char_not_found." },
+ "message": {
+ "text": "from clause of term \\result in function strdup."
+ },
"locations": [
{
"physicalLocation": {
@@ -4565,11 +4579,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 85,
- "startColumn": 28,
- "endLine": 85,
- "endColumn": 49,
- "byteLength": 21
+ "startLine": 474,
+ "startColumn": 12,
+ "endLine": 474,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -4580,7 +4594,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function strtok_r."
+ "text": "from clause of term \\result in function strdup."
},
"locations": [
{
@@ -4590,9 +4604,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 305,
+ "startLine": 470,
"startColumn": 12,
- "endLine": 305,
+ "endLine": 470,
"endColumn": 19,
"byteLength": 7
}
@@ -4604,7 +4618,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strpbrk." },
+ "message": {
+ "text": "from clause of term \\result in function strdup."
+ },
"locations": [
{
"physicalLocation": {
@@ -4613,11 +4629,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 218,
+ "startLine": 480,
"startColumn": 12,
- "endLine": 218,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 480,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -4650,7 +4666,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_bounded." },
+ "message": { "text": "allocates/frees clause in function strdup." },
"locations": [
{
"physicalLocation": {
@@ -4659,11 +4675,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 200,
- "startColumn": 28,
- "endLine": 200,
- "endColumn": 53,
- "byteLength": 25
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -4673,9 +4689,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term *(s + (0 ..)) in function strtok_r."
- },
+ "message": { "text": "behavior default! in function strerror." },
"locations": [
{
"physicalLocation": {
@@ -4684,11 +4698,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 304,
+ "startLine": 347,
"startColumn": 12,
- "endLine": 304,
- "endColumn": 18,
- "byteLength": 6
+ "endLine": 347,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -4698,7 +4712,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strcmp." },
+ "message": { "text": "result_internal_str." },
"locations": [
{
"physicalLocation": {
@@ -4707,11 +4721,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 142,
- "startColumn": 11,
- "endLine": 142,
- "endColumn": 17,
- "byteLength": 6
+ "startLine": 343,
+ "startColumn": 33,
+ "endLine": 343,
+ "endColumn": 59,
+ "byteLength": 26
}
}
}
@@ -4721,7 +4735,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "char_found." },
+ "message": { "text": "result_nul_terminated." },
"locations": [
{
"physicalLocation": {
@@ -4730,11 +4744,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 160,
- "startColumn": 24,
- "endLine": 160,
- "endColumn": 35,
- "byteLength": 11
+ "startLine": 344,
+ "startColumn": 35,
+ "endLine": 344,
+ "endColumn": 51,
+ "byteLength": 16
}
}
}
@@ -4744,7 +4758,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "saveptr_subset." },
+ "message": { "text": "result_valid_string." },
"locations": [
{
"physicalLocation": {
@@ -4753,11 +4767,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 323,
- "startColumn": 28,
- "endLine": 323,
- "endColumn": 67,
- "byteLength": 39
+ "startLine": 345,
+ "startColumn": 33,
+ "endLine": 345,
+ "endColumn": 59,
+ "byteLength": 26
}
}
}
@@ -4767,7 +4781,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_saveptr." },
+ "message": { "text": "assigns clause in function strerror." },
"locations": [
{
"physicalLocation": {
@@ -4776,11 +4790,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 287,
- "startColumn": 26,
- "endLine": 287,
- "endColumn": 41,
- "byteLength": 15
+ "startLine": 347,
+ "startColumn": 12,
+ "endLine": 347,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -4790,7 +4804,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strndup." },
+ "message": {
+ "text": "from clause of term \\result in function strerror."
+ },
"locations": [
{
"physicalLocation": {
@@ -4799,11 +4815,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 506,
+ "startLine": 342,
"startColumn": 12,
- "endLine": 506,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 342,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -4813,20 +4829,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_sup." },
+ "message": { "text": "behavior default! in function strlcat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 103,
- "startColumn": 4,
- "endLine": 105,
- "endColumn": 51,
- "byteLength": 108
+ "startLine": 455,
+ "startColumn": 14,
+ "endLine": 455,
+ "endColumn": 21,
+ "byteLength": 7
}
}
}
@@ -4836,20 +4852,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "StrLen." },
+ "message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 132,
- "startColumn": 4,
- "endLine": 135,
- "endColumn": 38,
- "byteLength": 185
+ "startLine": 448,
+ "startColumn": 31,
+ "endLine": 448,
+ "endColumn": 53,
+ "byteLength": 22
}
}
}
@@ -4859,7 +4875,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strncat." },
+ "message": { "text": "valid_string_dest." },
"locations": [
{
"physicalLocation": {
@@ -4868,11 +4884,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 431,
- "startColumn": 12,
- "endLine": 431,
- "endColumn": 58,
- "byteLength": 46
+ "startLine": 449,
+ "startColumn": 32,
+ "endLine": 449,
+ "endColumn": 50,
+ "byteLength": 18
}
}
}
@@ -4882,20 +4898,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "dynamic_allocation." },
+ "message": { "text": "room_nstring." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_alloc_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 39,
- "startColumn": 4,
- "endLine": 41,
- "endColumn": 61,
- "byteLength": 110
+ "startLine": 450,
+ "startColumn": 27,
+ "endLine": 450,
+ "endColumn": 48,
+ "byteLength": 21
}
}
}
@@ -4905,7 +4921,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "s_not_null." },
+ "message": { "text": "bounded_result." },
"locations": [
{
"physicalLocation": {
@@ -4914,11 +4930,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 298,
- "startColumn": 24,
- "endLine": 298,
- "endColumn": 34,
- "byteLength": 10
+ "startLine": 453,
+ "startColumn": 28,
+ "endLine": 453,
+ "endColumn": 65,
+ "byteLength": 37
}
}
}
@@ -4928,7 +4944,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "room_string." },
+ "message": { "text": "assigns clause in function strlcat." },
"locations": [
{
"physicalLocation": {
@@ -4937,11 +4953,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 397,
- "startColumn": 26,
- "endLine": 397,
- "endColumn": 55,
- "byteLength": 29
+ "startLine": 451,
+ "startColumn": 12,
+ "endLine": 451,
+ "endColumn": 33,
+ "byteLength": 21
}
}
}
@@ -4951,7 +4967,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "saveptr_subset." },
+ "message": {
+ "text":
+ "from clause of term *(dest + (strlen{Old}(dest) .. n)) in function strlcat."
+ },
"locations": [
{
"physicalLocation": {
@@ -4960,11 +4979,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 308,
- "startColumn": 28,
- "endLine": 308,
- "endColumn": 54,
- "byteLength": 26
+ "startLine": 451,
+ "startColumn": 12,
+ "endLine": 451,
+ "endColumn": 33,
+ "byteLength": 21
}
}
}
@@ -4974,7 +4993,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strsignal." },
+ "message": {
+ "text": "from clause of term \\result in function strlcat."
+ },
"locations": [
{
"physicalLocation": {
@@ -4983,11 +5004,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 523,
+ "startLine": 452,
"startColumn": 12,
- "endLine": 523,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 452,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -4997,7 +5018,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strlen." },
+ "message": { "text": "behavior default! in function strlcpy." },
"locations": [
{
"physicalLocation": {
@@ -5006,11 +5027,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 129,
- "startColumn": 14,
- "endLine": 129,
- "endColumn": 20,
- "byteLength": 6
+ "startLine": 393,
+ "startColumn": 7,
+ "endLine": 393,
+ "endColumn": 14,
+ "byteLength": 7
}
}
}
@@ -5020,7 +5041,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strsep." },
+ "message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
@@ -5029,11 +5050,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 331,
- "startColumn": 12,
- "endLine": 331,
- "endColumn": 20,
- "byteLength": 8
+ "startLine": 384,
+ "startColumn": 31,
+ "endLine": 384,
+ "endColumn": 53,
+ "byteLength": 22
}
}
}
@@ -5043,7 +5064,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_internal_str." },
+ "message": { "text": "room_nstring." },
"locations": [
{
"physicalLocation": {
@@ -5052,11 +5073,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 343,
- "startColumn": 33,
- "endLine": 343,
- "endColumn": 59,
- "byteLength": 26
+ "startLine": 385,
+ "startColumn": 27,
+ "endLine": 385,
+ "endColumn": 48,
+ "byteLength": 21
}
}
}
@@ -5066,20 +5087,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "MemSet." },
+ "message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 68,
+ "startLine": 387,
"startColumn": 4,
- "endLine": 70,
- "endColumn": 63,
- "byteLength": 135
+ "endLine": 387,
+ "endColumn": 61,
+ "byteLength": 57
}
}
}
@@ -5089,10 +5110,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *((char *)s + (0 .. n - 1)) in function memset."
- },
+ "message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
@@ -5101,11 +5119,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 116,
- "startColumn": 12,
- "endLine": 116,
- "endColumn": 32,
- "byteLength": 20
+ "startLine": 390,
+ "startColumn": 28,
+ "endLine": 390,
+ "endColumn": 73,
+ "byteLength": 45
}
}
}
@@ -5115,7 +5133,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strrchr." },
+ "message": { "text": "bounded_result." },
"locations": [
{
"physicalLocation": {
@@ -5124,11 +5142,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 195,
- "startColumn": 12,
- "endLine": 195,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 391,
+ "startColumn": 28,
+ "endLine": 391,
+ "endColumn": 50,
+ "byteLength": 22
}
}
}
@@ -5138,7 +5156,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strndup." },
+ "message": { "text": "assigns clause in function strlcpy." },
"locations": [
{
"physicalLocation": {
@@ -5147,11 +5165,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 506,
+ "startLine": 388,
"startColumn": 12,
- "endLine": 506,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 388,
+ "endColumn": 24,
+ "byteLength": 12
}
}
}
@@ -5161,7 +5179,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_subset." },
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. n - 1)) in function strlcpy."
+ },
"locations": [
{
"physicalLocation": {
@@ -5170,11 +5191,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 264,
- "startColumn": 27,
- "endLine": 264,
- "endColumn": 72,
- "byteLength": 45
+ "startLine": 388,
+ "startColumn": 12,
+ "endLine": 388,
+ "endColumn": 24,
+ "byteLength": 12
}
}
}
@@ -5185,7 +5206,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "behavior no_allocation in function strndup."
+ "text": "from clause of term \\result in function strlcpy."
},
"locations": [
{
@@ -5195,11 +5216,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 506,
+ "startLine": 389,
"startColumn": 12,
- "endLine": 506,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 389,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -5209,9 +5230,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "allocates/frees clause in function strndup."
- },
+ "message": { "text": "behavior default! in function strlen." },
"locations": [
{
"physicalLocation": {
@@ -5220,11 +5239,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 487,
+ "startLine": 129,
"startColumn": 14,
- "endLine": 487,
- "endColumn": 21,
- "byteLength": 7
+ "endLine": 129,
+ "endColumn": 20,
+ "byteLength": 6
}
}
}
@@ -5234,7 +5253,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strchr." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -5243,11 +5262,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 173,
- "startColumn": 12,
- "endLine": 173,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 125,
+ "startColumn": 29,
+ "endLine": 125,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -5257,20 +5276,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcsncmp_zero." },
+ "message": { "text": "acsl_c_equiv." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 252,
- "startColumn": 4,
- "endLine": 256,
- "endColumn": 53,
- "byteLength": 194
+ "startLine": 127,
+ "startColumn": 26,
+ "endLine": 127,
+ "endColumn": 46,
+ "byteLength": 20
}
}
}
@@ -5280,9 +5299,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strcspn."
- },
+ "message": { "text": "assigns clause in function strlen." },
"locations": [
{
"physicalLocation": {
@@ -5291,11 +5308,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 199,
- "startColumn": 12,
- "endLine": 199,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 129,
+ "startColumn": 14,
+ "endLine": 129,
+ "endColumn": 20,
+ "byteLength": 6
}
}
}
@@ -5305,7 +5322,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strchrnul." },
+ "message": {
+ "text": "from clause of term \\result in function strlen."
+ },
"locations": [
{
"physicalLocation": {
@@ -5314,11 +5333,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 179,
+ "startLine": 126,
"startColumn": 12,
- "endLine": 179,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 126,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -5328,20 +5347,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_char." },
+ "message": { "text": "behavior default! in function strncasecmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 161,
- "startColumn": 25,
- "endLine": 161,
- "endColumn": 44,
- "byteLength": 19
+ "startLine": 57,
+ "startColumn": 11,
+ "endLine": 57,
+ "endColumn": 22,
+ "byteLength": 11
}
}
}
@@ -5351,20 +5370,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "WcsChr." },
+ "message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 266,
- "startColumn": 4,
- "endLine": 269,
- "endColumn": 29,
- "byteLength": 153
+ "startLine": 53,
+ "startColumn": 28,
+ "endLine": 53,
+ "endColumn": 53,
+ "byteLength": 25
}
}
}
@@ -5374,22 +5393,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strlcat."
- },
+ "message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
- "startColumn": 12,
- "endLine": 452,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 54,
+ "startColumn": 28,
+ "endLine": 54,
+ "endColumn": 53,
+ "byteLength": 25
}
}
}
@@ -5399,20 +5416,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_same_base." },
+ "message": { "text": "assigns clause in function strncasecmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 162,
- "startColumn": 30,
- "endLine": 162,
- "endColumn": 66,
- "byteLength": 36
+ "startLine": 57,
+ "startColumn": 11,
+ "endLine": 57,
+ "endColumn": 22,
+ "byteLength": 11
}
}
}
@@ -5422,20 +5439,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": {
+ "text": "from clause of term \\result in function strncasecmp."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/string.h",
+ "uri": "libc/strings.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 157,
- "startColumn": 29,
- "endLine": 157,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 55,
+ "startColumn": 10,
+ "endLine": 55,
+ "endColumn": 17,
+ "byteLength": 7
}
}
}
@@ -5445,7 +5464,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strcspn." },
+ "message": { "text": "behavior complete in function strncat." },
"locations": [
{
"physicalLocation": {
@@ -5454,11 +5473,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 202,
- "startColumn": 14,
- "endLine": 202,
- "endColumn": 21,
- "byteLength": 7
+ "startLine": 444,
+ "startColumn": 12,
+ "endLine": 444,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -5468,7 +5487,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "bounded_result." },
+ "message": { "text": "behavior default! in function strncat." },
"locations": [
{
"physicalLocation": {
@@ -5477,11 +5496,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 453,
- "startColumn": 28,
- "endLine": 453,
- "endColumn": 65,
- "byteLength": 37
+ "startLine": 444,
+ "startColumn": 12,
+ "endLine": 444,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -5491,7 +5510,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "copied_contents." },
+ "message": { "text": "behavior partial in function strncat." },
"locations": [
{
"physicalLocation": {
@@ -5500,11 +5519,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 98,
- "startColumn": 29,
- "endLine": 98,
- "endColumn": 76,
- "byteLength": 47
+ "startLine": 444,
+ "startColumn": 12,
+ "endLine": 444,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -5514,7 +5533,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_valid_string." },
+ "message": { "text": "valid_nstring_src." },
"locations": [
{
"physicalLocation": {
@@ -5523,10 +5542,10 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 345,
- "startColumn": 33,
- "endLine": 345,
- "endColumn": 59,
+ "startLine": 423,
+ "startColumn": 32,
+ "endLine": 423,
+ "endColumn": 58,
"byteLength": 26
}
}
@@ -5537,7 +5556,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "room_string." },
+ "message": { "text": "valid_string_dest." },
"locations": [
{
"physicalLocation": {
@@ -5546,11 +5565,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 410,
- "startColumn": 26,
- "endLine": 410,
- "endColumn": 70,
- "byteLength": 44
+ "startLine": 424,
+ "startColumn": 32,
+ "endLine": 424,
+ "endColumn": 50,
+ "byteLength": 18
}
}
}
@@ -5560,20 +5579,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_zero." },
+ "message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 99,
- "startColumn": 4,
- "endLine": 101,
- "endColumn": 59,
- "byteLength": 117
+ "startLine": 430,
+ "startColumn": 26,
+ "endLine": 430,
+ "endColumn": 74,
+ "byteLength": 48
}
}
}
@@ -5583,9 +5602,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strdup."
- },
+ "message": { "text": "room_string." },
"locations": [
{
"physicalLocation": {
@@ -5594,11 +5611,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 470,
- "startColumn": 12,
- "endLine": 470,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 438,
+ "startColumn": 26,
+ "endLine": 438,
+ "endColumn": 64,
+ "byteLength": 38
}
}
}
@@ -5608,7 +5625,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strcasestr." },
+ "message": { "text": "valid_string_src_fits." },
"locations": [
{
"physicalLocation": {
@@ -5617,11 +5634,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 239,
- "startColumn": 12,
- "endLine": 239,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 429,
+ "startColumn": 35,
+ "endLine": 429,
+ "endColumn": 77,
+ "byteLength": 42
}
}
}
@@ -5631,20 +5648,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strcasecmp." },
+ "message": { "text": "valid_string_src_too_large." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 50,
- "startColumn": 11,
- "endLine": 50,
- "endColumn": 21,
- "byteLength": 10
+ "startLine": 437,
+ "startColumn": 4,
+ "endLine": 437,
+ "endColumn": 49,
+ "byteLength": 45
}
}
}
@@ -5654,7 +5671,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "bounded_result." },
+ "message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
@@ -5663,11 +5680,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 391,
- "startColumn": 28,
- "endLine": 391,
- "endColumn": 50,
- "byteLength": 22
+ "startLine": 427,
+ "startColumn": 24,
+ "endLine": 427,
+ "endColumn": 39,
+ "byteLength": 15
}
}
}
@@ -5677,7 +5694,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strncat." },
+ "message": { "text": "sum_of_lengths." },
"locations": [
{
"physicalLocation": {
@@ -5686,11 +5703,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 439,
- "startColumn": 12,
- "endLine": 439,
- "endColumn": 48,
- "byteLength": 36
+ "startLine": 434,
+ "startColumn": 28,
+ "endLine": 434,
+ "endColumn": 76,
+ "byteLength": 48
}
}
}
@@ -5700,10 +5717,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *(dest + (strlen{Old}(dest) .. n)) in function strlcat."
- },
+ "message": { "text": "sum_of_bounded_lengths." },
"locations": [
{
"physicalLocation": {
@@ -5712,11 +5726,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 451,
- "startColumn": 12,
- "endLine": 451,
- "endColumn": 33,
- "byteLength": 21
+ "startLine": 442,
+ "startColumn": 36,
+ "endLine": 442,
+ "endColumn": 74,
+ "byteLength": 38
}
}
}
@@ -5726,20 +5740,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_create." },
+ "message": { "text": "assigns clause in function strncat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 111,
- "startColumn": 4,
- "endLine": 113,
- "endColumn": 51,
- "byteLength": 111
+ "startLine": 431,
+ "startColumn": 12,
+ "endLine": 431,
+ "endColumn": 58,
+ "byteLength": 46
}
}
}
@@ -5749,22 +5763,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strcasecmp."
- },
+ "message": { "text": "assigns clause in function strncat." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 48,
- "startColumn": 10,
- "endLine": 48,
- "endColumn": 17,
- "byteLength": 7
+ "startLine": 425,
+ "startColumn": 12,
+ "endLine": 425,
+ "endColumn": 50,
+ "byteLength": 38
}
}
}
@@ -5774,7 +5786,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior resume_str in function strtok_r." },
+ "message": { "text": "assigns clause in function strncat." },
"locations": [
{
"physicalLocation": {
@@ -5783,11 +5795,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 327,
+ "startLine": 439,
"startColumn": 12,
- "endLine": 327,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 439,
+ "endColumn": 48,
+ "byteLength": 36
}
}
}
@@ -5797,7 +5809,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function memmove." },
+ "message": {
+ "text":
+ "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strncat."
+ },
"locations": [
{
"physicalLocation": {
@@ -5806,11 +5821,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 111,
+ "startLine": 431,
"startColumn": 12,
- "endLine": 111,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 431,
+ "endColumn": 58,
+ "byteLength": 46
}
}
}
@@ -5820,7 +5835,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strtok_r." },
+ "message": {
+ "text": "from clause of term \\result in function strncat."
+ },
"locations": [
{
"physicalLocation": {
@@ -5829,11 +5846,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 303,
+ "startLine": 433,
"startColumn": 12,
- "endLine": 303,
- "endColumn": 20,
- "byteLength": 8
+ "endLine": 433,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -5843,7 +5860,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior found in function strrchr." },
+ "message": {
+ "text":
+ "from clause of term *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) in function strncat."
+ },
"locations": [
{
"physicalLocation": {
@@ -5852,11 +5872,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 195,
+ "startLine": 425,
"startColumn": 12,
- "endLine": 195,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 425,
+ "endColumn": 50,
+ "byteLength": 38
}
}
}
@@ -5866,7 +5886,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_dest." },
+ "message": {
+ "text": "from clause of term \\result in function strncat."
+ },
"locations": [
{
"physicalLocation": {
@@ -5875,11 +5897,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 449,
- "startColumn": 32,
- "endLine": 449,
- "endColumn": 50,
- "byteLength": 18
+ "startLine": 426,
+ "startColumn": 12,
+ "endLine": 426,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -5889,7 +5911,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": {
+ "text":
+ "from clause of term *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) in function strncat."
+ },
"locations": [
{
"physicalLocation": {
@@ -5898,11 +5923,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 212,
- "startColumn": 29,
- "endLine": 212,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 439,
+ "startColumn": 12,
+ "endLine": 439,
+ "endColumn": 48,
+ "byteLength": 36
}
}
}
@@ -5912,7 +5937,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "cannot_allocate." },
+ "message": {
+ "text": "from clause of term \\result in function strncat."
+ },
"locations": [
{
"physicalLocation": {
@@ -5921,11 +5948,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 479,
- "startColumn": 29,
- "endLine": 479,
- "endColumn": 53,
- "byteLength": 24
+ "startLine": 441,
+ "startColumn": 12,
+ "endLine": 441,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -5935,20 +5962,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_create_shift." },
+ "message": { "text": "behavior default! in function strncmp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 115,
- "startColumn": 4,
- "endLine": 117,
- "endColumn": 62,
- "byteLength": 143
+ "startLine": 149,
+ "startColumn": 11,
+ "endLine": 149,
+ "endColumn": 18,
+ "byteLength": 7
}
}
}
@@ -5958,9 +5985,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strtok_r."
- },
+ "message": { "text": "valid_string_s1." },
"locations": [
{
"physicalLocation": {
@@ -5969,11 +5994,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 292,
- "startColumn": 10,
- "endLine": 292,
- "endColumn": 17,
- "byteLength": 7
+ "startLine": 144,
+ "startColumn": 30,
+ "endLine": 144,
+ "endColumn": 55,
+ "byteLength": 25
}
}
}
@@ -5983,7 +6008,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_nul_terminated." },
+ "message": { "text": "valid_string_s2." },
"locations": [
{
"physicalLocation": {
@@ -5992,11 +6017,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 520,
- "startColumn": 35,
- "endLine": 520,
- "endColumn": 51,
- "byteLength": 16
+ "startLine": 145,
+ "startColumn": 30,
+ "endLine": 145,
+ "endColumn": 55,
+ "byteLength": 25
}
}
}
@@ -6006,7 +6031,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "sum_of_lengths." },
+ "message": { "text": "acsl_c_equiv." },
"locations": [
{
"physicalLocation": {
@@ -6015,11 +6040,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 413,
- "startColumn": 28,
- "endLine": 413,
- "endColumn": 76,
- "byteLength": 48
+ "startLine": 147,
+ "startColumn": 26,
+ "endLine": 147,
+ "endColumn": 53,
+ "byteLength": 27
}
}
}
@@ -6029,7 +6054,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null." },
+ "message": { "text": "assigns clause in function strncmp." },
"locations": [
{
"physicalLocation": {
@@ -6038,11 +6063,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 86,
- "startColumn": 25,
- "endLine": 86,
- "endColumn": 41,
- "byteLength": 16
+ "startLine": 149,
+ "startColumn": 11,
+ "endLine": 149,
+ "endColumn": 18,
+ "byteLength": 7
}
}
}
@@ -6053,8 +6078,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text":
- "from clause of term __fc_heap_status in function strndup."
+ "text": "from clause of term \\result in function strncmp."
},
"locations": [
{
@@ -6064,11 +6088,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 492,
+ "startLine": 146,
"startColumn": 12,
- "endLine": 492,
- "endColumn": 28,
- "byteLength": 16
+ "endLine": 146,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -6078,7 +6102,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s2." },
+ "message": { "text": "behavior complete in function strncpy." },
"locations": [
{
"physicalLocation": {
@@ -6087,11 +6111,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 152,
- "startColumn": 30,
- "endLine": 152,
- "endColumn": 51,
- "byteLength": 21
+ "startLine": 378,
+ "startColumn": 12,
+ "endLine": 378,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -6101,7 +6125,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "separation." },
+ "message": { "text": "behavior default! in function strncpy." },
"locations": [
{
"physicalLocation": {
@@ -6110,11 +6134,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 366,
- "startColumn": 4,
- "endLine": 366,
- "endColumn": 43,
- "byteLength": 39
+ "startLine": 378,
+ "startColumn": 12,
+ "endLine": 378,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -6124,9 +6148,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strchr."
- },
+ "message": { "text": "behavior partial in function strncpy." },
"locations": [
{
"physicalLocation": {
@@ -6135,11 +6157,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 158,
+ "startLine": 378,
"startColumn": 12,
- "endLine": 158,
- "endColumn": 19,
- "byteLength": 7
+ "endLine": 378,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -6149,7 +6171,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_dest." },
+ "message": { "text": "valid_nstring_src." },
"locations": [
{
"physicalLocation": {
@@ -6158,11 +6180,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 104,
- "startColumn": 25,
- "endLine": 104,
- "endColumn": 48,
- "byteLength": 23
+ "startLine": 363,
+ "startColumn": 32,
+ "endLine": 363,
+ "endColumn": 58,
+ "byteLength": 26
}
}
}
@@ -6172,9 +6194,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term *saveptr in function strtok_r."
- },
+ "message": { "text": "room_nstring." },
"locations": [
{
"physicalLocation": {
@@ -6183,11 +6203,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 303,
- "startColumn": 12,
- "endLine": 303,
- "endColumn": 20,
- "byteLength": 8
+ "startLine": 364,
+ "startColumn": 27,
+ "endLine": 364,
+ "endColumn": 50,
+ "byteLength": 23
}
}
}
@@ -6197,9 +6217,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strtok."
- },
+ "message": { "text": "separation." },
"locations": [
{
"physicalLocation": {
@@ -6208,11 +6226,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 275,
- "startColumn": 12,
- "endLine": 275,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 366,
+ "startColumn": 4,
+ "endLine": 366,
+ "endColumn": 43,
+ "byteLength": 39
}
}
}
@@ -6222,7 +6240,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "copied_contents." },
+ "message": { "text": "src_fits." },
"locations": [
{
"physicalLocation": {
@@ -6231,11 +6249,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 108,
- "startColumn": 29,
- "endLine": 108,
- "endColumn": 76,
- "byteLength": 47
+ "startLine": 372,
+ "startColumn": 22,
+ "endLine": 372,
+ "endColumn": 37,
+ "byteLength": 15
}
}
}
@@ -6245,7 +6263,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strsep." },
+ "message": { "text": "src_too_long." },
"locations": [
{
"physicalLocation": {
@@ -6254,11 +6272,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 334,
- "startColumn": 12,
- "endLine": 334,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 375,
+ "startColumn": 26,
+ "endLine": 375,
+ "endColumn": 42,
+ "byteLength": 16
}
}
}
@@ -6268,10 +6286,7 @@
"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."
- },
+ "message": { "text": "result_ptr." },
"locations": [
{
"physicalLocation": {
@@ -6280,11 +6295,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 431,
- "startColumn": 12,
- "endLine": 431,
- "endColumn": 58,
- "byteLength": 46
+ "startLine": 369,
+ "startColumn": 24,
+ "endLine": 369,
+ "endColumn": 39,
+ "byteLength": 15
}
}
}
@@ -6294,7 +6309,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "sum_of_lengths." },
+ "message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
@@ -6303,11 +6318,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 434,
+ "startLine": 370,
"startColumn": 28,
- "endLine": 434,
- "endColumn": 76,
- "byteLength": 48
+ "endLine": 370,
+ "endColumn": 57,
+ "byteLength": 29
}
}
}
@@ -6317,7 +6332,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strcpy." },
+ "message": { "text": "equal_after_copy." },
"locations": [
{
"physicalLocation": {
@@ -6326,11 +6341,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 355,
- "startColumn": 12,
- "endLine": 355,
- "endColumn": 32,
- "byteLength": 20
+ "startLine": 373,
+ "startColumn": 30,
+ "endLine": 373,
+ "endColumn": 51,
+ "byteLength": 21
}
}
}
@@ -6340,10 +6355,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *((char *)dest + (0 .. n - 1)) in function memmove."
- },
+ "message": { "text": "equal_prefix." },
"locations": [
{
"physicalLocation": {
@@ -6352,11 +6364,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 106,
- "startColumn": 12,
- "endLine": 106,
- "endColumn": 35,
- "byteLength": 23
+ "startLine": 376,
+ "startColumn": 26,
+ "endLine": 376,
+ "endColumn": 60,
+ "byteLength": 34
}
}
}
@@ -6366,20 +6378,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_before_null." },
+ "message": { "text": "assigns clause in function strncpy." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 204,
- "startColumn": 4,
- "endLine": 205,
- "endColumn": 76,
- "byteLength": 105
+ "startLine": 367,
+ "startColumn": 12,
+ "endLine": 367,
+ "endColumn": 26,
+ "byteLength": 14
}
}
}
@@ -6389,7 +6401,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "ptr_subset." },
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. n - 1)) in function strncpy."
+ },
"locations": [
{
"physicalLocation": {
@@ -6398,11 +6413,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 279,
- "startColumn": 24,
- "endLine": 279,
- "endColumn": 77,
- "byteLength": 53
+ "startLine": 367,
+ "startColumn": 12,
+ "endLine": 367,
+ "endColumn": 26,
+ "byteLength": 14
}
}
}
@@ -6413,7 +6428,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function strcasestr."
+ "text": "from clause of term \\result in function strncpy."
},
"locations": [
{
@@ -6423,9 +6438,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 233,
+ "startLine": 368,
"startColumn": 12,
- "endLine": 233,
+ "endLine": 368,
"endColumn": 19,
"byteLength": 7
}
@@ -6437,7 +6452,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "allocates/frees clause in function strdup." },
+ "message": { "text": "behavior allocation in function strndup." },
"locations": [
{
"physicalLocation": {
@@ -6446,9 +6461,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 484,
+ "startLine": 506,
"startColumn": 12,
- "endLine": 484,
+ "endLine": 506,
"endColumn": 13,
"byteLength": 1
}
@@ -6460,7 +6475,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strncat." },
+ "message": { "text": "behavior default! in function strndup." },
"locations": [
{
"physicalLocation": {
@@ -6469,9 +6484,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 444,
+ "startLine": 506,
"startColumn": 12,
- "endLine": 444,
+ "endLine": 506,
"endColumn": 13,
"byteLength": 1
}
@@ -6483,7 +6498,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function memmove." },
+ "message": {
+ "text": "behavior no_allocation in function strndup."
+ },
"locations": [
{
"physicalLocation": {
@@ -6492,11 +6509,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 106,
+ "startLine": 506,
"startColumn": 12,
- "endLine": 106,
- "endColumn": 35,
- "byteLength": 23
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -6506,7 +6523,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_src." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -6515,11 +6532,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 448,
- "startColumn": 31,
- "endLine": 448,
- "endColumn": 53,
- "byteLength": 22
+ "startLine": 486,
+ "startColumn": 29,
+ "endLine": 486,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -6529,7 +6546,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strcspn." },
+ "message": { "text": "can_allocate." },
"locations": [
{
"physicalLocation": {
@@ -6538,11 +6555,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 202,
- "startColumn": 14,
- "endLine": 202,
- "endColumn": 21,
- "byteLength": 7
+ "startLine": 491,
+ "startColumn": 26,
+ "endLine": 491,
+ "endColumn": 60,
+ "byteLength": 34
}
}
}
@@ -6552,7 +6569,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function memcmp." },
+ "message": { "text": "cannot_allocate." },
"locations": [
{
"physicalLocation": {
@@ -6561,11 +6578,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 65,
- "startColumn": 11,
- "endLine": 65,
- "endColumn": 17,
- "byteLength": 6
+ "startLine": 501,
+ "startColumn": 29,
+ "endLine": 501,
+ "endColumn": 64,
+ "byteLength": 35
}
}
}
@@ -6575,7 +6592,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strncmp." },
+ "message": { "text": "allocation." },
"locations": [
{
"physicalLocation": {
@@ -6584,11 +6601,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 149,
- "startColumn": 11,
- "endLine": 149,
- "endColumn": 18,
- "byteLength": 7
+ "startLine": 495,
+ "startColumn": 24,
+ "endLine": 495,
+ "endColumn": 60,
+ "byteLength": 36
}
}
}
@@ -6599,44 +6616,21 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function strncasecmp."
+ "text": "result_valid_string_bounded_and_same_prefix."
},
"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": "memcmp_strlen_shift_left." },
- "locations": [
- {
- "physicalLocation": {
- "artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 127,
+ "startLine": 497,
"startColumn": 4,
- "endLine": 130,
- "endColumn": 38,
- "byteLength": 184
+ "endLine": 499,
+ "endColumn": 29,
+ "byteLength": 124
}
}
}
@@ -6646,9 +6640,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function memcmp."
- },
+ "message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
@@ -6657,11 +6649,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 61,
- "startColumn": 12,
- "endLine": 61,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 504,
+ "startColumn": 25,
+ "endLine": 504,
+ "endColumn": 41,
+ "byteLength": 16
}
}
}
@@ -6671,20 +6663,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "src_fits." },
+ "message": { "text": "assigns clause in function strndup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
"uri": "libc/string.h",
- "uriBaseId": "FRAMAC_SHARE"
- },
- "region": {
- "startLine": 372,
- "startColumn": 22,
- "endLine": 372,
- "endColumn": 37,
- "byteLength": 15
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 492,
+ "startColumn": 12,
+ "endLine": 492,
+ "endColumn": 28,
+ "byteLength": 16
}
}
}
@@ -6694,9 +6686,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strncmp."
- },
+ "message": { "text": "assigns clause in function strndup." },
"locations": [
{
"physicalLocation": {
@@ -6705,11 +6695,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 146,
+ "startLine": 506,
"startColumn": 12,
- "endLine": 146,
- "endColumn": 19,
- "byteLength": 7
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -6719,20 +6709,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "memcmp_zero." },
+ "message": { "text": "assigns clause in function strndup." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 39,
- "startColumn": 4,
- "endLine": 42,
- "endColumn": 70,
- "byteLength": 170
+ "startLine": 506,
+ "startColumn": 12,
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -6742,7 +6732,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_in_length." },
+ "message": {
+ "text":
+ "from clause of term __fc_heap_status in function strndup."
+ },
"locations": [
{
"physicalLocation": {
@@ -6751,11 +6744,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 163,
- "startColumn": 30,
- "endLine": 163,
- "endColumn": 59,
- "byteLength": 29
+ "startLine": 492,
+ "startColumn": 12,
+ "endLine": 492,
+ "endColumn": 28,
+ "byteLength": 16
}
}
}
@@ -6765,7 +6758,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "initialization." },
+ "message": {
+ "text": "from clause of term \\result in function strndup."
+ },
"locations": [
{
"physicalLocation": {
@@ -6774,11 +6769,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 57,
- "startColumn": 32,
- "endLine": 57,
- "endColumn": 68,
- "byteLength": 36
+ "startLine": 493,
+ "startColumn": 12,
+ "endLine": 493,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -6788,20 +6783,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "StrNCmp." },
+ "message": {
+ "text": "from clause of term \\result in function strndup."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 155,
- "startColumn": 4,
- "endLine": 159,
- "endColumn": 53,
- "byteLength": 191
+ "startLine": 488,
+ "startColumn": 12,
+ "endLine": 488,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -6836,20 +6833,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strncasecmp." },
+ "message": {
+ "text": "allocates/frees clause in function strndup."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 57,
- "startColumn": 11,
- "endLine": 57,
- "endColumn": 22,
- "byteLength": 11
+ "startLine": 487,
+ "startColumn": 14,
+ "endLine": 487,
+ "endColumn": 21,
+ "byteLength": 7
}
}
}
@@ -6859,7 +6858,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strcoll." },
+ "message": {
+ "text": "allocates/frees clause in function strndup."
+ },
"locations": [
{
"physicalLocation": {
@@ -6868,11 +6869,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 155,
- "startColumn": 11,
- "endLine": 155,
- "endColumn": 18,
- "byteLength": 7
+ "startLine": 506,
+ "startColumn": 12,
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -6882,10 +6883,7 @@
"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."
- },
+ "message": { "text": "behavior default! in function strnlen." },
"locations": [
{
"physicalLocation": {
@@ -6894,11 +6892,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 411,
- "startColumn": 12,
- "endLine": 411,
- "endColumn": 58,
- "byteLength": 46
+ "startLine": 135,
+ "startColumn": 14,
+ "endLine": 135,
+ "endColumn": 21,
+ "byteLength": 7
}
}
}
@@ -6908,7 +6906,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function memcpy." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -6917,11 +6915,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 101,
- "startColumn": 12,
- "endLine": 101,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 131,
+ "startColumn": 29,
+ "endLine": 131,
+ "endColumn": 53,
+ "byteLength": 24
}
}
}
@@ -6931,7 +6929,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "separation." },
+ "message": { "text": "result_bounded." },
"locations": [
{
"physicalLocation": {
@@ -6940,11 +6938,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 399,
- "startColumn": 4,
- "endLine": 399,
- "endColumn": 59,
- "byteLength": 55
+ "startLine": 133,
+ "startColumn": 28,
+ "endLine": 133,
+ "endColumn": 64,
+ "byteLength": 36
}
}
}
@@ -6954,7 +6952,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior new_str in function strtok." },
+ "message": { "text": "assigns clause in function strnlen." },
"locations": [
{
"physicalLocation": {
@@ -6963,11 +6961,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 283,
- "startColumn": 12,
- "endLine": 283,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 135,
+ "startColumn": 14,
+ "endLine": 135,
+ "endColumn": 21,
+ "byteLength": 7
}
}
}
@@ -6977,7 +6975,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function memchr." },
+ "message": {
+ "text": "from clause of term \\result in function strnlen."
+ },
"locations": [
{
"physicalLocation": {
@@ -6986,11 +6986,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 88,
+ "startLine": 132,
"startColumn": 12,
- "endLine": 88,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 132,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -7000,20 +7000,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_sup." },
+ "message": { "text": "behavior default! in function strpbrk." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
"startLine": 218,
- "startColumn": 4,
- "endLine": 220,
- "endColumn": 52,
- "byteLength": 112
+ "startColumn": 12,
+ "endLine": 218,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -7023,9 +7023,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term *(s + (0 ..)) in function strtok."
- },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -7034,11 +7032,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 262,
- "startColumn": 12,
- "endLine": 262,
- "endColumn": 18,
- "byteLength": 6
+ "startLine": 212,
+ "startColumn": 29,
+ "endLine": 212,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -7048,7 +7046,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s1." },
+ "message": { "text": "valid_string_accept." },
"locations": [
{
"physicalLocation": {
@@ -7057,11 +7055,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 137,
- "startColumn": 30,
- "endLine": 137,
- "endColumn": 51,
- "byteLength": 21
+ "startLine": 213,
+ "startColumn": 34,
+ "endLine": 213,
+ "endColumn": 59,
+ "byteLength": 25
}
}
}
@@ -7071,7 +7069,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_haystack." },
+ "message": { "text": "result_null_or_same_base." },
"locations": [
{
"physicalLocation": {
@@ -7080,11 +7078,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 220,
- "startColumn": 36,
- "endLine": 220,
- "endColumn": 63,
- "byteLength": 27
+ "startLine": 216,
+ "startColumn": 4,
+ "endLine": 216,
+ "endColumn": 60,
+ "byteLength": 56
}
}
}
@@ -7094,9 +7092,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term *stringp in function strsep."
- },
+ "message": { "text": "assigns clause in function strpbrk." },
"locations": [
{
"physicalLocation": {
@@ -7105,11 +7101,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 331,
+ "startLine": 218,
"startColumn": 12,
- "endLine": 331,
- "endColumn": 20,
- "byteLength": 8
+ "endLine": 218,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -7119,7 +7115,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "separation." },
+ "message": {
+ "text": "from clause of term \\result in function strpbrk."
+ },
"locations": [
{
"physicalLocation": {
@@ -7128,11 +7126,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 387,
- "startColumn": 4,
- "endLine": 387,
- "endColumn": 61,
- "byteLength": 57
+ "startLine": 214,
+ "startColumn": 12,
+ "endLine": 214,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -7142,7 +7140,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior found in function strchr." },
+ "message": { "text": "behavior default in function strrchr." },
"locations": [
{
"physicalLocation": {
@@ -7151,9 +7149,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 173,
+ "startLine": 195,
"startColumn": 12,
- "endLine": 173,
+ "endLine": 195,
"endColumn": 13,
"byteLength": 1
}
@@ -7165,20 +7163,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strcmp_zero." },
+ "message": { "text": "behavior default! in function strrchr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 143,
- "startColumn": 4,
- "endLine": 147,
- "endColumn": 63,
- "byteLength": 170
+ "startLine": 195,
+ "startColumn": 12,
+ "endLine": 195,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -7188,7 +7186,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": { "text": "behavior found in function strrchr." },
"locations": [
{
"physicalLocation": {
@@ -7197,11 +7195,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 468,
- "startColumn": 29,
- "endLine": 468,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 195,
+ "startColumn": 12,
+ "endLine": 195,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -7211,7 +7209,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior not_found in function strchr." },
+ "message": { "text": "behavior not_found in function strrchr." },
"locations": [
{
"physicalLocation": {
@@ -7220,9 +7218,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 173,
+ "startLine": 195,
"startColumn": 12,
- "endLine": 173,
+ "endLine": 195,
"endColumn": 13,
"byteLength": 1
}
@@ -7234,20 +7232,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "WcsCmp." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 240,
- "startColumn": 4,
- "endLine": 244,
- "endColumn": 63,
- "byteLength": 173
+ "startLine": 181,
+ "startColumn": 29,
+ "endLine": 181,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -7257,7 +7255,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strtok_r." },
+ "message": { "text": "char_found." },
"locations": [
{
"physicalLocation": {
@@ -7266,11 +7264,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 327,
- "startColumn": 12,
- "endLine": 327,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 184,
+ "startColumn": 24,
+ "endLine": 184,
+ "endColumn": 35,
+ "byteLength": 11
}
}
}
@@ -7280,7 +7278,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null_or_same_base." },
+ "message": { "text": "char_not_found." },
"locations": [
{
"physicalLocation": {
@@ -7289,11 +7287,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 193,
- "startColumn": 4,
- "endLine": 193,
- "endColumn": 60,
- "byteLength": 56
+ "startLine": 189,
+ "startColumn": 28,
+ "endLine": 189,
+ "endColumn": 40,
+ "byteLength": 12
}
}
}
@@ -7303,7 +7301,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "initialization." },
+ "message": { "text": "result_char." },
"locations": [
{
"physicalLocation": {
@@ -7312,11 +7310,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 416,
- "startColumn": 4,
- "endLine": 416,
- "endColumn": 60,
- "byteLength": 56
+ "startLine": 185,
+ "startColumn": 25,
+ "endLine": 185,
+ "endColumn": 38,
+ "byteLength": 13
}
}
}
@@ -7326,7 +7324,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "equal_contents." },
+ "message": { "text": "result_same_base." },
"locations": [
{
"physicalLocation": {
@@ -7335,11 +7333,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 402,
- "startColumn": 28,
- "endLine": 402,
- "endColumn": 49,
- "byteLength": 21
+ "startLine": 186,
+ "startColumn": 30,
+ "endLine": 186,
+ "endColumn": 66,
+ "byteLength": 36
}
}
}
@@ -7349,20 +7347,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_pos_or_null." },
+ "message": { "text": "result_valid_string." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 78,
- "startColumn": 4,
- "endLine": 82,
- "endColumn": 40,
- "byteLength": 169
+ "startLine": 187,
+ "startColumn": 33,
+ "endLine": 187,
+ "endColumn": 59,
+ "byteLength": 26
}
}
}
@@ -7372,7 +7370,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strdup." },
+ "message": { "text": "result_null." },
"locations": [
{
"physicalLocation": {
@@ -7381,11 +7379,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 484,
- "startColumn": 12,
- "endLine": 484,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 190,
+ "startColumn": 25,
+ "endLine": 190,
+ "endColumn": 41,
+ "byteLength": 16
}
}
}
@@ -7395,7 +7393,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strdup." },
+ "message": { "text": "result_null_or_same_base." },
"locations": [
{
"physicalLocation": {
@@ -7404,11 +7402,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 473,
- "startColumn": 12,
- "endLine": 473,
- "endColumn": 28,
- "byteLength": 16
+ "startLine": 193,
+ "startColumn": 4,
+ "endLine": 193,
+ "endColumn": 60,
+ "byteLength": 56
}
}
}
@@ -7418,7 +7416,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_valid_string_and_same_contents." },
+ "message": { "text": "assigns clause in function strrchr." },
"locations": [
{
"physicalLocation": {
@@ -7427,11 +7425,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 477,
- "startColumn": 4,
- "endLine": 477,
- "endColumn": 51,
- "byteLength": 47
+ "startLine": 195,
+ "startColumn": 12,
+ "endLine": 195,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -7441,7 +7439,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strtok." },
+ "message": {
+ "text": "from clause of term \\result in function strrchr."
+ },
"locations": [
{
"physicalLocation": {
@@ -7450,11 +7450,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 283,
+ "startLine": 182,
"startColumn": 12,
- "endLine": 283,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 182,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -7464,7 +7464,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "room_nstring." },
+ "message": { "text": "behavior default! in function strsep." },
"locations": [
{
"physicalLocation": {
@@ -7473,11 +7473,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 450,
- "startColumn": 27,
- "endLine": 450,
- "endColumn": 48,
- "byteLength": 21
+ "startLine": 334,
+ "startColumn": 12,
+ "endLine": 334,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -7487,20 +7487,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "memcmp_strlen_shift_right." },
+ "message": { "text": "valid_string_stringp." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 132,
- "startColumn": 4,
- "endLine": 135,
- "endColumn": 38,
- "byteLength": 185
+ "startLine": 329,
+ "startColumn": 35,
+ "endLine": 329,
+ "endColumn": 76,
+ "byteLength": 41
}
}
}
@@ -7510,7 +7510,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "src_too_long." },
+ "message": { "text": "valid_string_delim." },
"locations": [
{
"physicalLocation": {
@@ -7519,11 +7519,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 375,
- "startColumn": 26,
- "endLine": 375,
- "endColumn": 42,
- "byteLength": 16
+ "startLine": 330,
+ "startColumn": 33,
+ "endLine": 330,
+ "endColumn": 57,
+ "byteLength": 24
}
}
}
@@ -7533,7 +7533,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strsignal." },
+ "message": { "text": "assigns clause in function strsep." },
"locations": [
{
"physicalLocation": {
@@ -7542,11 +7542,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 523,
+ "startLine": 331,
"startColumn": 12,
- "endLine": 523,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 331,
+ "endColumn": 20,
+ "byteLength": 8
}
}
}
@@ -7556,7 +7556,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "can_allocate." },
+ "message": {
+ "text": "from clause of term *stringp in function strsep."
+ },
"locations": [
{
"physicalLocation": {
@@ -7565,11 +7567,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 472,
- "startColumn": 26,
- "endLine": 472,
- "endColumn": 49,
- "byteLength": 23
+ "startLine": 331,
+ "startColumn": 12,
+ "endLine": 331,
+ "endColumn": 20,
+ "byteLength": 8
}
}
}
@@ -7579,20 +7581,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_pos_or_null." },
+ "message": {
+ "text": "from clause of term \\result in function strsep."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 193,
- "startColumn": 4,
- "endLine": 197,
- "endColumn": 41,
- "byteLength": 174
+ "startLine": 332,
+ "startColumn": 12,
+ "endLine": 332,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -7602,20 +7606,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strncmp_zero." },
+ "message": { "text": "behavior default! in function strsignal." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 155,
- "startColumn": 4,
- "endLine": 159,
- "endColumn": 53,
- "byteLength": 191
+ "startLine": 523,
+ "startColumn": 12,
+ "endLine": 523,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -7625,20 +7629,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s1." },
+ "message": { "text": "result_internal_str." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 53,
- "startColumn": 28,
- "endLine": 53,
- "endColumn": 53,
- "byteLength": 25
+ "startLine": 519,
+ "startColumn": 33,
+ "endLine": 519,
+ "endColumn": 60,
+ "byteLength": 27
}
}
}
@@ -7648,9 +7652,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strsep."
- },
+ "message": { "text": "result_nul_terminated." },
"locations": [
{
"physicalLocation": {
@@ -7659,11 +7661,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 332,
- "startColumn": 12,
- "endLine": 332,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 520,
+ "startColumn": 35,
+ "endLine": 520,
+ "endColumn": 51,
+ "byteLength": 16
}
}
}
@@ -7673,7 +7675,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior allocation in function strdup." },
+ "message": { "text": "result_valid_string." },
"locations": [
{
"physicalLocation": {
@@ -7682,11 +7684,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 484,
- "startColumn": 12,
- "endLine": 484,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 521,
+ "startColumn": 33,
+ "endLine": 521,
+ "endColumn": 59,
+ "byteLength": 26
}
}
}
@@ -7696,7 +7698,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s." },
+ "message": { "text": "assigns clause in function strsignal." },
"locations": [
{
"physicalLocation": {
@@ -7705,11 +7707,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 181,
- "startColumn": 29,
- "endLine": 181,
- "endColumn": 49,
- "byteLength": 20
+ "startLine": 523,
+ "startColumn": 12,
+ "endLine": 523,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -7719,7 +7721,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "char_not_found." },
+ "message": {
+ "text": "from clause of term \\result in function strsignal."
+ },
"locations": [
{
"physicalLocation": {
@@ -7728,11 +7732,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 167,
- "startColumn": 28,
- "endLine": 167,
- "endColumn": 40,
- "byteLength": 12
+ "startLine": 518,
+ "startColumn": 12,
+ "endLine": 518,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -7742,7 +7746,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_needle." },
+ "message": { "text": "behavior default! in function strspn." },
"locations": [
{
"physicalLocation": {
@@ -7751,11 +7755,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 232,
- "startColumn": 34,
- "endLine": 232,
- "endColumn": 59,
- "byteLength": 25
+ "startLine": 210,
+ "startColumn": 14,
+ "endLine": 210,
+ "endColumn": 20,
+ "byteLength": 6
}
}
}
@@ -7765,7 +7769,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior found in function memchr." },
+ "message": { "text": "valid_string_s." },
"locations": [
{
"physicalLocation": {
@@ -7774,11 +7778,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 88,
- "startColumn": 12,
- "endLine": 88,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 204,
+ "startColumn": 29,
+ "endLine": 204,
+ "endColumn": 49,
+ "byteLength": 20
}
}
}
@@ -7788,7 +7792,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_same_base." },
+ "message": { "text": "valid_string_accept." },
"locations": [
{
"physicalLocation": {
@@ -7797,11 +7801,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 186,
- "startColumn": 30,
- "endLine": 186,
- "endColumn": 66,
- "byteLength": 36
+ "startLine": 205,
+ "startColumn": 34,
+ "endLine": 205,
+ "endColumn": 59,
+ "byteLength": 25
}
}
}
@@ -7834,7 +7838,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "acsl_c_equiv." },
+ "message": { "text": "assigns clause in function strspn." },
"locations": [
{
"physicalLocation": {
@@ -7843,11 +7847,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 140,
- "startColumn": 26,
- "endLine": 140,
- "endColumn": 50,
- "byteLength": 24
+ "startLine": 206,
+ "startColumn": 12,
+ "endLine": 206,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -7857,20 +7861,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_not_zero." },
+ "message": {
+ "text": "from clause of term \\result in function strspn."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 210,
- "startColumn": 4,
- "endLine": 212,
- "endColumn": 59,
- "byteLength": 124
+ "startLine": 206,
+ "startColumn": 12,
+ "endLine": 206,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -7881,7 +7887,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function strdup."
+ "text": "from clause of term \\result in function strspn."
},
"locations": [
{
@@ -7891,9 +7897,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 474,
+ "startLine": 207,
"startColumn": 12,
- "endLine": 474,
+ "endLine": 207,
"endColumn": 19,
"byteLength": 7
}
@@ -7905,7 +7911,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strrchr." },
+ "message": { "text": "behavior default! in function strstr." },
"locations": [
{
"physicalLocation": {
@@ -7914,9 +7920,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 195,
+ "startLine": 229,
"startColumn": 12,
- "endLine": 195,
+ "endLine": 229,
"endColumn": 13,
"byteLength": 1
}
@@ -7928,7 +7934,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "allocation." },
+ "message": { "text": "valid_string_haystack." },
"locations": [
{
"physicalLocation": {
@@ -7937,11 +7943,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 495,
- "startColumn": 24,
- "endLine": 495,
- "endColumn": 60,
- "byteLength": 36
+ "startLine": 220,
+ "startColumn": 36,
+ "endLine": 220,
+ "endColumn": 63,
+ "byteLength": 27
}
}
}
@@ -7951,7 +7957,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s2." },
+ "message": { "text": "valid_string_needle." },
"locations": [
{
"physicalLocation": {
@@ -7960,10 +7966,10 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 145,
- "startColumn": 30,
- "endLine": 145,
- "endColumn": 55,
+ "startLine": 221,
+ "startColumn": 34,
+ "endLine": 221,
+ "endColumn": 59,
"byteLength": 25
}
}
@@ -7974,7 +7980,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strncat." },
+ "message": { "text": "result_null_or_in_haystack." },
"locations": [
{
"physicalLocation": {
@@ -7983,11 +7989,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 425,
- "startColumn": 12,
- "endLine": 425,
- "endColumn": 50,
- "byteLength": 38
+ "startLine": 225,
+ "startColumn": 4,
+ "endLine": 227,
+ "endColumn": 59,
+ "byteLength": 141
}
}
}
@@ -7997,20 +8003,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "never_allocable." },
+ "message": { "text": "assigns clause in function strstr." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_alloc_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 39,
- "startColumn": 4,
- "endLine": 41,
- "endColumn": 61,
- "byteLength": 110
+ "startLine": 229,
+ "startColumn": 12,
+ "endLine": 229,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -8020,7 +8026,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null." },
+ "message": {
+ "text": "from clause of term \\result in function strstr."
+ },
"locations": [
{
"physicalLocation": {
@@ -8029,11 +8037,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 504,
- "startColumn": 25,
- "endLine": 504,
- "endColumn": 41,
- "byteLength": 16
+ "startLine": 222,
+ "startColumn": 12,
+ "endLine": 222,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -8043,7 +8051,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strndup." },
+ "message": { "text": "behavior default! in function strtok." },
"locations": [
{
"physicalLocation": {
@@ -8052,9 +8060,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 506,
+ "startLine": 283,
"startColumn": 12,
- "endLine": 506,
+ "endLine": 283,
"endColumn": 13,
"byteLength": 1
}
@@ -8066,7 +8074,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "initialization." },
+ "message": { "text": "behavior new_str in function strtok." },
"locations": [
{
"physicalLocation": {
@@ -8075,11 +8083,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 307,
- "startColumn": 28,
- "endLine": 307,
- "endColumn": 49,
- "byteLength": 21
+ "startLine": 283,
+ "startColumn": 12,
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -8089,7 +8097,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_valid_string." },
+ "message": { "text": "behavior resume_str in function strtok." },
"locations": [
{
"physicalLocation": {
@@ -8098,34 +8106,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 521,
- "startColumn": 33,
- "endLine": 521,
- "endColumn": 59,
- "byteLength": 26
- }
- }
- }
- ]
- },
- {
- "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
+ "startLine": 283,
+ "startColumn": 12,
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -8135,7 +8120,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "sum_of_bounded_lengths." },
+ "message": { "text": "valid_string_delim." },
"locations": [
{
"physicalLocation": {
@@ -8144,11 +8129,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 442,
- "startColumn": 36,
- "endLine": 442,
- "endColumn": 74,
- "byteLength": 38
+ "startLine": 245,
+ "startColumn": 31,
+ "endLine": 245,
+ "endColumn": 55,
+ "byteLength": 24
}
}
}
@@ -8158,7 +8143,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "points_to_end." },
+ "message": { "text": "valid_string_s_or_delim_not_found." },
"locations": [
{
"physicalLocation": {
@@ -8167,11 +8152,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 403,
- "startColumn": 27,
- "endLine": 403,
- "endColumn": 57,
- "byteLength": 30
+ "startLine": 258,
+ "startColumn": 6,
+ "endLine": 260,
+ "endColumn": 70,
+ "byteLength": 120
}
}
}
@@ -8181,7 +8166,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_s." },
+ "message": { "text": "not_first_call." },
"locations": [
{
"physicalLocation": {
@@ -8190,11 +8175,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 115,
- "startColumn": 22,
- "endLine": 115,
- "endColumn": 42,
- "byteLength": 20
+ "startLine": 268,
+ "startColumn": 29,
+ "endLine": 268,
+ "endColumn": 53,
+ "byteLength": 24
}
}
}
@@ -8204,9 +8189,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strxfrm."
- },
+ "message": { "text": "s_not_null." },
"locations": [
{
"physicalLocation": {
@@ -8215,11 +8198,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 461,
- "startColumn": 12,
- "endLine": 461,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 256,
+ "startColumn": 24,
+ "endLine": 256,
+ "endColumn": 34,
+ "byteLength": 10
}
}
}
@@ -8229,9 +8212,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function memcpy."
- },
+ "message": { "text": "s_null." },
"locations": [
{
"physicalLocation": {
@@ -8240,11 +8221,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 97,
- "startColumn": 12,
- "endLine": 97,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 267,
+ "startColumn": 20,
+ "endLine": 267,
+ "endColumn": 30,
+ "byteLength": 10
}
}
}
@@ -8254,20 +8235,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wmemchr_def." },
+ "message": { "text": "result_subset." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 183,
- "startColumn": 4,
- "endLine": 185,
- "endColumn": 63,
- "byteLength": 143
+ "startLine": 264,
+ "startColumn": 27,
+ "endLine": 264,
+ "endColumn": 72,
+ "byteLength": 45
}
}
}
@@ -8277,7 +8258,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strtok." },
+ "message": { "text": "ptr_subset." },
"locations": [
{
"physicalLocation": {
@@ -8286,11 +8267,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 261,
- "startColumn": 12,
- "endLine": 261,
- "endColumn": 27,
- "byteLength": 15
+ "startLine": 265,
+ "startColumn": 24,
+ "endLine": 265,
+ "endColumn": 57,
+ "byteLength": 33
}
}
}
@@ -8300,9 +8281,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strnlen."
- },
+ "message": { "text": "result_subset." },
"locations": [
{
"physicalLocation": {
@@ -8311,11 +8290,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 132,
- "startColumn": 12,
- "endLine": 132,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 277,
+ "startColumn": 27,
+ "endLine": 278,
+ "endColumn": 72,
+ "byteLength": 92
}
}
}
@@ -8325,10 +8304,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *(dest + (0 .. strlen{Old}(src))) in function stpcpy."
- },
+ "message": { "text": "ptr_subset." },
"locations": [
{
"physicalLocation": {
@@ -8337,11 +8313,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 400,
- "startColumn": 12,
- "endLine": 400,
- "endColumn": 32,
- "byteLength": 20
+ "startLine": 279,
+ "startColumn": 24,
+ "endLine": 279,
+ "endColumn": 77,
+ "byteLength": 53
}
}
}
@@ -8351,7 +8327,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_subset." },
+ "message": { "text": "assigns clause in function strtok." },
"locations": [
{
"physicalLocation": {
@@ -8360,11 +8336,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 277,
- "startColumn": 27,
- "endLine": 278,
- "endColumn": 72,
- "byteLength": 92
+ "startLine": 246,
+ "startColumn": 10,
+ "endLine": 246,
+ "endColumn": 16,
+ "byteLength": 6
}
}
}
@@ -8374,7 +8350,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strxfrm." },
+ "message": { "text": "assigns clause in function strtok." },
"locations": [
{
"physicalLocation": {
@@ -8383,11 +8359,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 460,
+ "startLine": 261,
"startColumn": 12,
- "endLine": 460,
- "endColumn": 26,
- "byteLength": 14
+ "endLine": 261,
+ "endColumn": 27,
+ "byteLength": 15
}
}
}
@@ -8397,20 +8373,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strncasecmp." },
+ "message": { "text": "assigns clause in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 57,
- "startColumn": 11,
- "endLine": 57,
- "endColumn": 22,
- "byteLength": 11
+ "startLine": 269,
+ "startColumn": 12,
+ "endLine": 269,
+ "endColumn": 32,
+ "byteLength": 20
}
}
}
@@ -8420,7 +8396,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "room_nstring." },
+ "message": {
+ "text": "from clause of term *(s + (0 ..)) in function strtok."
+ },
"locations": [
{
"physicalLocation": {
@@ -8429,11 +8407,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 385,
- "startColumn": 27,
- "endLine": 385,
- "endColumn": 48,
- "byteLength": 21
+ "startLine": 246,
+ "startColumn": 10,
+ "endLine": 246,
+ "endColumn": 16,
+ "byteLength": 6
}
}
}
@@ -8443,7 +8421,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "room_string." },
+ "message": {
+ "text":
+ "from clause of term *(__fc_strtok_ptr + (0 ..)) in function strtok."
+ },
"locations": [
{
"physicalLocation": {
@@ -8452,11 +8433,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 352,
- "startColumn": 26,
- "endLine": 352,
- "endColumn": 55,
- "byteLength": 29
+ "startLine": 248,
+ "startColumn": 10,
+ "endLine": 248,
+ "endColumn": 30,
+ "byteLength": 20
}
}
}
@@ -8466,7 +8447,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_ptr." },
+ "message": {
+ "text": "from clause of term \\result in function strtok."
+ },
"locations": [
{
"physicalLocation": {
@@ -8475,11 +8458,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 427,
- "startColumn": 24,
- "endLine": 427,
- "endColumn": 39,
- "byteLength": 15
+ "startLine": 250,
+ "startColumn": 10,
+ "endLine": 250,
+ "endColumn": 17,
+ "byteLength": 7
}
}
}
@@ -8489,7 +8472,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_dest." },
+ "message": {
+ "text": "from clause of term __fc_strtok_ptr in function strtok."
+ },
"locations": [
{
"physicalLocation": {
@@ -8498,11 +8483,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 458,
- "startColumn": 25,
- "endLine": 458,
- "endColumn": 48,
- "byteLength": 23
+ "startLine": 252,
+ "startColumn": 10,
+ "endLine": 252,
+ "endColumn": 25,
+ "byteLength": 15
}
}
}
@@ -8513,7 +8498,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function strspn."
+ "text": "from clause of term __fc_strtok_ptr in function strtok."
},
"locations": [
{
@@ -8523,11 +8508,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 206,
+ "startLine": 261,
"startColumn": 12,
- "endLine": 206,
- "endColumn": 19,
- "byteLength": 7
+ "endLine": 261,
+ "endColumn": 27,
+ "byteLength": 15
}
}
}
@@ -8537,7 +8522,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strerror." },
+ "message": {
+ "text": "from clause of term *(s + (0 ..)) in function strtok."
+ },
"locations": [
{
"physicalLocation": {
@@ -8546,11 +8533,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 347,
+ "startLine": 262,
"startColumn": 12,
- "endLine": 347,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 262,
+ "endColumn": 18,
+ "byteLength": 6
}
}
}
@@ -8560,7 +8547,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_src_too_large." },
+ "message": {
+ "text": "from clause of term \\result in function strtok."
+ },
"locations": [
{
"physicalLocation": {
@@ -8569,11 +8558,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 437,
- "startColumn": 4,
- "endLine": 437,
- "endColumn": 49,
- "byteLength": 45
+ "startLine": 263,
+ "startColumn": 12,
+ "endLine": 263,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -8583,20 +8572,23 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "MemCmp." },
+ "message": {
+ "text":
+ "from clause of term *(__fc_strtok_ptr + (0 ..)) in function strtok."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 39,
- "startColumn": 4,
- "endLine": 42,
- "endColumn": 70,
- "byteLength": 170
+ "startLine": 269,
+ "startColumn": 12,
+ "endLine": 269,
+ "endColumn": 32,
+ "byteLength": 20
}
}
}
@@ -8606,20 +8598,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "wcslen_zero." },
+ "message": {
+ "text": "from clause of term __fc_strtok_ptr in function strtok."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 214,
- "startColumn": 4,
- "endLine": 216,
- "endColumn": 60,
- "byteLength": 121
+ "startLine": 272,
+ "startColumn": 12,
+ "endLine": 272,
+ "endColumn": 27,
+ "byteLength": 15
}
}
}
@@ -8630,7 +8624,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function strncpy."
+ "text": "from clause of term \\result in function strtok."
},
"locations": [
{
@@ -8640,9 +8634,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 368,
+ "startLine": 275,
"startColumn": 12,
- "endLine": 368,
+ "endLine": 275,
"endColumn": 19,
"byteLength": 7
}
@@ -8654,7 +8648,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function memcpy." },
+ "message": { "text": "complete clause in function strtok." },
"locations": [
{
"physicalLocation": {
@@ -8663,11 +8657,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 96,
+ "startLine": 283,
"startColumn": 12,
- "endLine": 96,
- "endColumn": 35,
- "byteLength": 23
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -8677,22 +8671,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "specialization of valid_string_s at stmt 2."
- },
+ "message": { "text": "disjoint clause in function strtok." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "tests/sarif/libc.c",
- "uriBaseId": "PWD"
+ "uri": "libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 13,
- "startColumn": 10,
- "endLine": 13,
- "endColumn": 19,
- "byteLength": 9
+ "startLine": 283,
+ "startColumn": 12,
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -8702,7 +8694,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_stringp." },
+ "message": { "text": "behavior default! in function strtok_r." },
"locations": [
{
"physicalLocation": {
@@ -8711,11 +8703,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 329,
- "startColumn": 35,
- "endLine": 329,
- "endColumn": 76,
- "byteLength": 41
+ "startLine": 327,
+ "startColumn": 12,
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -8725,20 +8717,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strlen_neg." },
+ "message": { "text": "behavior new_str in function strtok_r." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 84,
- "startColumn": 4,
- "endLine": 87,
- "endColumn": 22,
- "byteLength": 109
+ "startLine": 327,
+ "startColumn": 12,
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -8748,7 +8740,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strstr." },
+ "message": { "text": "behavior resume_str in function strtok_r." },
"locations": [
{
"physicalLocation": {
@@ -8757,9 +8749,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 229,
+ "startLine": 327,
"startColumn": 12,
- "endLine": 229,
+ "endLine": 327,
"endColumn": 13,
"byteLength": 1
}
@@ -8771,7 +8763,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_needle." },
+ "message": { "text": "valid_string_delim." },
"locations": [
{
"physicalLocation": {
@@ -8780,11 +8772,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 221,
- "startColumn": 34,
- "endLine": 221,
- "endColumn": 59,
- "byteLength": 25
+ "startLine": 286,
+ "startColumn": 31,
+ "endLine": 286,
+ "endColumn": 55,
+ "byteLength": 24
}
}
}
@@ -8794,7 +8786,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "initialization." },
+ "message": { "text": "valid_saveptr." },
"locations": [
{
"physicalLocation": {
@@ -8803,11 +8795,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 390,
- "startColumn": 28,
- "endLine": 390,
- "endColumn": 73,
- "byteLength": 45
+ "startLine": 287,
+ "startColumn": 26,
+ "endLine": 287,
+ "endColumn": 41,
+ "byteLength": 15
}
}
}
@@ -8817,20 +8809,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "memset_def." },
+ "message": { "text": "valid_string_s_or_delim_not_found." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 68,
- "startColumn": 4,
- "endLine": 70,
- "endColumn": 63,
- "byteLength": 135
+ "startLine": 300,
+ "startColumn": 6,
+ "endLine": 302,
+ "endColumn": 70,
+ "byteLength": 120
}
}
}
@@ -8840,7 +8832,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_ptr." },
+ "message": { "text": "not_first_call." },
"locations": [
{
"physicalLocation": {
@@ -8849,11 +8841,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 369,
- "startColumn": 24,
- "endLine": 369,
- "endColumn": 39,
- "byteLength": 15
+ "startLine": 311,
+ "startColumn": 29,
+ "endLine": 311,
+ "endColumn": 46,
+ "byteLength": 17
}
}
}
@@ -8863,9 +8855,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strncat."
- },
+ "message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
@@ -8874,11 +8864,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 426,
- "startColumn": 12,
- "endLine": 426,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 312,
+ "startColumn": 37,
+ "endLine": 312,
+ "endColumn": 58,
+ "byteLength": 21
}
}
}
@@ -8888,9 +8878,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strlcpy."
- },
+ "message": { "text": "s_not_null." },
"locations": [
{
"physicalLocation": {
@@ -8899,11 +8887,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 389,
- "startColumn": 12,
- "endLine": 389,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 298,
+ "startColumn": 24,
+ "endLine": 298,
+ "endColumn": 34,
+ "byteLength": 10
}
}
}
@@ -8913,7 +8901,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strchrnul." },
+ "message": { "text": "s_null." },
"locations": [
{
"physicalLocation": {
@@ -8922,11 +8910,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 179,
- "startColumn": 12,
- "endLine": 179,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 310,
+ "startColumn": 20,
+ "endLine": 310,
+ "endColumn": 30,
+ "byteLength": 10
}
}
}
@@ -8936,7 +8924,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "acsl_c_equiv." },
+ "message": { "text": "result_subset." },
"locations": [
{
"physicalLocation": {
@@ -8945,11 +8933,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 118,
- "startColumn": 26,
- "endLine": 118,
- "endColumn": 46,
- "byteLength": 20
+ "startLine": 306,
+ "startColumn": 27,
+ "endLine": 306,
+ "endColumn": 72,
+ "byteLength": 45
}
}
}
@@ -8959,9 +8947,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strlen."
- },
+ "message": { "text": "initialization." },
"locations": [
{
"physicalLocation": {
@@ -8970,11 +8956,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 126,
- "startColumn": 12,
- "endLine": 126,
- "endColumn": 19,
- "byteLength": 7
+ "startLine": 307,
+ "startColumn": 28,
+ "endLine": 307,
+ "endColumn": 49,
+ "byteLength": 21
}
}
}
@@ -8984,10 +8970,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text":
- "from clause of term *(dest + (0 .. n - 1)) in function strlcpy."
- },
+ "message": { "text": "saveptr_subset." },
"locations": [
{
"physicalLocation": {
@@ -8996,11 +8979,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 388,
- "startColumn": 12,
- "endLine": 388,
- "endColumn": 24,
- "byteLength": 12
+ "startLine": 308,
+ "startColumn": 28,
+ "endLine": 308,
+ "endColumn": 54,
+ "byteLength": 26
}
}
}
@@ -9010,7 +8993,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function strncmp." },
+ "message": { "text": "result_subset." },
"locations": [
{
"physicalLocation": {
@@ -9019,11 +9002,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 149,
- "startColumn": 11,
- "endLine": 149,
- "endColumn": 18,
- "byteLength": 7
+ "startLine": 321,
+ "startColumn": 27,
+ "endLine": 322,
+ "endColumn": 65,
+ "byteLength": 85
}
}
}
@@ -9033,7 +9016,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strndup." },
+ "message": { "text": "saveptr_subset." },
"locations": [
{
"physicalLocation": {
@@ -9042,11 +9025,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 492,
- "startColumn": 12,
- "endLine": 492,
- "endColumn": 28,
- "byteLength": 16
+ "startLine": 323,
+ "startColumn": 28,
+ "endLine": 323,
+ "endColumn": 67,
+ "byteLength": 39
}
}
}
@@ -9056,7 +9039,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_delim." },
+ "message": { "text": "assigns clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
@@ -9065,11 +9048,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 330,
- "startColumn": 33,
- "endLine": 330,
- "endColumn": 57,
- "byteLength": 24
+ "startLine": 288,
+ "startColumn": 10,
+ "endLine": 288,
+ "endColumn": 16,
+ "byteLength": 6
}
}
}
@@ -9079,7 +9062,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strpbrk." },
+ "message": { "text": "assigns clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
@@ -9088,11 +9071,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 218,
- "startColumn": 12,
- "endLine": 218,
- "endColumn": 13,
- "byteLength": 1
+ "startLine": 303,
+ "startColumn": 12,
+ "endLine": 303,
+ "endColumn": 20,
+ "byteLength": 8
}
}
}
@@ -9102,7 +9085,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_null." },
+ "message": { "text": "assigns clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
@@ -9111,11 +9094,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 482,
- "startColumn": 25,
- "endLine": 482,
- "endColumn": 41,
- "byteLength": 16
+ "startLine": 313,
+ "startColumn": 12,
+ "endLine": 313,
+ "endColumn": 27,
+ "byteLength": 15
}
}
}
@@ -9125,20 +9108,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_memory_area." },
+ "message": {
+ "text": "from clause of term *(s + (0 ..)) in function strtok_r."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 36,
- "startColumn": 32,
- "endLine": 36,
- "endColumn": 63,
- "byteLength": 31
+ "startLine": 288,
+ "startColumn": 10,
+ "endLine": 288,
+ "endColumn": 16,
+ "byteLength": 6
}
}
}
@@ -9148,7 +9133,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s_or_delim_not_found." },
+ "message": {
+ "text":
+ "from clause of term *(*saveptr + (0 ..)) in function strtok_r."
+ },
"locations": [
{
"physicalLocation": {
@@ -9157,11 +9145,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 300,
- "startColumn": 6,
- "endLine": 302,
- "endColumn": 70,
- "byteLength": 120
+ "startLine": 290,
+ "startColumn": 10,
+ "endLine": 290,
+ "endColumn": 25,
+ "byteLength": 15
}
}
}
@@ -9172,7 +9160,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function strspn."
+ "text": "from clause of term \\result in function strtok_r."
},
"locations": [
{
@@ -9182,10 +9170,10 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 207,
- "startColumn": 12,
- "endLine": 207,
- "endColumn": 19,
+ "startLine": 292,
+ "startColumn": 10,
+ "endLine": 292,
+ "endColumn": 17,
"byteLength": 7
}
}
@@ -9196,7 +9184,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_ptr." },
+ "message": {
+ "text": "from clause of term *saveptr in function strtok_r."
+ },
"locations": [
{
"physicalLocation": {
@@ -9205,11 +9195,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 119,
- "startColumn": 24,
- "endLine": 119,
- "endColumn": 36,
- "byteLength": 12
+ "startLine": 294,
+ "startColumn": 10,
+ "endLine": 294,
+ "endColumn": 18,
+ "byteLength": 8
}
}
}
@@ -9220,7 +9210,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term __fc_strtok_ptr in function strtok."
+ "text": "from clause of term *saveptr in function strtok_r."
},
"locations": [
{
@@ -9230,11 +9220,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 252,
- "startColumn": 10,
- "endLine": 252,
- "endColumn": 25,
- "byteLength": 15
+ "startLine": 303,
+ "startColumn": 12,
+ "endLine": 303,
+ "endColumn": 20,
+ "byteLength": 8
}
}
}
@@ -9244,7 +9234,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strcat." },
+ "message": {
+ "text": "from clause of term *(s + (0 ..)) in function strtok_r."
+ },
"locations": [
{
"physicalLocation": {
@@ -9253,11 +9245,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 411,
+ "startLine": 304,
"startColumn": 12,
- "endLine": 411,
- "endColumn": 58,
- "byteLength": 46
+ "endLine": 304,
+ "endColumn": 18,
+ "byteLength": 6
}
}
}
@@ -9267,7 +9259,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function stpcpy." },
+ "message": {
+ "text": "from clause of term \\result in function strtok_r."
+ },
"locations": [
{
"physicalLocation": {
@@ -9276,11 +9270,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 405,
+ "startLine": 305,
"startColumn": 12,
- "endLine": 405,
- "endColumn": 13,
- "byteLength": 1
+ "endLine": 305,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -9290,20 +9284,23 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "zero_initialized." },
+ "message": {
+ "text":
+ "from clause of term *(*saveptr + (0 ..)) in function strtok_r."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 39,
- "startColumn": 28,
- "endLine": 39,
- "endColumn": 63,
- "byteLength": 35
+ "startLine": 313,
+ "startColumn": 12,
+ "endLine": 313,
+ "endColumn": 27,
+ "byteLength": 15
}
}
}
@@ -9313,7 +9310,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "result_char." },
+ "message": {
+ "text": "from clause of term *saveptr in function strtok_r."
+ },
"locations": [
{
"physicalLocation": {
@@ -9322,11 +9321,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 185,
- "startColumn": 25,
- "endLine": 185,
- "endColumn": 38,
- "byteLength": 13
+ "startLine": 316,
+ "startColumn": 12,
+ "endLine": 316,
+ "endColumn": 20,
+ "byteLength": 8
}
}
}
@@ -9336,7 +9335,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_s2." },
+ "message": {
+ "text": "from clause of term \\result in function strtok_r."
+ },
"locations": [
{
"physicalLocation": {
@@ -9345,11 +9346,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 56,
- "startColumn": 23,
- "endLine": 56,
- "endColumn": 49,
- "byteLength": 26
+ "startLine": 319,
+ "startColumn": 12,
+ "endLine": 319,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}
@@ -9359,7 +9360,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function stpcpy." },
+ "message": { "text": "complete clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
@@ -9368,11 +9369,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 400,
+ "startLine": 327,
"startColumn": 12,
- "endLine": 400,
- "endColumn": 32,
- "byteLength": 20
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -9382,9 +9383,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strstr."
- },
+ "message": { "text": "disjoint clause in function strtok_r." },
"locations": [
{
"physicalLocation": {
@@ -9393,11 +9392,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 222,
+ "startLine": 327,
"startColumn": 12,
- "endLine": 222,
- "endColumn": 19,
- "byteLength": 7
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -9407,9 +9406,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function strrchr."
- },
+ "message": { "text": "behavior default! in function strxfrm." },
"locations": [
{
"physicalLocation": {
@@ -9418,10 +9415,10 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 182,
- "startColumn": 12,
- "endLine": 182,
- "endColumn": 19,
+ "startLine": 463,
+ "startColumn": 14,
+ "endLine": 463,
+ "endColumn": 21,
"byteLength": 7
}
}
@@ -9432,7 +9429,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function strnlen." },
+ "message": { "text": "valid_dest." },
"locations": [
{
"physicalLocation": {
@@ -9441,11 +9438,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 135,
- "startColumn": 14,
- "endLine": 135,
- "endColumn": 21,
- "byteLength": 7
+ "startLine": 458,
+ "startColumn": 25,
+ "endLine": 458,
+ "endColumn": 48,
+ "byteLength": 23
}
}
}
@@ -9455,20 +9452,20 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_s2." },
+ "message": { "text": "valid_string_src." },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/strings.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 54,
- "startColumn": 28,
- "endLine": 54,
+ "startLine": 459,
+ "startColumn": 31,
+ "endLine": 459,
"endColumn": 53,
- "byteLength": 25
+ "byteLength": 22
}
}
}
@@ -9478,9 +9475,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term *(s + (0 ..)) in function strtok."
- },
+ "message": { "text": "assigns clause in function strxfrm." },
"locations": [
{
"physicalLocation": {
@@ -9489,11 +9484,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 246,
- "startColumn": 10,
- "endLine": 246,
- "endColumn": 16,
- "byteLength": 6
+ "startLine": 460,
+ "startColumn": 12,
+ "endLine": 460,
+ "endColumn": 26,
+ "byteLength": 14
}
}
}
@@ -9503,7 +9498,10 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_string_src." },
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. n - 1)) in function strxfrm."
+ },
"locations": [
{
"physicalLocation": {
@@ -9512,11 +9510,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 408,
- "startColumn": 31,
- "endLine": 408,
- "endColumn": 53,
- "byteLength": 22
+ "startLine": 460,
+ "startColumn": 12,
+ "endLine": 460,
+ "endColumn": 26,
+ "byteLength": 14
}
}
}
@@ -9526,20 +9524,22 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "strchr_def." },
+ "message": {
+ "text": "from clause of term \\result in function strxfrm."
+ },
"locations": [
{
"physicalLocation": {
"artifactLocation": {
- "uri": "libc/__fc_string_axiomatic.h",
+ "uri": "libc/string.h",
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 168,
- "startColumn": 4,
- "endLine": 170,
- "endColumn": 75,
- "byteLength": 132
+ "startLine": 461,
+ "startColumn": 12,
+ "endLine": 461,
+ "endColumn": 19,
+ "byteLength": 7
}
}
}