gmp_types.ml 4.21 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
(*                                                                        *)
(*  Copyright (C) 2012-2018                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

23
24
(** GMP Values. *)

25
26
27
open Cil_types

(**************************************************************************)
28
(***************************** GMP types***********************************)
29
30
(**************************************************************************)

31
let mk_dummy_type_info_ref () =
32
33
34
35
36
37
  ref
    { torig_name = "";
      tname = "";
      ttype = TVoid [];
      treferenced = false }

38
39
module type S = sig
  val t: unit -> typ
40
  val t_as_ptr: unit -> typ
41
42
43
44
45
  val is_now_referenced: unit -> unit
  val is_t: typ -> bool
end

module Make(X: sig end) = struct
46

47
  let t_torig_ref = mk_dummy_type_info_ref ()
48
  let t_struct_torig_ref = mk_dummy_type_info_ref ()
49

50
51
  let set_t ty = t_torig_ref := ty
  let set_t_struct ty = t_struct_torig_ref := ty
52

53
  let is_now_referenced () = !t_torig_ref.treferenced <- true
54

55
  let t () = TNamed(!t_torig_ref, [])
56

57
58
59
  (* create a unique shared representation in order to use [==] in [is_t] *)
  let t_as_ptr_info =
    lazy
60
61
      {
        torig_name = "";
62
        tname = !t_struct_torig_ref.tname ^ " *";
63
64
65
66
67
68
        ttype = TArray(
            TNamed(!t_struct_torig_ref, []),
            Some (Cil.one ~loc:Cil_datatype.Location.unknown),
            {scache = Not_Computed},
            []);
        treferenced = true;
69
70
71
72
73
74
75
76
77
      }

  let t_as_ptr () = TNamed (Lazy.force t_as_ptr_info, [])

  let is_t ty = match ty with
    | TNamed(tinfo, []) ->
      tinfo == !t_torig_ref || tinfo == Lazy.force t_as_ptr_info
    | _ -> false

78
79
end

80
module Z = Make(struct end)
81
module Q = Make(struct end)
82
83
84
85
86

(**************************************************************************)
(******************* Initialization of mpz and mpq types ******************)
(**************************************************************************)

87
let init () =
88
  Options.feedback ~level:2 "initializing GMP types.";
Julien Signoles's avatar
Julien Signoles committed
89
  let set_mp_t = object (self)
90
    inherit Cil.nopCilVisitor
Julien Signoles's avatar
Julien Signoles committed
91

92
93
    (* exit after having initialized the 4 values (for Z.t and Q.t) *)
    val mutable visited = 0
Julien Signoles's avatar
Julien Signoles committed
94
95
    method private set f info =
      f info;
96
      if visited = 3 then
Julien Signoles's avatar
Julien Signoles committed
97
98
        raise Exit
      else begin
99
        visited <- visited + 1;
Julien Signoles's avatar
Julien Signoles committed
100
101
102
        Cil.SkipChildren
      end

103
    method !vglob = function
104
105
106
107
108
109
110
111
      | GType({ torig_name = name } as info, _) ->
        if name = "__e_acsl_mpz_t" then self#set Z.set_t info
        else if name = "__e_acsl_mpz_struct" then self#set Z.set_t_struct info
        else if name = "__e_acsl_mpq_t" then self#set Q.set_t info
        else if name = "__e_acsl_mpq_struct" then self#set Q.set_t_struct info
        else Cil.SkipChildren
      | _ ->
        Cil.SkipChildren
Julien Signoles's avatar
Julien Signoles committed
112

113
  end in
Julien Signoles's avatar
Julien Signoles committed
114
  try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()