package goblint-cil

You can search for identifiers within the package.

in-package search v0.2.0

A front-end for the C programming language that facilitates program analysis and transformation

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

Maintainers

Sources

goblint-cil-2.0.6.tbz

sha256=5577007bfac63c3f0609abdb74119fe674c9bc8529d790e90ef73a85964aa07a

sha512=f1a393fa92614ceaf857bec4df474d3e152c578d0ab5fdf791e9129668861ccaa37efae2f18aa539965d6c2ed4dabb47b4a5262aab55112e181935def06f18da

doc/src/goblint-cil.syntacticsearch/resultPrinter.ml.html

Source file `resultPrinter.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
open GoblintCil
open CodeQuery
open Feature

let rec contains list elem =
  match list with
  | x :: xs -> if elem = x then true else contains xs elem
  | [] -> false

let rec get_max_lengths result_list name_l line_l file_l byte_l typ_l id_l =
  match result_list with
  | (name, loc, typ, id) :: xs ->
      get_max_lengths xs
        (max name_l (String.length name))
        (max line_l (String.length (string_of_int loc.line)))
        (max file_l (String.length loc.file))
        (max byte_l (String.length (string_of_int loc.byte)))
        (max typ_l (String.length typ))
        (max id_l (String.length (string_of_int id)))
  | [] -> (name_l, line_l, file_l, byte_l, typ_l, id_l)

let print_result result query =
  let print_name = contains query.sel Name_sel in
  let print_loc = contains query.sel Location_sel in
  let print_typ = contains query.sel Type_sel in
  let print_id = contains query.sel ID_sel in
  let max_lengths = get_max_lengths result 0 0 0 0 0 0 in
  let name_l = match max_lengths with x, _, _, _, _, _ -> x in
  let line_l = match max_lengths with _, x, _, _, _, _ -> x in
  let file_l = match max_lengths with _, _, x, _, _, _ -> x in
  let byte_l = match max_lengths with _, _, _, x, _, _ -> x in
  let typ_l = match max_lengths with _, _, _, _, x, _ -> x in
  let id_l = match max_lengths with _, _, _, _, _, x -> x in
  let rec add_whitespace num =
    if num <= 0 then "" else " " ^ add_whitespace (num - 1)
  in
  let create_name name =
    if print_name then
      "name: " ^ name ^ add_whitespace (name_l - String.length name) ^ ", "
    else ""
  in
  let create_location loc =
    if print_loc then
      "line: " ^ string_of_int loc.line
      ^ add_whitespace (line_l - String.length (string_of_int loc.line))
      ^ ", file: " ^ loc.file
      ^ add_whitespace (file_l - String.length loc.file)
      ^ ", byte: " ^ string_of_int loc.byte
      ^ add_whitespace (byte_l - String.length (string_of_int loc.byte))
      ^ ", "
    else ""
  in
  let create_type typ =
    if print_typ then
      "type: " ^ typ ^ add_whitespace (typ_l - String.length typ) ^ ", "
    else ""
  in
  let create_id id =
    if print_id then
      "id: " ^ string_of_int id
      ^ add_whitespace (id_l - String.length (string_of_int id))
      ^ ""
    else ""
  in
  let create_entry (name, loc, typ, id) =
    create_name name ^ create_location loc ^ create_type typ ^ create_id id
    ^ "\n"
  in
  let rec create_printout list =
    match list with x :: xs -> create_entry x ^ create_printout xs | [] -> ""
  in
  if print_name || print_loc || print_typ || print_id then
    create_printout result
  else ""

let query_file_name = ref ""

let feature = {
  fd_name = "syntacticsearch";
  fd_enabled = false;
  fd_description = "Syntactic Search in CIL programs";
  fd_extraopt = [
    ("--syntacticsearch_query_file",
     Arg.Set_string query_file_name,
     "<fname> Name of the file containing the syntactic search query")
  ];
  fd_doit = (fun f ->
    Printexc.record_backtrace true;
    let q = CodeQuery.parse_json_file !query_file_name in
    let results = QueryMapping.map_query q f in
    print_endline (print_result results q));
  fd_post_check = false
}

let () = Feature.register feature