Skip to content

Commit 5577a68

Browse files
committed
Use GoblintCil.var where possible
1 parent 2dd48c1 commit 5577a68

File tree

10 files changed

+22
-14
lines changed

10 files changed

+22
-14
lines changed

.semgrep/cil.yml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,3 +15,11 @@ rules:
1515
message: use Cilfacade instead
1616
languages: [ocaml]
1717
severity: WARNING
18+
19+
- id: cil-var
20+
pattern: (Var $X, NoOffset)
21+
# Autofix is broken: https://github.com/semgrep/semgrep/issues/11278
22+
# fix: GoblintCil.var $X
23+
message: use GoblintCil.var instead
24+
languages: [ocaml]
25+
severity: WARNING

src/analyses/apron/relationAnalysis.apron.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -506,7 +506,7 @@ struct
506506
foldGlobals !Cilfacade.current_file (fun acc global ->
507507
match global with
508508
| GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
509-
mkAddrOf (Var vi, NoOffset) :: acc
509+
mkAddrOf (Cil.var vi) :: acc
510510
(* TODO: what about GVarDecl? *)
511511
| _ -> acc
512512
) deep_addrs

src/analyses/base.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2058,7 +2058,7 @@ struct
20582058
if not (Cil.isArrayType v.vtype) then
20592059
man.local
20602060
else
2061-
let lval = eval_lv ~man man.local (Var v, NoOffset) in
2061+
let lval = eval_lv ~man man.local (Cil.var v) in
20622062
let current_value = eval_rv ~man man.local (Lval (Var v, NoOffset)) in
20632063
let new_value = VD.update_array_lengths (eval_rv ~man man.local) current_value v.vtype in
20642064
set ~man man.local lval v.vtype new_value
@@ -2233,7 +2233,7 @@ struct
22332233
foldGlobals !Cilfacade.current_file (fun acc global ->
22342234
match global with
22352235
| GVar (vi, _, _) when not (is_static vi) ->
2236-
mkAddrOf (Var vi, NoOffset) :: acc
2236+
mkAddrOf (Cil.var vi) :: acc
22372237
(* TODO: what about GVarDecl? *)
22382238
| _ -> acc
22392239
) deep_addrs

src/analyses/baseInvariant.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ struct
107107
if is_some_bot v then contra st
108108
else (
109109
if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)" CilType.Varinfo.pretty var VD.pretty old_val VD.pretty v pretty c VD.pretty c';
110-
let r = set' (Var var,NoOffset) v st in
110+
let r = set' (Cil.var var) v st in
111111
if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r;
112112
r
113113
)

src/analyses/c2poAnalysis.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -247,7 +247,7 @@ struct
247247
let state_with_ghosts = meet_conjs_opt equalities_to_add d.data in
248248
let state_with_ghosts = data_to_t state_with_ghosts in
249249
if M.tracing then begin
250-
let dummy_lval = Var (Var.dummy_varinfo (TVoid [])), NoOffset in
250+
let dummy_lval = Cil.var (Var.dummy_varinfo (TVoid [])) in
251251
let lval = BatOption.default dummy_lval var_opt in
252252
M.trace "c2po-function" "enter1: var_opt: %a; state: %s; state_with_ghosts: %s\n" d_lval lval (D.show ctx.local) (C2PODomain.show state_with_ghosts);
253253
end;
@@ -295,7 +295,7 @@ struct
295295
let cc = remove_out_of_scope_vars d.data f in
296296
let d = data_to_t cc in
297297
if M.tracing then begin
298-
let dummy_lval = Var (Var.dummy_varinfo (TVoid[])), NoOffset in
298+
let dummy_lval = Cil.var (Var.dummy_varinfo (TVoid[])) in
299299
let lval = BatOption.default dummy_lval lval_opt in
300300
M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" d_lval lval (D.show ctx.local) (D.show f_d) (C2PODomain.show d)
301301
end;

src/analyses/startStateAnalysis.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ struct
5555
let lval = Lval (Var var, NoOffset) in
5656
let value = get_value (ask_of_man ctx) lval in
5757
let duplicated_var = to_varinfo (DuplicVar var) in
58-
if M.tracing then M.trace "startState" "added value: var: %a; value: %a" d_lval (Var duplicated_var, NoOffset) AD.pretty value;
58+
if M.tracing then M.trace "startState" "added value: var: %a; value: %a" CilType.Varinfo.pretty duplicated_var AD.pretty value;
5959
D.add duplicated_var value st
6060
in
6161
(* assign function parameters *)

src/analyses/taintPartialContexts.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ struct
6868
foldGlobals !Cilfacade.current_file (fun acc global ->
6969
match global with
7070
| GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
71-
mkAddrOf (Var vi, NoOffset) :: acc
71+
mkAddrOf (Cil.var vi) :: acc
7272
(* TODO: what about GVarDecl? (see "base.ml -> special_unknown_invalidate")*)
7373
| _ -> acc
7474
) deep_addrs

src/analyses/varEq.ml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -411,7 +411,7 @@ struct
411411

412412
(* Just remove things that go out of scope. *)
413413
let return man exp fundec =
414-
let rm acc v = remove (Analyses.ask_of_man man) (Var v, NoOffset) acc in
414+
let rm acc v = remove (Analyses.ask_of_man man) (Cil.var v) acc in
415415
List.fold_left rm man.local (fundec.sformals@fundec.slocals)
416416

417417
(* removes all equalities with lval and then tries to make a new one: lval=rval *)
@@ -427,9 +427,9 @@ struct
427427
| x::xs, y::ys -> fold_left2 f (f r x y) xs ys
428428
| _ -> r
429429
in
430-
let assign_one_param st lv exp =
431-
let rm = remove (Analyses.ask_of_man man) (Var lv, NoOffset) st in
432-
add_eq (Analyses.ask_of_man man) (Var lv, NoOffset) exp rm
430+
let assign_one_param st v exp =
431+
let rm = remove (Analyses.ask_of_man man) (Cil.var v) st in
432+
add_eq (Analyses.ask_of_man man) (Cil.var v) exp rm
433433
in
434434
let nst =
435435
try fold_left2 assign_one_param man.local f.sformals args

src/cdomains/unionFind.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -320,7 +320,7 @@ module T = struct
320320
function
321321
| Addr v ->
322322
let varinfo = Var.to_varinfo v in
323-
let lval = (Var varinfo, NoOffset) in
323+
let lval = Cil.var varinfo in
324324
AddrOf lval
325325
| Aux (_, exp)
326326
| (Deref (_, _, exp)) -> exp

src/util/returnUtil.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,6 @@ module AD = ValueDomain.AD
66
let return_varstore = ref dummyFunDec.svar
77
let return_varinfo () = !return_varstore
88
let return_var () = AD.of_var (return_varinfo ())
9-
let return_lval (): lval = (Var (return_varinfo ()), NoOffset)
9+
let return_lval (): lval = Cil.var (return_varinfo ())
1010

1111
let longjmp_return = ref dummyFunDec.svar

0 commit comments

Comments
 (0)