[all-commits] [llvm/llvm-project] d1f595: [clang][dataflow] Add `Environment::allows()`. (#7...

[martinboehme via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: d1f59544cf31488d84a2daff0020af2f8e366ed8
      https://github.com/llvm/llvm-project/commit/d1f59544cf31488d84a2daff0020af2f8e366ed8
  Author: martinboehme <mboehme at google.com>
  Date:   2023-10-25 (Wed, 25 Oct 2023)

  Changed paths:
    M clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
    M clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
    M clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
    M clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
    M clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp

  Log Message:
  -----------
  [clang][dataflow] Add `Environment::allows()`. (#70046)

This allows querying whether, given the flow condition, a certain
formula still
has a solution (though it is not necessarily implied by the flow
condition, as
`flowConditionImplies()` would check).

This can be checked today, but only with a double negation, i.e. to
check
whether, given the flow condition, a formula F has a solution, you can
check
`!Env.flowConditionImplies(Arena.makeNot(F))`. The double negation makes
this
hard to reason about, and it would be nicer to have a way of directly
checking
this.

For consistency, this patch also renames `flowConditionImplies()` to
`proves()`;
the old name is kept around for compatibility but deprecated.