diff --git a/.semgrep/let.yml b/.semgrep/let.yml new file mode 100644 index 0000000000..f49e97d7e9 --- /dev/null +++ b/.semgrep/let.yml @@ -0,0 +1,6 @@ +rules: + - id: let-unit-in + pattern: let () = $E in ... + message: use ; instead (and, if needed, add surrounding parentheses to preserve precedence) + languages: [ocaml] + severity: WARNING diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index f4d72c3d71..5c449e63cf 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -36,7 +36,7 @@ let () = Printexc.register_printer (function | Apron.Manager.Error e -> - let () = Apron.Manager.print_exclog Format.str_formatter e in - Some(Printf.sprintf "Apron.Manager.Error\n %s" (Format.flush_str_formatter ())) + Apron.Manager.print_exclog Format.str_formatter e; + Some (Printf.sprintf "Apron.Manager.Error\n %s" (Format.flush_str_formatter ())) | _ -> None (* for other exceptions *) ) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index ff3946d047..72daac3a51 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -269,7 +269,7 @@ struct | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () end in let e_size = get_size_of_ptr_target man e in - let () = begin match e_size with + begin match e_size with | `Top -> (set_mem_safety_flag InvalidDeref; M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e) @@ -297,7 +297,7 @@ struct (set_mem_safety_flag InvalidDeref; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs) end - end in + end; begin match e with | Lval (Var v, _) as lval_exp -> check_no_binop_deref man lval_exp | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI -> diff --git a/src/solver/sLRterm.ml b/src/solver/sLRterm.ml index 947c73e4e1..7cde3e10ae 100644 --- a/src/solver/sLRterm.ml +++ b/src/solver/sLRterm.ml @@ -49,13 +49,13 @@ module SLR3term = let count = ref 0 in let count_side = ref (max_int - 1) in - let () = print_solver_stats := fun () -> + print_solver_stats := (fun () -> Logs.info "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side); let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *) HM.iter (fun k _ -> Hashtbl.modify_def 1 (S.Var.var_id k) ((+)1) histo) rho; let vid,n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in Logs.info "max #contexts: %d for var_id %s" n vid - in + ); let init ?(side=false) x = if not (HM.mem rho x) then begin diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 69a5d8179d..71667eff9b 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -287,11 +287,11 @@ module Base = include WPS (EqS) (HM) (VS) end in - let () = print_solver_stats := fun () -> + print_solver_stats := (fun () -> print_data data; Logs.info "|called|=%d" (HM.length called); print_context_stats rho - in + ); if GobConfig.get_bool "incremental.load" then ( print_data_verbose data "Loaded data for incremental analysis"; diff --git a/src/solver/td_simplified.ml b/src/solver/td_simplified.ml index 8844319e02..d2e8c93241 100644 --- a/src/solver/td_simplified.ml +++ b/src/solver/td_simplified.ml @@ -24,14 +24,14 @@ module Base : GenericEqSolver = let wpoint = HM.create 10 in let stable = HM.create 10 in - let () = print_solver_stats := fun () -> + print_solver_stats := (fun () -> Logs.debug "|rho|=%d" (HM.length rho); Logs.debug "|stable|=%d" (HM.length stable); Logs.debug "|infl|=%d" (HM.length infl); Logs.debug "|wpoint|=%d" (HM.length wpoint); Logs.info "|called|=%d" (HM.length called); print_context_stats rho - in + ); let add_infl y x = if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; @@ -122,7 +122,7 @@ module Base : GenericEqSolver = if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x; box old eqd) in - if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( + if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* old != wpd *) if tracing && not (S.Dom.is_bot old) then trace "update" "%a (wpx: %b): %a" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old); update_var_event x old wpd; @@ -132,7 +132,7 @@ module Base : GenericEqSolver = (iterate[@tailcall]) x ) else ( (* old == wpd *) - if not (HM.mem stable x) then ( + if not (HM.mem stable x) then ( (* value unchanged, but not stable, i.e. destabilized itself during rhs *) if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x; (iterate[@tailcall]) x @@ -172,7 +172,7 @@ module Base : GenericEqSolver = ); List.iter (fun x -> HM.replace called x (); if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x; - iterate x; + iterate x; HM.remove called x ) unstable_vs; solver (); diff --git a/src/solver/td_simplified_ref.ml b/src/solver/td_simplified_ref.ml index 76e8dde082..fb6f2182e9 100644 --- a/src/solver/td_simplified_ref.ml +++ b/src/solver/td_simplified_ref.ml @@ -28,9 +28,9 @@ module Base : GenericEqSolver = let solve st vs = let (data : var_data ref HM.t) = HM.create 10 in - let () = print_solver_stats := fun () -> + print_solver_stats := (fun () -> Logs.debug "|data|=%d" (HM.length data); - in + ); let add_infl y x = if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; @@ -46,12 +46,12 @@ module Base : GenericEqSolver = begin new_var_event x; if tracing then trace "init" "init %a" S.Var.pretty_trace x; - let data_x = ref { + let data_x = ref { infl = VS.empty; value = S.Dom.bot (); wpoint = false; stable = false; - called = false + called = false } in HM.replace data x data_x; data_x @@ -138,7 +138,7 @@ module Base : GenericEqSolver = if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x; box old eqd) in - if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( + if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* old != wpd *) if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old); update_var_event x old wpd; @@ -148,7 +148,7 @@ module Base : GenericEqSolver = (iterate[@tailcall]) x ) else ( (* old == wpd *) - if not (!x_ref.stable) then ( + if not (!x_ref.stable) then ( (* value unchanged, but not stable, i.e. destabilized itself during rhs *) if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x; (iterate[@tailcall]) x @@ -185,12 +185,12 @@ module Base : GenericEqSolver = Logs.newline (); flush_all (); ); - List.iter (fun x -> + List.iter (fun x -> let x_ref = HM.find data x in x_ref := { !x_ref with called = true }; if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x; - iterate x; - x_ref := { !x_ref with called = false } + iterate x; + x_ref := { !x_ref with called = false } ) unstable_vs; solver (); )