[Markdown-report] add option -mdr-print-libc/-mdr-no-print-libc

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)

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

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 [])
 

src/plugins/markdown-report/tests/sarif/libc.c

+/* 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;
+}

src/plugins/markdown-report/tests/sarif/oracle/libc.res.oracle

+[kernel] Parsing tests/sarif/libc.c (with preprocessing)

src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif.clean

+{
+  "$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