Source file sva_dummy.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
(**************************************************************************)
(*  This file is part of the Codex semantics library.                     *)
(*                                                                        *)
(*  Copyright (C) 2013-2025                                               *)
(*    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 LICENSE).                      *)
(*                                                                        *)
(**************************************************************************)

(* Useful to complete functors. That way, everybody can take All
   as a parameter. *)

open Sva_sig

module Make(UnimplementedId:sig val loc:string end) = struct

  module Dummy_Enum_Lattice = Lattices.Unimplemented.Enum_Lattice(UnimplementedId)
  module Dummy_Integer_Lattice = Lattices.Unimplemented.Integer_Lattice(struct
      type t = unit
      include UnimplementedId end)    

  module Complete_Binary(B:BITVECTOR):ALL
    with type bitvector = B.bitvector
     and type boolean = B.boolean
  = struct
    include B
    module Memory_Lattice = Lattices.Unit
    type memory = Memory_Lattice.t
    module Memory_Backward = Sva_noop_transfer_functions.Memory_Backward
    module Memory_Forward = Sva_noop_transfer_functions.Memory_Forward

    module Block_Lattice = Lattices.Unit
    type block = Memory_Lattice.t
    module Block_Backward = Sva_noop_transfer_functions.Block_Backward
    module Block_Forward = Sva_noop_transfer_functions.Block_Forward

    module Integer_Lattice = Dummy_Integer_Lattice
    type integer = Integer_Lattice.t
    module Integer_Backward = Sva_Assert_False_Transfer_Functions.Integer_Backward
    module Integer_Forward = Sva_Assert_False_Transfer_Functions.Integer_Forward

    module Enum_Lattice = Dummy_Enum_Lattice
    type enum = Enum_Lattice.t
    module Enum_Backward = Sva_Assert_False_Transfer_Functions.Enum_Backward
    module Enum_Forward = Sva_Assert_False_Transfer_Functions.Enum_Forward
  end

  module Complete_Bitvector_Enum(B:BITVECTOR_ENUM):ALL
    with type bitvector = B.bitvector
     and type boolean = B.boolean
  = struct
    include B
    module Memory_Lattice = Lattices.Unit
    type memory = Memory_Lattice.t
    module Memory_Backward = Sva_noop_transfer_functions.Memory_Backward
    module Memory_Forward = Sva_noop_transfer_functions.Memory_Forward

    module Integer_Lattice = Dummy_Integer_Lattice
    type integer = Integer_Lattice.t
    module Integer_Backward = Sva_Assert_False_Transfer_Functions.Integer_Backward
    module Integer_Forward = Sva_Assert_False_Transfer_Functions.Integer_Forward

    module Block_Lattice = Lattices.Unit
    type block = Memory_Lattice.t
    module Block_Backward = Sva_noop_transfer_functions.Block_Backward
    module Block_Forward = Sva_noop_transfer_functions.Block_Forward
  end

  module Complete_Integer(B:INTEGER):ALL
    with type integer = B.integer
     and type boolean = B.boolean
  = struct
    include B
    module Memory_Lattice = Lattices.Unit
    type memory = Memory_Lattice.t
    module Memory_Backward = Sva_noop_transfer_functions.Memory_Backward
    module Memory_Forward = Sva_noop_transfer_functions.Memory_Forward

    module Block_Lattice = Lattices.Unit
    type block = Memory_Lattice.t
    module Block_Backward = Sva_noop_transfer_functions.Block_Backward
    module Block_Forward = Sva_noop_transfer_functions.Block_Forward

    module Bitvector_Lattice =  Lattices.Unimplemented.Bitvector_Lattice(struct
        type t = unit
        let loc = __LOC__
      end)

    type bitvector = Bitvector_Lattice.t
    module Bitvector_Backward = Sva_Assert_False_Transfer_Functions.Bitvector_Backward
    module Bitvector_Forward = Sva_Assert_False_Transfer_Functions.Bitvector_Forward

    module Enum_Lattice = Dummy_Enum_Lattice  
    type enum = Enum_Lattice.t
    module Enum_Backward = Sva_Assert_False_Transfer_Functions.Enum_Backward
    module Enum_Forward = Sva_Assert_False_Transfer_Functions.Enum_Forward

  end

  module Dummy_All:ALL = struct

    let _name = "Dummy"

    include Sva_quadrivalent

    module Integer_Lattice = Dummy_Integer_Lattice
    type integer = Integer_Lattice.t
    module Integer_Backward = Sva_Assert_False_Transfer_Functions.Integer_Backward
    module Integer_Forward = Sva_Assert_False_Transfer_Functions.Integer_Forward

    module Bitvector_Lattice =  Lattices.Unimplemented.Bitvector_Lattice(struct
        type t = unit
        let loc = __LOC__
      end)

    type bitvector = Bitvector_Lattice.t
    module Bitvector_Backward = Sva_Assert_False_Transfer_Functions.Bitvector_Backward
    module Bitvector_Forward = Sva_Assert_False_Transfer_Functions.Bitvector_Forward

    module Enum_Lattice = Dummy_Enum_Lattice
    type enum = Enum_Lattice.t
    module Enum_Backward = Sva_Assert_False_Transfer_Functions.Enum_Backward
    module Enum_Forward = Sva_Assert_False_Transfer_Functions.Enum_Forward

    module Memory_Lattice = Lattices.Unit
    type memory = Memory_Lattice.t
    module Memory_Backward = Sva_noop_transfer_functions.Memory_Backward
    module Memory_Forward = Sva_noop_transfer_functions.Memory_Forward

    module Block_Lattice = Lattices.Unit
    type block = Memory_Lattice.t
    module Block_Backward = Sva_noop_transfer_functions.Block_Backward
    module Block_Forward = Sva_noop_transfer_functions.Block_Forward
  end
end