llvm/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
//
//  Ranged constraint manager, built on SimpleConstraintManager.
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_RANGEDCONSTRAINTMANAGER_H
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_RANGEDCONSTRAINTMANAGER_H

#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
#include "llvm/ADT/APSInt.h"
#include "llvm/Support/Allocator.h"

namespace clang {

namespace ento {

/// A Range represents the closed range [from, to].  The caller must
/// guarantee that from <= to.  Note that Range is immutable, so as not
/// to subvert RangeSet's immutability.
class Range { … };

/// @class RangeSet is a persistent set of non-overlapping ranges.
///
/// New RangeSet objects can be ONLY produced by RangeSet::Factory object, which
/// also supports the most common operations performed on range sets.
///
/// Empty set corresponds to an overly constrained symbol meaning that there
/// are no possible values for that symbol.
class RangeSet { … };

ConstraintMap;
ConstraintMap getConstraintMap(ProgramStateRef State);

class RangedConstraintManager : public SimpleConstraintManager { … };

/// Try to simplify a given symbolic expression based on the constraints in
/// State. This is needed because the Environment bindings are not getting
/// updated when a new constraint is added to the State. If the symbol is
/// simplified to a non-symbol (e.g. to a constant) then the original symbol
/// is returned. We use this function in the family of assumeSymNE/EQ/LT/../GE
/// functions where we can work only with symbols. Use the other function
/// (simplifyToSVal) if you are interested in a simplification that may yield
/// a concrete constant value.
SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);

/// Try to simplify a given symbolic expression's associated `SVal` based on the
/// constraints in State. This is very similar to `simplify`, but this function
/// always returns the simplified SVal. The simplified SVal might be a single
/// constant (i.e. `ConcreteInt`).
SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);

} // namespace ento
} // namespace clang

REGISTER_FACTORY_WITH_PROGRAMSTATE(…)

#endif