package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file classify.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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Format_types
open Va_types
open Options
module Typ = Extends.Typ


(* ************************************************************************ *)
(* Variadic classes builders                                                *)
(* ************************************************************************ *)

let find_function env s =
  try
    Some (Environment.find_function env s)
  with Not_found ->
    Self.warning ~wkey:wkey_libc_framac
      "Unable to locate function %s which should be in the Frama-C LibC."
      s;
    None

let mk_overload env names =
  let vis = List.filter_map (find_function env) names in
  let overload = List.map (fun vi -> Typ.params_types vi.vtype, vi) vis in
  Overload overload

let mk_aggregator env fun_name a_pos pname a_type =
  match find_function env fun_name with
  | None -> Misc
  | Some vi ->
    try
      (* Get the list of arguments *)
      let params = Typ.params vi.vtype in

      (* Check that pos is a valid position in the list *)
      assert (a_pos >= 0);
      if a_pos >= List.length params then begin
        Self.warning ~current:true ~wkey:wkey_libc
          "The standard function %s should have at least %d parameters."
          fun_name
          (a_pos + 1);
        raise Exit
      end;

      (* Get the aggregate type of elements *)
      let _,ptyp,_ = List.nth params a_pos in
      let a_param = pname, match ptyp with
        | TArray (typ,_,_)
        | TPtr (typ, _) -> typ
        | _ ->
          Self.warning ~current:true ~wkey:wkey_libc
            "The parameter %d of standard function %s should be \
             of array type."
            (a_pos + 1)
            fun_name;
          raise Exit
      in

      Aggregator {a_target = vi; a_pos; a_type; a_param}

    (* In case of failure return Misc (apply generic translation) *)
    with Exit -> Misc

let mk_format_fun vi f_kind f_buffer ~format_pos =
  let buffer_arguments = match f_buffer with
    | StdIO | Syslog -> []
    | File i | Stream i | Arg (i, None) -> [i]
    | Arg (i, Some j) -> [i ; j]
  in
  let expected_args = buffer_arguments @ [ format_pos ] in
  let n_expected_args = (List.fold_left max (-1) expected_args) + 1
  and n_actual_args = List.length (Typ.params vi.vtype) in
  if n_actual_args < n_expected_args then
    begin
      Self.warning ~current:true ~wkey:wkey_libc
        "The standard function %s was expected to have at least %d fixed \
         parameters but only has %d.@ \
         No variadic translation will be performed."
        vi.vname
        n_expected_args
        n_actual_args;
      Misc
    end
  else
    FormatFun { f_kind ; f_buffer ; f_format_pos = format_pos }


(* ************************************************************************ *)
(* Classification                                                           *)
(* ************************************************************************ *)

let is_frama_c_builtin name =
  Ast_info.start_with_frama_c_builtin name ||
  Cil_builtins.Builtin_functions.mem name ||
  String.starts_with ~prefix:"__FRAMAC_" name (* Mthread prefixes *)

let va_builtins = [
  "__builtin_va_start";
  "__builtin_va_copy";
  "__builtin_va_arg";
  "__builtin_va_end";
]

let is_va_builtin s = List.mem s va_builtins

let classify_std env vi = match vi.vname with
  (* fcntl.h - Overloads of functions *)
  | "fcntl" -> mk_overload env
                 ["__va_fcntl_void" ; "__va_fcntl_int" ; "__va_fcntl_flock"]
  | "open" -> mk_overload env
                ["__va_open_void" ; "__va_open_mode_t"]
  | "openat" -> mk_overload env
                  ["__va_openat_void" ; "__va_openat_mode_t"]

  (* unistd.h *)
  | "execl"   -> mk_aggregator env "execv" 1 "argv" EndedByNull
  | "execle"  -> mk_aggregator env "execve" 1 "argv" EndedByNull
  | "execlp"  -> mk_aggregator env "execvp" 1 "argv" EndedByNull
  | "syscall" -> Misc

  (* stdio.h *)
  | "fprintf"  -> mk_format_fun vi PrintfLike ~format_pos:1 (Stream 0)
  | "printf"   -> mk_format_fun vi PrintfLike ~format_pos:0 (StdIO)
  | "sprintf"  -> mk_format_fun vi PrintfLike ~format_pos:1 (Arg (0, None))
  | "snprintf" -> mk_format_fun vi PrintfLike ~format_pos:2 (Arg (0, Some 1))
  | "dprintf"  -> mk_format_fun vi PrintfLike ~format_pos:1 (File 0)
  | "fscanf"   -> mk_format_fun vi ScanfLike  ~format_pos:1 (Stream 0)
  | "scanf"    -> mk_format_fun vi ScanfLike  ~format_pos:0 (StdIO)
  | "sscanf"   -> mk_format_fun vi ScanfLike  ~format_pos:1 (Arg (0, None))

  (* syslog.h *)
  | "syslog"   -> mk_format_fun vi PrintfLike ~format_pos:1 (Syslog)

  (* wchar.h *)
  | "fwprintf" -> mk_format_fun vi PrintfLike ~format_pos:1 (Stream 0)
  | "swprintf" -> mk_format_fun vi PrintfLike ~format_pos:2 (Arg (0, Some 1))
  | "wprintf"  -> mk_format_fun vi PrintfLike ~format_pos:0 (StdIO)
  | "fwscanf"  -> mk_format_fun vi ScanfLike  ~format_pos:1 (Stream 0)
  | "swscanf"  -> mk_format_fun vi ScanfLike  ~format_pos:1 (Arg (0, None))
  | "wscanf"   -> mk_format_fun vi ScanfLike  ~format_pos:0 (StdIO)

  (* stropts.h *)
  | "ioctl"   -> mk_overload env ["__va_ioctl_void" ; "__va_ioctl_int" ; "__va_ioctl_ptr"]
  | n when String.starts_with ~prefix:"__sync_" n -> Misc
  | n when is_va_builtin n -> Misc
  | n when is_frama_c_builtin n -> Builtin
  (* Anything else *)
  | _ -> Unknown

let is_variadic_function vi =
  match Cil.unrollType vi.vtype with
  | TFun (_, _, b, _) -> b
  |  _ -> false

let classify env vi =
  if is_variadic_function vi then begin
    Self.result ~level:2 ~current:true
      "Declaration of variadic function %s." vi.vname;
    Some {
      vf_decl = vi;
      vf_original_type = vi.vtype;
      vf_class = if vi.vdefined then Defined else classify_std env vi;
      vf_specialization_count = 0
    }
  end else
    None
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct