Skip to content

Commit 3ba92c5

Browse files
committed
Remove deprecated Cil.featureDescr
Replaced by Feature.t. Note that fd_enabled has been changed, from a bool ref to a mutable bool field.
1 parent 2dbad8f commit 3ba92c5

35 files changed

+124
-154
lines changed

src/cil.ml

-27
Original file line numberDiff line numberDiff line change
@@ -866,33 +866,6 @@ and typsig =
866866
| TSEnum of string * attribute list
867867
| TSBase of typ
868868

869-
870-
871-
(** To be able to add/remove features easily, each feature should be packaged
872-
* as an interface with the following interface. These features should be *)
873-
type featureDescr = {
874-
fd_enabled: bool ref;
875-
(** The enable flag. Set to default value *)
876-
877-
fd_name: string;
878-
(** This is used to construct an option "--doxxx" and "--dontxxx" that
879-
* enable and disable the feature *)
880-
881-
fd_description: string;
882-
(* A longer name that can be used to document the new options *)
883-
884-
fd_extraopt: (string * Arg.spec * string) list;
885-
(** Additional command line options. The description strings should
886-
usually start with a space for Arg.align to print the --help nicely. *)
887-
888-
fd_doit: (file -> unit);
889-
(** This performs the transformation *)
890-
891-
fd_post_check: bool;
892-
(* Whether to perform a CIL consistency checking after this stage, if
893-
* checking is enabled (--check is passed to cilly) *)
894-
}
895-
896869
let locUnknown = { line = -1;
897870
file = "";
898871
byte = -1;}

src/cil.mli

-26
Original file line numberDiff line numberDiff line change
@@ -1127,32 +1127,6 @@ val lowerConstants: bool ref
11271127
val insertImplicitCasts: bool ref
11281128
(** Do insert implicit casts (default true) *)
11291129

1130-
(** To be able to add/remove features easily, each feature should be package
1131-
* as an interface with the following interface. These features should be *)
1132-
type featureDescr = {
1133-
fd_enabled: bool ref;
1134-
(** The enable flag. Set to default value *)
1135-
1136-
fd_name: string;
1137-
(** This is used to construct an option "--doxxx" and "--dontxxx" that
1138-
* enable and disable the feature *)
1139-
1140-
fd_description: string;
1141-
(** A longer name that can be used to document the new options *)
1142-
1143-
fd_extraopt: (string * Arg.spec * string) list;
1144-
(** Additional command line options. The description strings should
1145-
usually start with a space for Arg.align to print the --help nicely. *)
1146-
1147-
fd_doit: (file -> unit);
1148-
(** This performs the transformation *)
1149-
1150-
fd_post_check: bool;
1151-
(** Whether to perform a CIL consistency checking after this stage, if
1152-
* checking is enabled (--check is passed to cilly). Set this to true if
1153-
* your feature makes any changes for the program. *)
1154-
}
1155-
11561130
(** Comparison function for locations.
11571131
** Compares first by filename, then line, then byte *)
11581132
val compareLoc: location -> location -> int

src/cilutil.ml

-21
Original file line numberDiff line numberDiff line change
@@ -40,20 +40,6 @@ let doCheck= ref false (* Whether to check CIL *)
4040
let strictChecking= ref false (* If doCheck is true and warnings are found,
4141
* treat them as errors. *)
4242

43-
let logCalls = ref false (* Whether to produce a log with all the function
44-
* calls made *)
45-
let logWrites = ref false (* Whether to produce a log with all the mem
46-
* writes made *)
47-
let doPartial = ref false (* Whether to do partial evaluation and constant
48-
* folding *)
49-
let doSimpleMem = ref false (* reduce complex memory expressions so that
50-
* they contain at most one lval *)
51-
let doOneRet = ref false (* make a functions have at most one 'return' *)
52-
let doStackGuard = ref false (* instrument function calls and returns to
53-
maintain a separate stack for return addresses *)
54-
let doHeapify = ref false (* move stack-allocated arrays to the heap *)
55-
let makeCFG = ref false (* turn the input CIL file into something more like
56-
* a CFG *)
5743
let printStats = ref false
5844

5945
(* when 'sliceGlobal' is set, then when 'rmtmps' runs, only globals*)
@@ -63,10 +49,3 @@ let sliceGlobal = ref false
6349

6450

6551
let printStages = ref false
66-
67-
68-
let doCxxPP = ref false
69-
70-
let libDir = ref ""
71-
72-
let dumpFCG = ref false

src/ext/blockinggraph/blockinggraph.ml

+3-2
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@
3535
*
3636
*)
3737
open Cil
38+
open Feature
3839
open Pretty
3940
module E = Errormsg
4041

@@ -750,9 +751,9 @@ let instrumentProgram (f: file) : unit =
750751

751752

752753

