diff --git a/src/plugins/markdown-report/mdr_params.ml b/src/plugins/markdown-report/mdr_params.ml
index ce052fa96fddda7cf1c709be133ad75ca4847083..6f1cbcdc05bc66e19863216f63f59e08a4315ec4 100644
--- a/src/plugins/markdown-report/mdr_params.ml
+++ b/src/plugins/markdown-report/mdr_params.ml
@@ -112,3 +112,10 @@ module Stubs = String_list(
let arg_name = "f1,...,fn"
let help = "list of C files containing stub functions"
end)
+
+module PrintLibc = True(
+ struct
+ let option_name = "-mdr-print-libc"
+ let help =
+ "when set (default), reports include information about libc elements."
+ end)
diff --git a/src/plugins/markdown-report/mdr_params.mli b/src/plugins/markdown-report/mdr_params.mli
index 34d405af386b627dbf467ce1ac4b6a94b921c1fa..b626fb5227135f8780c9a7e499bb3915d836818c 100644
--- a/src/plugins/markdown-report/mdr_params.mli
+++ b/src/plugins/markdown-report/mdr_params.mli
@@ -45,3 +45,6 @@ module Date: Parameter_sig.String
(** Value of [-mdr-stubs]. *)
module Stubs: Parameter_sig.String_list
+
+(** Value of [-mdr-print-libc]. *)
+module PrintLibc: Parameter_sig.Bool
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 407b4f064e11bcd4a183d05a5aaa36a895413558..6a8607eaf036792bb7bad366df352d6bfeaf3303 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -53,6 +53,9 @@ module Analysis_cmdline =
let gen_invocation () =
let cl = Analysis_cmdline.get () in
+ (* The first argument is _always_ the binary name, but to avoid printing it
+ as an absolute path to binlevel.opt, we replace it with 'frama-c' *)
+ let cl = "frama-c" :: List.tl cl in
let commandLine = String.concat " " cl in
let arguments = List.tl cl in
Invocation.create ~commandLine ~arguments ()
@@ -107,27 +110,51 @@ let make_message alarm annot remark =
in
Message.create ~text ~markdown ()
+let kf_is_in_libc kf =
+ let g = Kernel_function.get_global kf in
+ Cil.hasAttribute "fc_stdlib" (Cil_datatype.Global.attr g)
+
+let ip_is_in_libc ip =
+ match Property.get_kf ip with
+ | None ->
+ (* possibly an identified lemma; check its attributes *)
+ begin
+ match ip with
+ | IPAxiomatic {iax_attrs=attrs}
+ | IPLemma {il_attrs=attrs}
+ | IPAxiom {il_attrs=attrs} ->
+ Cil.hasAttribute "fc_stdlib" attrs
+ | _ ->
+ false
+ end
+ | Some kf ->
+ kf_is_in_libc kf
+
let opt_physical_location_of_loc loc =
if loc = Cil_datatype.Location.unknown then []
else [ Location.of_loc loc ]
-
+(* Cil_types *)
let gen_results remarks =
let treat_alarm _e kf s ~rank:_ alarm annot (i, rules, content) =
- let prop = Property.ip_of_code_annot_single kf s annot in
- let ruleId = Alarms.get_name alarm in
- let rules =
- Datatype.String.Map.add ruleId (Alarms.get_description alarm) rules
- in
- let label = "Alarm-" ^ string_of_int i in
- let kind = kind_of_status (Property_status.Feedback.get prop) in
- let level = level_of_status (Property_status.Feedback.get prop) in
- let remark = get_remark remarks label in
- let message = make_message alarm annot remark in
- let locations = opt_physical_location_of_loc (Cil_datatype.Stmt.loc s) in
- let res =
- Sarif_result.create ~kind ~level ~ruleId ~message ~locations ()
- in
- (i+1, rules, res :: content)
+ if not (Mdr_params.PrintLibc.get ()) && kf_is_in_libc kf then
+ (* skip alarm in libc *)
+ (i, rules, content)
+ else
+ let prop = Property.ip_of_code_annot_single kf s annot in
+ let ruleId = Alarms.get_name alarm in
+ let rules =
+ Datatype.String.Map.add ruleId (Alarms.get_description alarm) rules
+ in
+ let label = "Alarm-" ^ string_of_int i in
+ let kind = kind_of_status (Property_status.Feedback.get prop) in
+ let level = level_of_status (Property_status.Feedback.get prop) in
+ let remark = get_remark remarks label in
+ let message = make_message alarm annot remark in
+ let locations = opt_physical_location_of_loc (Cil_datatype.Stmt.loc s) in
+ let res =
+ Sarif_result.create ~kind ~level ~ruleId ~message ~locations ()
+ in
+ (i+1, rules, res :: content)
in
let _, rules, content =
Alarms.fold treat_alarm (0, Datatype.String.Map.empty,[])
@@ -153,7 +180,11 @@ let gen_status ip =
let gen_statuses () =
let f ip content =
- if is_alarm ip then content else (gen_status ip) :: content
+ let exclude =
+ is_alarm ip ||
+ (not (Mdr_params.PrintLibc.get ()) && ip_is_in_libc ip)
+ in
+ if exclude then content else (gen_status ip) :: content
in
List.rev (Property_status.fold f [])
diff --git a/src/plugins/markdown-report/tests/sarif/libc.c b/src/plugins/markdown-report/tests/sarif/libc.c
new file mode 100644
index 0000000000000000000000000000000000000000..b2458ae945850e9542e76ad75cc73312d981910a
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/libc.c
@@ -0,0 +1,13 @@
+/* run.config
+ LOG: @PTEST_DIR@/oracle/with-libc.sarif.clean
+ EXECNOW: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -mdr-gen sarif -mdr-out @PTEST_DIR@/oracle/with-libc.sarif && sed -e "s:$FRAMAC_SHARE:REPLACED_FOR_PTESTS_FRAMAC_SHARE:g" -e "s:$FRAMAC_LIB:REPLACED_FOR_PTESTS_FRAMAC_LIB:g" -e "s:$FRAMAC_PLUGIN:REPLACED_FOR_PTESTS_FRAMAC_PLUGIN:g" -e "s:$PWD:REPLACED_FOR_PTESTS_PWD:g" @PTEST_DIR@/oracle/with-libc.sarif > @PTEST_DIR@/oracle/with-libc.sarif.clean && rm -f @PTEST_DIR@/oracle/with-libc.sarif
+ EXECNOW: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -mdr-gen sarif -mdr-out @PTEST_DIR@/oracle/without-libc.sarif -mdr-no-print-libc && sed -e "s:$FRAMAC_SHARE:REPLACED_FOR_PTESTS_FRAMAC_SHARE:g" -e "s:$FRAMAC_LIB:REPLACED_FOR_PTESTS_FRAMAC_LIB:g" -e "s:$FRAMAC_PLUGIN:REPLACED_FOR_PTESTS_FRAMAC_PLUGIN:g" -e "s:$PWD:REPLACED_FOR_PTESTS_PWD:g" @PTEST_DIR@/oracle/without-libc.sarif > @PTEST_DIR@/oracle/without-libc.sarif.clean && rm -f @PTEST_DIR@/oracle/without-libc.sarif
+*/
+
+#include <string.h>
+
+int main() {
+ char *s = "hello world";
+ int n = strlen(s);
+ return n;
+}
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle b/src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..189063ded537cd8d9a0b69bc5f876b303efb3543
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/sarif/libc.c (with preprocessing)
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif.clean b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif.clean
new file mode 100644
index 0000000000000000000000000000000000000000..8c6bcc8f3da44520a80a326fd695339cabd89351
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif.clean
@@ -0,0 +1,9563 @@
+{
+ "$schema":
+ "https://github.com/oasis-tcs/sarif-spec/blob/master/Documents/CommitteeSpecificationDrafts/v2.1.0-CSD.1/sarif-schema-2.1.0.json",
+ "version": "2.1.0",
+ "runs": [
+ {
+ "tool": {
+ "driver": {
+ "name": "frama-c",
+ "fullName": "frama-c-21.1+dev (Scandium)",
+ "version": "21.1+dev (Scandium)",
+ "semanticVersion": "21.1+dev",
+ "downloadUri": "https://frama-c.com/download.html"
+ }
+ },
+ "invocations": [
+ {
+ "commandLine":
+ "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -mdr-gen sarif -mdr-out tests/sarif/oracle/with-libc.sarif",
+ "arguments": [
+ "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
+ "-load-module", "eva,from,scope,markdown_report", "-eva",
+ "-mdr-gen", "sarif", "-mdr-out",
+ "tests/sarif/oracle/with-libc.sarif"
+ ],
+ "exitCode": 0,
+ "executionSuccessful": true
+ }
+ ],
+ "originalUriBaseIds": {
+ "FRAMAC_SHARE": { "uri": "REPLACED_FOR_PTESTS_FRAMAC_SHARE" },
+ "FRAMAC_LIB": { "uri": "REPLACED_FOR_PTESTS_FRAMAC_LIB" },
+ "FRAMAC_PLUGIN": { "uri": "REPLACED_FOR_PTESTS_FRAMAC_PLUGIN" },
+ "PWD": {
+ "uri": "REPLACED_FOR_PTESTS_PWD"
+ }
+ },
+ "artifacts": [
+ {
+ "location": { "uri": "tests/sarif/libc.c" },
+ "roles": [ "analysisTarget" ],
+ "mimeType": "text/x-csrc"
+ }
+ ],
+ "results": [
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term __fc_strtok_ptr in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 261,
+ "startColumn": 12,
+ "endLine": 261,
+ "endColumn": 27,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strcpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 356,
+ "startColumn": 12,
+ "endLine": 356,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strnlen." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 135,
+ "startColumn": 14,
+ "endLine": 135,
+ "endColumn": 21,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strcasecmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 50,
+ "startColumn": 11,
+ "endLine": 50,
+ "endColumn": 21,
+ "byteLength": 10
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strpbrk."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 214,
+ "startColumn": 12,
+ "endLine": 214,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strncat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 433,
+ "startColumn": 12,
+ "endLine": 433,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *(s + (0 ..)) in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 288,
+ "startColumn": 10,
+ "endLine": 288,
+ "endColumn": 16,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior partial in function strncpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 378,
+ "startColumn": 12,
+ "endLine": 378,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strcat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 414,
+ "startColumn": 12,
+ "endLine": 414,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default in function strrchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 195,
+ "startColumn": 12,
+ "endLine": 195,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "dest_null_terminated." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 417,
+ "startColumn": 34,
+ "endLine": 417,
+ "endColumn": 77,
+ "byteLength": 43
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function bzero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 40,
+ "startColumn": 12,
+ "endLine": 40,
+ "endColumn": 17,
+ "byteLength": 5
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior new_str in function strtok_r." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 327,
+ "startColumn": 12,
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term __fc_strtok_ptr in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 272,
+ "startColumn": 12,
+ "endLine": 272,
+ "endColumn": 27,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) in function strncat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 439,
+ "startColumn": 12,
+ "endLine": 439,
+ "endColumn": 48,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 486,
+ "startColumn": 29,
+ "endLine": 486,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "room_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 438,
+ "startColumn": 26,
+ "endLine": 438,
+ "endColumn": 64,
+ "byteLength": 38
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s_or_delim_not_found." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 258,
+ "startColumn": 6,
+ "endLine": 260,
+ "endColumn": 70,
+ "byteLength": 120
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_create_shift." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 230,
+ "startColumn": 4,
+ "endLine": 232,
+ "endColumn": 63,
+ "byteLength": 147
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "StrChr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 168,
+ "startColumn": 4,
+ "endLine": 170,
+ "endColumn": 82,
+ "byteLength": 146
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function memmove."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 107,
+ "startColumn": 12,
+ "endLine": 107,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcscmp_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 240,
+ "startColumn": 4,
+ "endLine": 244,
+ "endColumn": 70,
+ "byteLength": 180
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_valid_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 164,
+ "startColumn": 33,
+ "endLine": 164,
+ "endColumn": 59,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "equal_prefix." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 376,
+ "startColumn": 26,
+ "endLine": 376,
+ "endColumn": 60,
+ "byteLength": 34
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_ptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 358,
+ "startColumn": 24,
+ "endLine": 358,
+ "endColumn": 39,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_same_base." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 177,
+ "startColumn": 30,
+ "endLine": 177,
+ "endColumn": 64,
+ "byteLength": 34
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_nstring_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 423,
+ "startColumn": 32,
+ "endLine": 423,
+ "endColumn": 58,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strtok." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 246,
+ "startColumn": 10,
+ "endLine": 246,
+ "endColumn": 16,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "equal_after_copy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 373,
+ "startColumn": 30,
+ "endLine": 373,
+ "endColumn": 51,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_same_base." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 79,
+ "startColumn": 30,
+ "endLine": 79,
+ "endColumn": 66,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strsignal."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 518,
+ "startColumn": 12,
+ "endLine": 518,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 459,
+ "startColumn": 31,
+ "endLine": 459,
+ "endColumn": 53,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strdup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 480,
+ "startColumn": 12,
+ "endLine": 480,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strcoll." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 155,
+ "startColumn": 11,
+ "endLine": 155,
+ "endColumn": 18,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null_or_same_base." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 171,
+ "startColumn": 4,
+ "endLine": 171,
+ "endColumn": 60,
+ "byteLength": 56
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 131,
+ "startColumn": 29,
+ "endLine": 131,
+ "endColumn": 53,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strndup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 493,
+ "startColumn": 12,
+ "endLine": 493,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "not_first_call." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 268,
+ "startColumn": 29,
+ "endLine": 268,
+ "endColumn": 53,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function memchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 88,
+ "startColumn": 12,
+ "endLine": 88,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *saveptr in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 316,
+ "startColumn": 12,
+ "endLine": 316,
+ "endColumn": 20,
+ "byteLength": 8
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "separation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 95,
+ "startColumn": 4,
+ "endLine": 95,
+ "endColumn": 62,
+ "byteLength": 58
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "room_nstring." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 364,
+ "startColumn": 27,
+ "endLine": 364,
+ "endColumn": 50,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "acsl_c_equiv." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 127,
+ "startColumn": 26,
+ "endLine": 127,
+ "endColumn": 46,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. n - 1)) in function strncpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 367,
+ "startColumn": 12,
+ "endLine": 367,
+ "endColumn": 26,
+ "byteLength": 14
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "initialization." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 370,
+ "startColumn": 28,
+ "endLine": 370,
+ "endColumn": 57,
+ "byteLength": 29
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "memcmp_strlen_left." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 119,
+ "startColumn": 4,
+ "endLine": 121,
+ "endColumn": 77,
+ "byteLength": 155
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strlcat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 451,
+ "startColumn": 12,
+ "endLine": 451,
+ "endColumn": 33,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "danglingness." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 74,
+ "startColumn": 8,
+ "endLine": 75,
+ "endColumn": 61,
+ "byteLength": 80
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_delim." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 245,
+ "startColumn": 31,
+ "endLine": 245,
+ "endColumn": 55,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "allocation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 475,
+ "startColumn": 24,
+ "endLine": 475,
+ "endColumn": 49,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "memcmp_strlen_right." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 123,
+ "startColumn": 4,
+ "endLine": 125,
+ "endColumn": 77,
+ "byteLength": 156
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 190,
+ "startColumn": 25,
+ "endLine": 190,
+ "endColumn": 41,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *((char *)dest + (0 .. n - 1)) in function memcpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 96,
+ "startColumn": 12,
+ "endLine": 96,
+ "endColumn": 35,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "initialization." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 71,
+ "startColumn": 8,
+ "endLine": 72,
+ "endColumn": 71,
+ "byteLength": 116
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s1." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 151,
+ "startColumn": 30,
+ "endLine": 151,
+ "endColumn": 51,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 168,
+ "startColumn": 25,
+ "endLine": 168,
+ "endColumn": 41,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "danglingness." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 59,
+ "startColumn": 30,
+ "endLine": 59,
+ "endColumn": 49,
+ "byteLength": 19
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strerror."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 342,
+ "startColumn": 12,
+ "endLine": 342,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_shift." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 107,
+ "startColumn": 4,
+ "endLine": 109,
+ "endColumn": 59,
+ "byteLength": 125
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior not_found in function strrchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 195,
+ "startColumn": 12,
+ "endLine": 195,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "cannot_allocate." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 501,
+ "startColumn": 29,
+ "endLine": 501,
+ "endColumn": 64,
+ "byteLength": 35
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strcasestr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 239,
+ "startColumn": 12,
+ "endLine": 239,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "ptr_subset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 265,
+ "startColumn": 24,
+ "endLine": 265,
+ "endColumn": 57,
+ "byteLength": 33
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strncpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 367,
+ "startColumn": 12,
+ "endLine": 367,
+ "endColumn": 26,
+ "byteLength": 14
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_s1." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 55,
+ "startColumn": 23,
+ "endLine": 55,
+ "endColumn": 49,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior complete in function strncat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 444,
+ "startColumn": 12,
+ "endLine": 444,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 125,
+ "startColumn": 29,
+ "endLine": 125,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strcoll."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 153,
+ "startColumn": 12,
+ "endLine": 153,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "result_valid_string_bounded_and_same_prefix."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 497,
+ "startColumn": 4,
+ "endLine": 499,
+ "endColumn": 29,
+ "byteLength": 124
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 204,
+ "startColumn": 29,
+ "endLine": 204,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior allocation in function strndup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 506,
+ "startColumn": 12,
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(__fc_strtok_ptr + (0 ..)) in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 248,
+ "startColumn": 10,
+ "endLine": 248,
+ "endColumn": 30,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "char_not_found." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 189,
+ "startColumn": 28,
+ "endLine": 189,
+ "endColumn": 40,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "disjoint clause in function strtok." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 283,
+ "startColumn": 12,
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strndup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 488,
+ "startColumn": 12,
+ "endLine": 488,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "s_not_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 256,
+ "startColumn": 24,
+ "endLine": 256,
+ "endColumn": 34,
+ "byteLength": 10
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 68,
+ "startColumn": 9,
+ "endLine": 69,
+ "endColumn": 74,
+ "byteLength": 100
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_accept." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 213,
+ "startColumn": 34,
+ "endLine": 213,
+ "endColumn": 59,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior not_found in function memchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 88,
+ "startColumn": 12,
+ "endLine": 88,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strspn." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 206,
+ "startColumn": 12,
+ "endLine": 206,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "initialization." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 58,
+ "startColumn": 32,
+ "endLine": 58,
+ "endColumn": 68,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_before_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 89,
+ "startColumn": 4,
+ "endLine": 90,
+ "endColumn": 79,
+ "byteLength": 108
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strlen." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 129,
+ "startColumn": 14,
+ "endLine": 129,
+ "endColumn": 20,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strlcpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 393,
+ "startColumn": 7,
+ "endLine": 393,
+ "endColumn": 14,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "separation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 354,
+ "startColumn": 4,
+ "endLine": 354,
+ "endColumn": 59,
+ "byteLength": 55
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default in function strchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "complete clause in function strtok_r." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 327,
+ "startColumn": 12,
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) in function strncat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 425,
+ "startColumn": 12,
+ "endLine": 425,
+ "endColumn": 50,
+ "byteLength": 38
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior no_allocation in function strdup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strcat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 420,
+ "startColumn": 12,
+ "endLine": 420,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "StrCmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 143,
+ "startColumn": 4,
+ "endLine": 147,
+ "endColumn": 70,
+ "byteLength": 177
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_at_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 92,
+ "startColumn": 4,
+ "endLine": 93,
+ "endColumn": 61,
+ "byteLength": 86
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(*saveptr + (0 ..)) in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 290,
+ "startColumn": 10,
+ "endLine": 290,
+ "endColumn": 25,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strspn." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 210,
+ "startColumn": 14,
+ "endLine": 210,
+ "endColumn": 20,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s2." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 138,
+ "startColumn": 30,
+ "endLine": 138,
+ "endColumn": 51,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_char." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 80,
+ "startColumn": 25,
+ "endLine": 80,
+ "endColumn": 45,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strlcpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 388,
+ "startColumn": 12,
+ "endLine": 388,
+ "endColumn": 24,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *((char *)s + (0 .. n - 1)) in function bzero."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 37,
+ "startColumn": 10,
+ "endLine": 37,
+ "endColumn": 31,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_in_str." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 81,
+ "startColumn": 27,
+ "endLine": 83,
+ "endColumn": 54,
+ "byteLength": 120
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "char_found." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 78,
+ "startColumn": 24,
+ "endLine": 78,
+ "endColumn": 44,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "MemChr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 57,
+ "startColumn": 4,
+ "endLine": 59,
+ "endColumn": 62,
+ "byteLength": 148
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 319,
+ "startColumn": 12,
+ "endLine": 319,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "char_found." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 184,
+ "startColumn": 24,
+ "endLine": 184,
+ "endColumn": 35,
+ "byteLength": 11
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 250,
+ "startColumn": 10,
+ "endLine": 250,
+ "endColumn": 17,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 396,
+ "startColumn": 31,
+ "endLine": 396,
+ "endColumn": 53,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strtok." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 269,
+ "startColumn": 12,
+ "endLine": 269,
+ "endColumn": 32,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_at_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 207,
+ "startColumn": 4,
+ "endLine": 208,
+ "endColumn": 65,
+ "byteLength": 90
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_valid_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 187,
+ "startColumn": 33,
+ "endLine": 187,
+ "endColumn": 59,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_src_fits." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 429,
+ "startColumn": 35,
+ "endLine": 429,
+ "endColumn": 77,
+ "byteLength": 42
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null_or_in_haystack." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 236,
+ "startColumn": 4,
+ "endLine": 237,
+ "endColumn": 65,
+ "byteLength": 82
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function memset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 121,
+ "startColumn": 12,
+ "endLine": 121,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_first_occur." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 165,
+ "startColumn": 32,
+ "endLine": 165,
+ "endColumn": 79,
+ "byteLength": 47
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strtok_r." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 313,
+ "startColumn": 12,
+ "endLine": 313,
+ "endColumn": 27,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "room_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 430,
+ "startColumn": 26,
+ "endLine": 430,
+ "endColumn": 74,
+ "byteLength": 48
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "initialization." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 312,
+ "startColumn": 37,
+ "endLine": 312,
+ "endColumn": 58,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "WMemChr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 183,
+ "startColumn": 4,
+ "endLine": 185,
+ "endColumn": 63,
+ "byteLength": 150
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strcmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 142,
+ "startColumn": 11,
+ "endLine": 142,
+ "endColumn": 17,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s1." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 46,
+ "startColumn": 28,
+ "endLine": 46,
+ "endColumn": 49,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function bzero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 37,
+ "startColumn": 10,
+ "endLine": 37,
+ "endColumn": 31,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. strlen{Old}(src))) in function strcpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 355,
+ "startColumn": 12,
+ "endLine": 355,
+ "endColumn": 32,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_delim." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 286,
+ "startColumn": 31,
+ "endLine": 286,
+ "endColumn": 55,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior partial in function strncat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 444,
+ "startColumn": 12,
+ "endLine": 444,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_ptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 418,
+ "startColumn": 24,
+ "endLine": 418,
+ "endColumn": 39,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_ptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 109,
+ "startColumn": 24,
+ "endLine": 109,
+ "endColumn": 39,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strdup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "equal_contents." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 357,
+ "startColumn": 28,
+ "endLine": 357,
+ "endColumn": 49,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strstr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 229,
+ "startColumn": 12,
+ "endLine": 229,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strchrnul."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 176,
+ "startColumn": 12,
+ "endLine": 176,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 93,
+ "startColumn": 24,
+ "endLine": 93,
+ "endColumn": 51,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 384,
+ "startColumn": 31,
+ "endLine": 384,
+ "endColumn": 53,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strcmp."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 139,
+ "startColumn": 12,
+ "endLine": 139,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strdup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "s_initialized." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 38,
+ "startColumn": 39,
+ "endLine": 38,
+ "endColumn": 75,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "s_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 310,
+ "startColumn": 20,
+ "endLine": 310,
+ "endColumn": 30,
+ "byteLength": 10
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "WcsLen." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 230,
+ "startColumn": 4,
+ "endLine": 232,
+ "endColumn": 63,
+ "byteLength": 147
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_subset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 306,
+ "startColumn": 27,
+ "endLine": 306,
+ "endColumn": 72,
+ "byteLength": 45
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_dest." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 424,
+ "startColumn": 32,
+ "endLine": 424,
+ "endColumn": 50,
+ "byteLength": 18
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_subset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 321,
+ "startColumn": 27,
+ "endLine": 322,
+ "endColumn": 65,
+ "byteLength": 85
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 197,
+ "startColumn": 29,
+ "endLine": 197,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_ptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 99,
+ "startColumn": 24,
+ "endLine": 99,
+ "endColumn": 39,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strlcat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 455,
+ "startColumn": 14,
+ "endLine": 455,
+ "endColumn": 21,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "disjoint clause in function strtok_r." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 327,
+ "startColumn": 12,
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(__fc_strtok_ptr + (0 ..)) in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 269,
+ "startColumn": 12,
+ "endLine": 269,
+ "endColumn": 32,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_nstring_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 363,
+ "startColumn": 32,
+ "endLine": 363,
+ "endColumn": 58,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *saveptr in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 294,
+ "startColumn": 10,
+ "endLine": 294,
+ "endColumn": 18,
+ "byteLength": 8
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function stpcpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 401,
+ "startColumn": 12,
+ "endLine": 401,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function memset."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 117,
+ "startColumn": 12,
+ "endLine": 117,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 105,
+ "startColumn": 24,
+ "endLine": 105,
+ "endColumn": 51,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_neg." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 199,
+ "startColumn": 4,
+ "endLine": 202,
+ "endColumn": 22,
+ "byteLength": 120
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_internal_str." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 519,
+ "startColumn": 33,
+ "endLine": 519,
+ "endColumn": 60,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strncpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 378,
+ "startColumn": 12,
+ "endLine": 378,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_reject." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 198,
+ "startColumn": 34,
+ "endLine": 198,
+ "endColumn": 59,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcschr_def." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 266,
+ "startColumn": 4,
+ "endLine": 269,
+ "endColumn": 29,
+ "byteLength": 167
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_shift." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 222,
+ "startColumn": 4,
+ "endLine": 224,
+ "endColumn": 55,
+ "byteLength": 117
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "not_first_call." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 311,
+ "startColumn": 29,
+ "endLine": 311,
+ "endColumn": 46,
+ "byteLength": 17
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null_or_in_haystack." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 225,
+ "startColumn": 4,
+ "endLine": 227,
+ "endColumn": 59,
+ "byteLength": 141
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s1." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 144,
+ "startColumn": 30,
+ "endLine": 144,
+ "endColumn": 55,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 263,
+ "startColumn": 12,
+ "endLine": 263,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 351,
+ "startColumn": 31,
+ "endLine": 351,
+ "endColumn": 53,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_bounded." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 133,
+ "startColumn": 28,
+ "endLine": 133,
+ "endColumn": 64,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "acsl_c_equiv." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 147,
+ "startColumn": 26,
+ "endLine": 147,
+ "endColumn": 53,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "allocates/frees clause in function strndup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 506,
+ "startColumn": 12,
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_nul_terminated." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 344,
+ "startColumn": 35,
+ "endLine": 344,
+ "endColumn": 51,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_dest." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 409,
+ "startColumn": 32,
+ "endLine": 409,
+ "endColumn": 50,
+ "byteLength": 18
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strcpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 360,
+ "startColumn": 12,
+ "endLine": 360,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_not_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 95,
+ "startColumn": 4,
+ "endLine": 97,
+ "endColumn": 58,
+ "byteLength": 127
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null_or_same_base." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 216,
+ "startColumn": 4,
+ "endLine": 216,
+ "endColumn": 60,
+ "byteLength": 56
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strncat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 441,
+ "startColumn": 12,
+ "endLine": 441,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "danglingness." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 60,
+ "startColumn": 30,
+ "endLine": 60,
+ "endColumn": 49,
+ "byteLength": 19
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(*saveptr + (0 ..)) in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 313,
+ "startColumn": 12,
+ "endLine": 313,
+ "endColumn": 27,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "can_allocate." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 491,
+ "startColumn": 26,
+ "endLine": 491,
+ "endColumn": 60,
+ "byteLength": 34
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 175,
+ "startColumn": 29,
+ "endLine": 175,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_haystack." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 231,
+ "startColumn": 36,
+ "endLine": 231,
+ "endColumn": 63,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function memchr."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 76,
+ "startColumn": 12,
+ "endLine": 76,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strtok_r." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 288,
+ "startColumn": 10,
+ "endLine": 288,
+ "endColumn": 16,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "complete clause in function strtok." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 283,
+ "startColumn": 12,
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term __fc_heap_status in function strdup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 473,
+ "startColumn": 12,
+ "endLine": 473,
+ "endColumn": 28,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s2." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 47,
+ "startColumn": 28,
+ "endLine": 47,
+ "endColumn": 49,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function memset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 116,
+ "startColumn": 12,
+ "endLine": 116,
+ "endColumn": 32,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "logic_spec." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 63,
+ "startColumn": 24,
+ "endLine": 63,
+ "endColumn": 73,
+ "byteLength": 49
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strxfrm." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 463,
+ "startColumn": 14,
+ "endLine": 463,
+ "endColumn": 21,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_accept." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 205,
+ "startColumn": 34,
+ "endLine": 205,
+ "endColumn": 59,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. n - 1)) in function strxfrm."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 460,
+ "startColumn": 12,
+ "endLine": 460,
+ "endColumn": 26,
+ "byteLength": 14
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior resume_str in function strtok." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 283,
+ "startColumn": 12,
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_create." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 226,
+ "startColumn": 4,
+ "endLine": 228,
+ "endColumn": 52,
+ "byteLength": 115
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "memchr_def." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 57,
+ "startColumn": 4,
+ "endLine": 59,
+ "endColumn": 62,
+ "byteLength": 148
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "s_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 267,
+ "startColumn": 20,
+ "endLine": 267,
+ "endColumn": 30,
+ "byteLength": 10
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function memcmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 65,
+ "startColumn": 11,
+ "endLine": 65,
+ "endColumn": 17,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strerror." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 347,
+ "startColumn": 12,
+ "endLine": 347,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior complete in function strncpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 378,
+ "startColumn": 12,
+ "endLine": 378,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_dest." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 92,
+ "startColumn": 25,
+ "endLine": 92,
+ "endColumn": 48,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "char_not_found." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 85,
+ "startColumn": 28,
+ "endLine": 85,
+ "endColumn": 49,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 305,
+ "startColumn": 12,
+ "endLine": 305,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strpbrk." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 218,
+ "startColumn": 12,
+ "endLine": 218,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "allocates/frees clause in function strdup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 469,
+ "startColumn": 14,
+ "endLine": 469,
+ "endColumn": 21,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_bounded." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 200,
+ "startColumn": 28,
+ "endLine": 200,
+ "endColumn": 53,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *(s + (0 ..)) in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 304,
+ "startColumn": 12,
+ "endLine": 304,
+ "endColumn": 18,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strcmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 142,
+ "startColumn": 11,
+ "endLine": 142,
+ "endColumn": 17,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "char_found." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 160,
+ "startColumn": 24,
+ "endLine": 160,
+ "endColumn": 35,
+ "byteLength": 11
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "saveptr_subset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 323,
+ "startColumn": 28,
+ "endLine": 323,
+ "endColumn": 67,
+ "byteLength": 39
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_saveptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 287,
+ "startColumn": 26,
+ "endLine": 287,
+ "endColumn": 41,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strndup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 506,
+ "startColumn": 12,
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_sup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 103,
+ "startColumn": 4,
+ "endLine": 105,
+ "endColumn": 51,
+ "byteLength": 115
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "StrLen." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 132,
+ "startColumn": 4,
+ "endLine": 135,
+ "endColumn": 38,
+ "byteLength": 192
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strncat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 431,
+ "startColumn": 12,
+ "endLine": 431,
+ "endColumn": 58,
+ "byteLength": 46
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "dynamic_allocation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_alloc_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 39,
+ "startColumn": 4,
+ "endLine": 41,
+ "endColumn": 50,
+ "byteLength": 99
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "s_not_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 298,
+ "startColumn": 24,
+ "endLine": 298,
+ "endColumn": 34,
+ "byteLength": 10
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "room_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 397,
+ "startColumn": 26,
+ "endLine": 397,
+ "endColumn": 55,
+ "byteLength": 29
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "saveptr_subset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 308,
+ "startColumn": 28,
+ "endLine": 308,
+ "endColumn": 54,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strsignal." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 523,
+ "startColumn": 12,
+ "endLine": 523,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strlen." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 129,
+ "startColumn": 14,
+ "endLine": 129,
+ "endColumn": 20,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strsep." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 331,
+ "startColumn": 12,
+ "endLine": 331,
+ "endColumn": 20,
+ "byteLength": 8
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_internal_str." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 343,
+ "startColumn": 33,
+ "endLine": 343,
+ "endColumn": 59,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "MemSet." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 68,
+ "startColumn": 4,
+ "endLine": 70,
+ "endColumn": 70,
+ "byteLength": 156
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *((char *)s + (0 .. n - 1)) in function memset."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 116,
+ "startColumn": 12,
+ "endLine": 116,
+ "endColumn": 32,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strrchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 195,
+ "startColumn": 12,
+ "endLine": 195,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strndup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 506,
+ "startColumn": 12,
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_subset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 264,
+ "startColumn": 27,
+ "endLine": 264,
+ "endColumn": 72,
+ "byteLength": 45
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "behavior no_allocation in function strndup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 506,
+ "startColumn": 12,
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "allocates/frees clause in function strndup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 487,
+ "startColumn": 14,
+ "endLine": 487,
+ "endColumn": 21,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcsncmp_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 252,
+ "startColumn": 4,
+ "endLine": 256,
+ "endColumn": 60,
+ "byteLength": 208
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strcspn."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 199,
+ "startColumn": 12,
+ "endLine": 199,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strchrnul." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 179,
+ "startColumn": 12,
+ "endLine": 179,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_char." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 161,
+ "startColumn": 25,
+ "endLine": 161,
+ "endColumn": 44,
+ "byteLength": 19
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "WcsChr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 266,
+ "startColumn": 4,
+ "endLine": 269,
+ "endColumn": 29,
+ "byteLength": 167
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strlcat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_same_base." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 162,
+ "startColumn": 30,
+ "endLine": 162,
+ "endColumn": 66,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 157,
+ "startColumn": 29,
+ "endLine": 157,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strcspn." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 202,
+ "startColumn": 14,
+ "endLine": 202,
+ "endColumn": 21,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "bounded_result." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 453,
+ "startColumn": 28,
+ "endLine": 453,
+ "endColumn": 65,
+ "byteLength": 37
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "copied_contents." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 98,
+ "startColumn": 29,
+ "endLine": 98,
+ "endColumn": 76,
+ "byteLength": 47
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_valid_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 345,
+ "startColumn": 33,
+ "endLine": 345,
+ "endColumn": 59,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "room_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 410,
+ "startColumn": 26,
+ "endLine": 410,
+ "endColumn": 70,
+ "byteLength": 44
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 99,
+ "startColumn": 4,
+ "endLine": 101,
+ "endColumn": 59,
+ "byteLength": 124
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strdup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 470,
+ "startColumn": 12,
+ "endLine": 470,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strcasestr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 239,
+ "startColumn": 12,
+ "endLine": 239,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strcasecmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 50,
+ "startColumn": 11,
+ "endLine": 50,
+ "endColumn": 21,
+ "byteLength": 10
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "bounded_result." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 391,
+ "startColumn": 28,
+ "endLine": 391,
+ "endColumn": 50,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strncat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 439,
+ "startColumn": 12,
+ "endLine": 439,
+ "endColumn": 48,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest + (strlen{Old}(dest) .. n)) in function strlcat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 451,
+ "startColumn": 12,
+ "endLine": 451,
+ "endColumn": 33,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_create." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 111,
+ "startColumn": 4,
+ "endLine": 113,
+ "endColumn": 51,
+ "byteLength": 118
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strcasecmp."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 48,
+ "startColumn": 10,
+ "endLine": 48,
+ "endColumn": 17,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior resume_str in function strtok_r." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 327,
+ "startColumn": 12,
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function memmove." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 111,
+ "startColumn": 12,
+ "endLine": 111,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strtok_r." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 303,
+ "startColumn": 12,
+ "endLine": 303,
+ "endColumn": 20,
+ "byteLength": 8
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior found in function strrchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 195,
+ "startColumn": 12,
+ "endLine": 195,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_dest." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 449,
+ "startColumn": 32,
+ "endLine": 449,
+ "endColumn": 50,
+ "byteLength": 18
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 212,
+ "startColumn": 29,
+ "endLine": 212,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "cannot_allocate." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 479,
+ "startColumn": 29,
+ "endLine": 479,
+ "endColumn": 53,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_create_shift." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 115,
+ "startColumn": 4,
+ "endLine": 117,
+ "endColumn": 62,
+ "byteLength": 157
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 292,
+ "startColumn": 10,
+ "endLine": 292,
+ "endColumn": 17,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_nul_terminated." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 520,
+ "startColumn": 35,
+ "endLine": 520,
+ "endColumn": 51,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "sum_of_lengths." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 413,
+ "startColumn": 28,
+ "endLine": 413,
+ "endColumn": 76,
+ "byteLength": 48
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 86,
+ "startColumn": 25,
+ "endLine": 86,
+ "endColumn": 41,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term __fc_heap_status in function strndup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 492,
+ "startColumn": 12,
+ "endLine": 492,
+ "endColumn": 28,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s2." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 152,
+ "startColumn": 30,
+ "endLine": 152,
+ "endColumn": 51,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "separation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 366,
+ "startColumn": 4,
+ "endLine": 366,
+ "endColumn": 43,
+ "byteLength": 39
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strchr."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 158,
+ "startColumn": 12,
+ "endLine": 158,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_dest." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 104,
+ "startColumn": 25,
+ "endLine": 104,
+ "endColumn": 48,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *saveptr in function strtok_r."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 303,
+ "startColumn": 12,
+ "endLine": 303,
+ "endColumn": 20,
+ "byteLength": 8
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 275,
+ "startColumn": 12,
+ "endLine": 275,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "copied_contents." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 108,
+ "startColumn": 29,
+ "endLine": 108,
+ "endColumn": 76,
+ "byteLength": 47
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strsep." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 334,
+ "startColumn": 12,
+ "endLine": 334,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strncat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 431,
+ "startColumn": 12,
+ "endLine": 431,
+ "endColumn": 58,
+ "byteLength": 46
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "sum_of_lengths." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 434,
+ "startColumn": 28,
+ "endLine": 434,
+ "endColumn": 76,
+ "byteLength": 48
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strcpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 355,
+ "startColumn": 12,
+ "endLine": 355,
+ "endColumn": 32,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *((char *)dest + (0 .. n - 1)) in function memmove."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 106,
+ "startColumn": 12,
+ "endLine": 106,
+ "endColumn": 35,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_before_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 204,
+ "startColumn": 4,
+ "endLine": 205,
+ "endColumn": 76,
+ "byteLength": 105
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "ptr_subset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 279,
+ "startColumn": 24,
+ "endLine": 279,
+ "endColumn": 77,
+ "byteLength": 53
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strcasestr."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 233,
+ "startColumn": 12,
+ "endLine": 233,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "allocates/frees clause in function strdup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strncat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 444,
+ "startColumn": 12,
+ "endLine": 444,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function memmove." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 106,
+ "startColumn": 12,
+ "endLine": 106,
+ "endColumn": 35,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 448,
+ "startColumn": 31,
+ "endLine": 448,
+ "endColumn": 53,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strcspn." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 202,
+ "startColumn": 14,
+ "endLine": 202,
+ "endColumn": 21,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function memcmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 65,
+ "startColumn": 11,
+ "endLine": 65,
+ "endColumn": 17,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strncmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 149,
+ "startColumn": 11,
+ "endLine": 149,
+ "endColumn": 18,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strncasecmp."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 55,
+ "startColumn": 10,
+ "endLine": 55,
+ "endColumn": 17,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "memcmp_strlen_shift_left." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 127,
+ "startColumn": 4,
+ "endLine": 130,
+ "endColumn": 38,
+ "byteLength": 191
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function memcmp."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 61,
+ "startColumn": 12,
+ "endLine": 61,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "src_fits." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 372,
+ "startColumn": 22,
+ "endLine": 372,
+ "endColumn": 37,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strncmp."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 146,
+ "startColumn": 12,
+ "endLine": 146,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "memcmp_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 39,
+ "startColumn": 4,
+ "endLine": 42,
+ "endColumn": 77,
+ "byteLength": 184
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_in_length." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 163,
+ "startColumn": 30,
+ "endLine": 163,
+ "endColumn": 59,
+ "byteLength": 29
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "initialization." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 57,
+ "startColumn": 32,
+ "endLine": 57,
+ "endColumn": 68,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "StrNCmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 155,
+ "startColumn": 4,
+ "endLine": 159,
+ "endColumn": 60,
+ "byteLength": 205
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strndup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 502,
+ "startColumn": 12,
+ "endLine": 502,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strncasecmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 57,
+ "startColumn": 11,
+ "endLine": 57,
+ "endColumn": 22,
+ "byteLength": 11
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strcoll." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 155,
+ "startColumn": 11,
+ "endLine": 155,
+ "endColumn": 18,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest +\n (strlen{Old}(dest) ..\n strlen{Old}(dest) +\n strlen{Old}(src))) in function strcat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 411,
+ "startColumn": 12,
+ "endLine": 411,
+ "endColumn": 58,
+ "byteLength": 46
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function memcpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 101,
+ "startColumn": 12,
+ "endLine": 101,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "separation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 399,
+ "startColumn": 4,
+ "endLine": 399,
+ "endColumn": 59,
+ "byteLength": 55
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior new_str in function strtok." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 283,
+ "startColumn": 12,
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function memchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 88,
+ "startColumn": 12,
+ "endLine": 88,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_sup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 218,
+ "startColumn": 4,
+ "endLine": 220,
+ "endColumn": 52,
+ "byteLength": 112
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *(s + (0 ..)) in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 262,
+ "startColumn": 12,
+ "endLine": 262,
+ "endColumn": 18,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s1." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 137,
+ "startColumn": 30,
+ "endLine": 137,
+ "endColumn": 51,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_haystack." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 220,
+ "startColumn": 36,
+ "endLine": 220,
+ "endColumn": 63,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *stringp in function strsep."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 331,
+ "startColumn": 12,
+ "endLine": 331,
+ "endColumn": 20,
+ "byteLength": 8
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "separation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 387,
+ "startColumn": 4,
+ "endLine": 387,
+ "endColumn": 61,
+ "byteLength": 57
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior found in function strchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strcmp_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 143,
+ "startColumn": 4,
+ "endLine": 147,
+ "endColumn": 70,
+ "byteLength": 177
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 468,
+ "startColumn": 29,
+ "endLine": 468,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior not_found in function strchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 173,
+ "startColumn": 12,
+ "endLine": 173,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "WcsCmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 240,
+ "startColumn": 4,
+ "endLine": 244,
+ "endColumn": 70,
+ "byteLength": 180
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strtok_r." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 327,
+ "startColumn": 12,
+ "endLine": 327,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null_or_same_base." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 193,
+ "startColumn": 4,
+ "endLine": 193,
+ "endColumn": 60,
+ "byteLength": 56
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "initialization." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 416,
+ "startColumn": 4,
+ "endLine": 416,
+ "endColumn": 60,
+ "byteLength": 56
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "equal_contents." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 402,
+ "startColumn": 28,
+ "endLine": 402,
+ "endColumn": 49,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_pos_or_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 78,
+ "startColumn": 4,
+ "endLine": 82,
+ "endColumn": 40,
+ "byteLength": 183
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strdup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strdup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 473,
+ "startColumn": 12,
+ "endLine": 473,
+ "endColumn": 28,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_valid_string_and_same_contents." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 477,
+ "startColumn": 4,
+ "endLine": 477,
+ "endColumn": 51,
+ "byteLength": 47
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strtok." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 283,
+ "startColumn": 12,
+ "endLine": 283,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "room_nstring." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 450,
+ "startColumn": 27,
+ "endLine": 450,
+ "endColumn": 48,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "memcmp_strlen_shift_right." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 132,
+ "startColumn": 4,
+ "endLine": 135,
+ "endColumn": 38,
+ "byteLength": 192
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "src_too_long." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 375,
+ "startColumn": 26,
+ "endLine": 375,
+ "endColumn": 42,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strsignal." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 523,
+ "startColumn": 12,
+ "endLine": 523,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "can_allocate." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 472,
+ "startColumn": 26,
+ "endLine": 472,
+ "endColumn": 49,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_pos_or_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 193,
+ "startColumn": 4,
+ "endLine": 197,
+ "endColumn": 41,
+ "byteLength": 188
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strncmp_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 155,
+ "startColumn": 4,
+ "endLine": 159,
+ "endColumn": 60,
+ "byteLength": 205
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s1." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 53,
+ "startColumn": 28,
+ "endLine": 53,
+ "endColumn": 53,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strsep."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 332,
+ "startColumn": 12,
+ "endLine": 332,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior allocation in function strdup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 484,
+ "startColumn": 12,
+ "endLine": 484,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 181,
+ "startColumn": 29,
+ "endLine": 181,
+ "endColumn": 49,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "char_not_found." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 167,
+ "startColumn": 28,
+ "endLine": 167,
+ "endColumn": 40,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_needle." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 232,
+ "startColumn": 34,
+ "endLine": 232,
+ "endColumn": 59,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior found in function memchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 88,
+ "startColumn": 12,
+ "endLine": 88,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_same_base." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 186,
+ "startColumn": 30,
+ "endLine": 186,
+ "endColumn": 66,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_bounded." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 208,
+ "startColumn": 28,
+ "endLine": 208,
+ "endColumn": 53,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "acsl_c_equiv." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 140,
+ "startColumn": 26,
+ "endLine": 140,
+ "endColumn": 50,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_not_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 210,
+ "startColumn": 4,
+ "endLine": 212,
+ "endColumn": 59,
+ "byteLength": 124
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strdup."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 474,
+ "startColumn": 12,
+ "endLine": 474,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strrchr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 195,
+ "startColumn": 12,
+ "endLine": 195,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "allocation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 495,
+ "startColumn": 24,
+ "endLine": 495,
+ "endColumn": 60,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s2." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 145,
+ "startColumn": 30,
+ "endLine": 145,
+ "endColumn": 55,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strncat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 425,
+ "startColumn": 12,
+ "endLine": 425,
+ "endColumn": 50,
+ "byteLength": 38
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "never_allocable." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_alloc_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 39,
+ "startColumn": 4,
+ "endLine": 41,
+ "endColumn": 50,
+ "byteLength": 99
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 504,
+ "startColumn": 25,
+ "endLine": 504,
+ "endColumn": 41,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strndup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 506,
+ "startColumn": 12,
+ "endLine": 506,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "initialization." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 307,
+ "startColumn": 28,
+ "endLine": 307,
+ "endColumn": 49,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_valid_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 521,
+ "startColumn": 33,
+ "endLine": 521,
+ "endColumn": 59,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "WcsNCmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 252,
+ "startColumn": 4,
+ "endLine": 256,
+ "endColumn": 60,
+ "byteLength": 208
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "sum_of_bounded_lengths." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 442,
+ "startColumn": 36,
+ "endLine": 442,
+ "endColumn": 74,
+ "byteLength": 38
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "points_to_end." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 403,
+ "startColumn": 27,
+ "endLine": 403,
+ "endColumn": 57,
+ "byteLength": 30
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_s." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 115,
+ "startColumn": 22,
+ "endLine": 115,
+ "endColumn": 42,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strxfrm."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 461,
+ "startColumn": 12,
+ "endLine": 461,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function memcpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 97,
+ "startColumn": 12,
+ "endLine": 97,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wmemchr_def." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 183,
+ "startColumn": 4,
+ "endLine": 185,
+ "endColumn": 63,
+ "byteLength": 150
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strtok." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 261,
+ "startColumn": 12,
+ "endLine": 261,
+ "endColumn": 27,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strnlen."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 132,
+ "startColumn": 12,
+ "endLine": 132,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. strlen{Old}(src))) in function stpcpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 400,
+ "startColumn": 12,
+ "endLine": 400,
+ "endColumn": 32,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_subset." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 277,
+ "startColumn": 27,
+ "endLine": 278,
+ "endColumn": 72,
+ "byteLength": 92
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strxfrm." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 460,
+ "startColumn": 12,
+ "endLine": 460,
+ "endColumn": 26,
+ "byteLength": 14
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strncasecmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 57,
+ "startColumn": 11,
+ "endLine": 57,
+ "endColumn": 22,
+ "byteLength": 11
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "room_nstring." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 385,
+ "startColumn": 27,
+ "endLine": 385,
+ "endColumn": 48,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "room_string." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 352,
+ "startColumn": 26,
+ "endLine": 352,
+ "endColumn": 55,
+ "byteLength": 29
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_ptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 427,
+ "startColumn": 24,
+ "endLine": 427,
+ "endColumn": 39,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_dest." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 458,
+ "startColumn": 25,
+ "endLine": 458,
+ "endColumn": 48,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strspn."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 206,
+ "startColumn": 12,
+ "endLine": 206,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strerror." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 347,
+ "startColumn": 12,
+ "endLine": 347,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_src_too_large." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 437,
+ "startColumn": 4,
+ "endLine": 437,
+ "endColumn": 49,
+ "byteLength": 45
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "MemCmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 39,
+ "startColumn": 4,
+ "endLine": 42,
+ "endColumn": 77,
+ "byteLength": 184
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "wcslen_zero." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 214,
+ "startColumn": 4,
+ "endLine": 216,
+ "endColumn": 60,
+ "byteLength": 121
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strncpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 368,
+ "startColumn": 12,
+ "endLine": 368,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function memcpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 96,
+ "startColumn": 12,
+ "endLine": 96,
+ "endColumn": 35,
+ "byteLength": 23
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "specialization of valid_string_s at stmt 2."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri":
+ "REPLACED_FOR_PTESTS_PWD/tests/sarif/libc.c"
+ },
+ "region": {
+ "startLine": 11,
+ "startColumn": 10,
+ "endLine": 11,
+ "endColumn": 19,
+ "byteLength": 9
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_stringp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 329,
+ "startColumn": 35,
+ "endLine": 329,
+ "endColumn": 76,
+ "byteLength": 41
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strlen_neg." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 84,
+ "startColumn": 4,
+ "endLine": 87,
+ "endColumn": 22,
+ "byteLength": 116
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strstr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 229,
+ "startColumn": 12,
+ "endLine": 229,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_needle." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 221,
+ "startColumn": 34,
+ "endLine": 221,
+ "endColumn": 59,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "initialization." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 390,
+ "startColumn": 28,
+ "endLine": 390,
+ "endColumn": 73,
+ "byteLength": 45
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "memset_def." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 68,
+ "startColumn": 4,
+ "endLine": 70,
+ "endColumn": 70,
+ "byteLength": 156
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_ptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 369,
+ "startColumn": 24,
+ "endLine": 369,
+ "endColumn": 39,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strncat."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 426,
+ "startColumn": 12,
+ "endLine": 426,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strlcpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 389,
+ "startColumn": 12,
+ "endLine": 389,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strchrnul." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 179,
+ "startColumn": 12,
+ "endLine": 179,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "acsl_c_equiv." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 118,
+ "startColumn": 26,
+ "endLine": 118,
+ "endColumn": 46,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strlen."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 126,
+ "startColumn": 12,
+ "endLine": 126,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(dest + (0 .. n - 1)) in function strlcpy."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 388,
+ "startColumn": 12,
+ "endLine": 388,
+ "endColumn": 24,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function strncmp." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 149,
+ "startColumn": 11,
+ "endLine": 149,
+ "endColumn": 18,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strndup." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 492,
+ "startColumn": 12,
+ "endLine": 492,
+ "endColumn": 28,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_delim." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 330,
+ "startColumn": 33,
+ "endLine": 330,
+ "endColumn": 57,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strpbrk." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 218,
+ "startColumn": 12,
+ "endLine": 218,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 482,
+ "startColumn": 25,
+ "endLine": 482,
+ "endColumn": 41,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_memory_area." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 36,
+ "startColumn": 32,
+ "endLine": 36,
+ "endColumn": 63,
+ "byteLength": 31
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s_or_delim_not_found." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 300,
+ "startColumn": 6,
+ "endLine": 302,
+ "endColumn": 70,
+ "byteLength": 120
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strspn."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 207,
+ "startColumn": 12,
+ "endLine": 207,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_ptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 119,
+ "startColumn": 24,
+ "endLine": 119,
+ "endColumn": 36,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term __fc_strtok_ptr in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 252,
+ "startColumn": 10,
+ "endLine": 252,
+ "endColumn": 25,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strcat." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 411,
+ "startColumn": 12,
+ "endLine": 411,
+ "endColumn": 58,
+ "byteLength": 46
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function stpcpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 405,
+ "startColumn": 12,
+ "endLine": 405,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "zero_initialized." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 39,
+ "startColumn": 28,
+ "endLine": 39,
+ "endColumn": 63,
+ "byteLength": 35
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_char." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 185,
+ "startColumn": 25,
+ "endLine": 185,
+ "endColumn": 38,
+ "byteLength": 13
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_s2." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 56,
+ "startColumn": 23,
+ "endLine": 56,
+ "endColumn": 49,
+ "byteLength": 26
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function stpcpy." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 400,
+ "startColumn": 12,
+ "endLine": 400,
+ "endColumn": 32,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strstr."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 222,
+ "startColumn": 12,
+ "endLine": 222,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function strrchr."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 182,
+ "startColumn": 12,
+ "endLine": 182,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function strnlen." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 135,
+ "startColumn": 14,
+ "endLine": 135,
+ "endColumn": 21,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_s2." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/strings.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 54,
+ "startColumn": 28,
+ "endLine": 54,
+ "endColumn": 53,
+ "byteLength": 25
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *(s + (0 ..)) in function strtok."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 246,
+ "startColumn": 10,
+ "endLine": 246,
+ "endColumn": 16,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_src." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/string.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 408,
+ "startColumn": 31,
+ "endLine": 408,
+ "endColumn": 53,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "strchr_def." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "/libc/__fc_string_axiomatic.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 168,
+ "startColumn": 4,
+ "endLine": 170,
+ "endColumn": 82,
+ "byteLength": 146
+ }
+ }
+ }
+ ]
+ }
+ ],
+ "defaultSourceLanguage": "C",
+ "taxonomies": [
+ {
+ "name": "frama-c",
+ "rules": [
+ {
+ "id": "user-spec",
+ "shortDescription": {
+ "text": "User-written ACSL specification."
+ }
+ }
+ ],
+ "contents": [ "nonLocalizedData" ]
+ }
+ ]
+ }
+ ]
+}
\ No newline at end of file
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif.clean b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif.clean
new file mode 100644
index 0000000000000000000000000000000000000000..ba8d4dd7921a16588bbc57a8427e80c08307586d
--- /dev/null
+++ b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif.clean
@@ -0,0 +1,89 @@
+{
+ "$schema":
+ "https://github.com/oasis-tcs/sarif-spec/blob/master/Documents/CommitteeSpecificationDrafts/v2.1.0-CSD.1/sarif-schema-2.1.0.json",
+ "version": "2.1.0",
+ "runs": [
+ {
+ "tool": {
+ "driver": {
+ "name": "frama-c",
+ "fullName": "frama-c-21.1+dev (Scandium)",
+ "version": "21.1+dev (Scandium)",
+ "semanticVersion": "21.1+dev",
+ "downloadUri": "https://frama-c.com/download.html"
+ }
+ },
+ "invocations": [
+ {
+ "commandLine":
+ "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -mdr-gen sarif -mdr-out tests/sarif/oracle/without-libc.sarif -mdr-no-print-libc",
+ "arguments": [
+ "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
+ "-load-module", "eva,from,scope,markdown_report", "-eva",
+ "-mdr-gen", "sarif", "-mdr-out",
+ "tests/sarif/oracle/without-libc.sarif", "-mdr-no-print-libc"
+ ],
+ "exitCode": 0,
+ "executionSuccessful": true
+ }
+ ],
+ "originalUriBaseIds": {
+ "FRAMAC_SHARE": { "uri": "REPLACED_FOR_PTESTS_FRAMAC_SHARE" },
+ "FRAMAC_LIB": { "uri": "REPLACED_FOR_PTESTS_FRAMAC_LIB" },
+ "FRAMAC_PLUGIN": { "uri": "REPLACED_FOR_PTESTS_FRAMAC_PLUGIN" },
+ "PWD": {
+ "uri": "REPLACED_FOR_PTESTS_PWD"
+ }
+ },
+ "artifacts": [
+ {
+ "location": { "uri": "tests/sarif/libc.c" },
+ "roles": [ "analysisTarget" ],
+ "mimeType": "text/x-csrc"
+ }
+ ],
+ "results": [
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "specialization of valid_string_s at stmt 2."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri":
+ "REPLACED_FOR_PTESTS_PWD/tests/sarif/libc.c"
+ },
+ "region": {
+ "startLine": 11,
+ "startColumn": 10,
+ "endLine": 11,
+ "endColumn": 19,
+ "byteLength": 9
+ }
+ }
+ }
+ ]
+ }
+ ],
+ "defaultSourceLanguage": "C",
+ "taxonomies": [
+ {
+ "name": "frama-c",
+ "rules": [
+ {
+ "id": "user-spec",
+ "shortDescription": {
+ "text": "User-written ACSL specification."
+ }
+ }
+ ],
+ "contents": [ "nonLocalizedData" ]
+ }
+ ]
+ }
+ ]
+}
\ No newline at end of file