package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

dune-project
 Dependency

Authors

Maintainers

Sources

goblint-2.6.0.tbz
sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41
sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71

doc/src/goblint.constraint/varQuery.ml.html

Source file varQuery.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
open GoblintCil

type t =
  | Global of CilType.Varinfo.t
  | Node of {node: Node.t; fundec: CilType.Fundec.t option}
[@@deriving ord]

type 'v f = 'v -> unit

let varinfo_from_global (g : Cil.global) : Cil.varinfo option = match g with
  | GFun (f, _) -> Some f.svar
  | GVar (v, _, _) -> Some v
  | GVarDecl (v, _) -> Some v
  | _ -> None

let varquery_from_global (g : Cil.global) : t option = match g with
  | GFun (f, _) -> Some (Node {node = FunctionEntry f; fundec = Some f})
  | GVar (v, _, _) -> Some (Global v)
  | GVarDecl (v, _) -> Some (Global v)
  | _ -> None

let varqueries_from_names (file: Cil.file) (names: string list): t list * string list =
  let module SM = Set.Make(Printable.Strings) in
  let set = SM.of_list names in

  (* Find list of [Cil.global]s that have one of the queried names, and a set of the found names *)
  let globals, matched =
    Cil.foldGlobals file (fun ((globs, matched) as acc) g ->
        match varinfo_from_global g, varquery_from_global g with
        | Some v, Some vq ->
          begin match SM.mem v.vname set  with
            | true -> (vq::globs, SM.add v.vname matched)
            | _ -> acc
          end
        | None, None -> acc
        | _, _ -> assert false
      ) ([], SM.empty) in
  (* List of queried but not found names *)
  let unmatched = List.filter (fun s -> not @@ SM.mem s matched) names in
  globals, unmatched