753-
let feature : featureDescr =
754+
let feature =
754755
{ fd_name = "FCG";
755-
fd_enabled = ref false;
756+
fd_enabled = false;
756757
fd_description = "computing and printing a static call graph";
757758
fd_extraopt = [];
758759
fd_doit =

src/ext/blockinggraph/blockinggraph.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -37,4 +37,4 @@
3737

3838
(* This module finds and analyzes yield points. *)
3939

40-
val feature: Cil.featureDescr
40+
val feature: Feature.t

src/ext/callgraph/callgraph.ml

+3-4
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
(* see copyright notice at end of this file *)
55

66
open Cil
7+
open Feature
78
open Trace
89
open Printf
910
module P = Pretty
@@ -201,11 +202,9 @@ let printGraph (out:out_channel) (g:callgraph) : unit = begin
201202
g
202203
end
203204

204-
let doCallGraph = ref false
205-
206-
let feature : featureDescr =
205+
let feature =
207206
{ fd_name = "callgraph";
208-
fd_enabled = doCallGraph;
207+
fd_enabled = false;
209208
fd_description = "generation of a static call graph";
210209
fd_extraopt = [];
211210
fd_doit =

src/ext/callgraph/callgraph.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ val computeGraph : Cil.file -> callgraph
8888
val printGraph : out_channel -> callgraph -> unit
8989

9090

91-
val feature: Cil.featureDescr
91+
val feature: Feature.t
9292
(*
9393
*
9494
* Copyright (c) 2001-2002 by

src/ext/canonicalize/canonicalize.ml

+3-2
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@
6363
************************************************************************)
6464

6565
open Cil
66+
open Feature
6667
module E = Errormsg
6768
module H = Hashtbl
6869

@@ -282,9 +283,9 @@ let canonicalize (f:file) =
282283

283284

284285

285-
let feature : featureDescr =
286+
let feature =
286287
{ fd_name = "canonicalize";
287-
fd_enabled = ref false;
288+
fd_enabled = false;
288289
fd_description = "fixing some C-isms so that the result is C++ compliant.";
289290
fd_extraopt = [];
290291
fd_doit = canonicalize;

src/ext/canonicalize/canonicalize.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,4 +45,4 @@
4545
*
4646
************************************************************************)
4747

48-
val feature: Cil.featureDescr
48+
val feature: Feature.t

src/ext/ccl/ccl.ml

+3-2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@
3434
*
3535
*)
3636
open Cil
37+
open Feature
3738
open Pretty
3839
module E = Errormsg
3940

@@ -1930,9 +1931,9 @@ let analyzeFile (f : file) : unit =
19301931
if !E.hadErrors then
19311932
E.s (E.error "Verification failed")
19321933

1933-
let feature : featureDescr =
1934+
let feature =
19341935
{ fd_name = "CCL";
1935-
fd_enabled = ref false;
1936+
fd_enabled = false;
19361937
fd_description = "CCured Lite";
19371938
fd_extraopt = [
19381939
"--cclverbose", Arg.Set verbose, "Enable verbose output for CCL";

src/ext/ccl/ccl.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -37,4 +37,4 @@
3737
val verifiedExps: Cil.exp list ref
3838
val verifiedArgs: Cil.exp list ref
3939

40-
val feature: Cil.featureDescr
40+
val feature: Feature.t

src/ext/cqualann/cqualann.ml

+3-4
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@
2929
*)
3030

3131
open Cil
32+
open Feature
3233
open Pretty
3334
module E = Errormsg
3435
module H = Hashtbl
@@ -498,15 +499,13 @@ let entry_point (f : file) =
498499

499500

500501

501-
let enableAnn = ref false
502-
503502
(***********************
504503
* The Cil.featureDesc that tells the CIL front-end how to call this module.
505504
* This is the only value that needs to be exported from smalloc.ml. **)
506505

507-
let feature : featureDescr =
506+
let feature =
508507
{ fd_name = "CqualAnn";
509-
fd_enabled = enableAnn;
508+
fd_enabled = false;
510509
fd_description = "adding assembly annotations for Cqual qualifiers." ;
511510
fd_extraopt = [ "--doCollapseCallCast",
512511
Arg.Set Cabs2cil.doCollapseCallCast,

src/ext/dataslicing/dataslicing.ml

+3-2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@
3434
*
3535
*)
3636
open Cil
37+
open Feature
3738
open Pretty
3839
module E = Errormsg
3940

@@ -444,9 +445,9 @@ let sliceFile (f : file) : unit =
444445
f.globals <- List.rev !newGlobals;
445446
visitCilFile (new dropAttrsVisitor) f
446447

447-
let feature : featureDescr =
448+
let feature =
448449
{ fd_name = "DataSlicing";
449-
fd_enabled = ref false;
450+
fd_enabled = false;
450451
fd_description = "data slicing";
451452
fd_extraopt = [];
452453
fd_doit = sliceFile;

src/ext/dataslicing/dataslicing.mli

+1-1
Original file line numberDiff line numberDiff line change
@@ -38,4 +38,4 @@
3838
* and function types with region(i) annotations, and this transformation
3939
* will separate the fields into parallel data structures accordingly. *)
4040

41-
val feature: Cil.featureDescr
41+
val feature: Feature.t

src/ext/epicenter/epicenter.ml

+3-3
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66

77
open Callgraph
88
open Cil
9+
open Feature
910
open Trace
1011
open Pretty
1112
module H = Hashtbl
@@ -54,13 +55,12 @@ let sliceFile (f:file) (epicenter:string) (maxHops:int) : unit =
5455
Cilutil.sliceGlobal := true;
5556
Rmtmps.removeUnusedTemps ~isRoot:isRoot f
5657

57-
let doEpicenter = ref false
5858
let epicenterName = ref ""
5959
let epicenterHops = ref 0
6060

61-
let feature : featureDescr =
61+
let feature =
6262
{ fd_name = "epicenter";
63-
fd_enabled = doEpicenter;
63+
fd_enabled = false;
6464
fd_description = "remove all functions except those within some number" ^
6565
"\n\t\t\t\tof hops (in the call graph) from a given function";
6666
fd_extraopt =

src/ext/heapify/heapify.ml

+5-4
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@
4343
* and frees the structure on return.
4444
*)
4545
open Cil
46+
open Feature
4647

4748
(* utilities that should be in Cil.ml *)
4849
(* sfg: this function appears to never be called *)
@@ -223,17 +224,17 @@ void * stackguard_pop() {
223224
ignore (stackguard f push pop get_ra set_ra )
224225

225226

226-
let feature1 : featureDescr =
227+
let feature1 =
227228
{ fd_name = "stackGuard";
228-
fd_enabled = Cilutil.doStackGuard;
229+
fd_enabled = false;
229230
fd_description = "instrument function calls and returns to maintain a\n\t\t\t\tseparate stack for return addresses" ;
230231
fd_extraopt = [];
231232
fd_doit = (function (f: file) -> default_stackguard f);
232233
fd_post_check = true;
233234
}
234-
let feature2 : featureDescr =
235+
let feature2 =
235236
{ fd_name = "heapify";
236-
fd_enabled = Cilutil.doHeapify;
237+
fd_enabled = false;
237238
fd_description = "move stack-allocated arrays to the heap" ;
238239
fd_extraopt = [
239240
"--heapifyAll", Arg.Set heapifyNonArrays,

src/ext/inliner/inliner.ml

+4-4
Original file line numberDiff line numberDiff line change
@@ -49,12 +49,12 @@
4949

5050
open Pretty
5151
open Cil
52+
open Feature
5253
module E = Errormsg
5354
module H = Hashtbl
5455
module IH = Inthash
5556
module A = Alpha
5657

57-
let doInline = ref false
5858
let debug = true
5959

6060
exception Recursion (* Used to signal recursion *)
@@ -431,12 +431,12 @@ let doit (fl: file) =
431431

432432
doFile inlineWhat fl
433433

434-
let feature : featureDescr =
434+
let rec feature =
435435
{ fd_name = "inliner";
436-
fd_enabled = doInline;
436+
fd_enabled = false;
437437
fd_description = "inline function calls";
438438
fd_extraopt = [
439-
"--inline", Arg.String (fun s -> doInline := true;
439+
"--inline", Arg.String (fun s -> feature.fd_enabled <- true;
440440
toinline := s :: !toinline),
441441
"<func> inline this function";
442442
];

src/ext/liveness/liveness.ml

+2-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
*)
88

99
open Cil
10+
open Feature
1011
open Pretty
1112

1213
module DF = Dataflow
@@ -329,7 +330,7 @@ let do_live_feature (f:file) =
329330
let feature =
330331
{
331332
fd_name = "Liveness";
332-
fd_enabled = ref false;
333+
fd_enabled = false;
333334
fd_description = "Spit out live variables at a label";
334335
fd_extraopt = [
335336
"--live_label",

src/ext/llvm/llvm.ml

+3-2
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@
5454
- iBinop/MinusPP: will get an exception when computing elemsize
5555
*)
5656
open Cil
57+
open Feature
5758
open Pretty
5859
open List
5960
open Llvmutils
@@ -163,9 +164,9 @@ let generate (f:file) : doc =
163164
(globals#printGlobals ()) ++ body
164165

165166
(* CIL feature setup *)
166-
let feature : featureDescr =
167+
let feature =
167168
{ fd_name = "llvm";
168-
fd_enabled = ref false;
169+
fd_enabled = false;
169170
fd_description = "generate llvm code";
170171
fd_extraopt = [];
171172
fd_doit =

0 commit comments

Comments
 (0)