From 924130132a766149cc97745629fd52e08ec6b798 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 6 Sep 2023 12:02:35 +0200 Subject: [PATCH] Remove TODO comment and add a few other explaining comments --- src/analyses/memOutOfBounds.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 0e93adb295..1738970739 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -1,3 +1,5 @@ +(** An analysis for the detection of out-of-bounds memory accesses ([memOutOfBounds]).*) + open GoblintCil open Analyses open MessageCategory @@ -5,6 +7,12 @@ open MessageCategory module AS = AnalysisState module VDQ = ValueDomainQueries +(* + Note: + * This functionality is implemented as an analysis solely for the sake of maintaining + separation of concerns, as well as for having the ablility to conveniently turn it on or off + * It doesn't track any internal state +*) module Spec = struct include Analyses.IdentitySpec @@ -12,7 +20,6 @@ struct module D = Lattice.Unit module C = D - (* TODO: Check out later for benchmarking *) let context _ _ = () let name () = "memOutOfBounds"