Class PosIntervalDomain<Value>
Type Parameters
- Value extends PosIntervalLift = PosIntervalLift
Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
Hierarchy (View Summary)
- IntervalDomain<Value>
- PosIntervalDomain
Hierarchy-Diagram
Constructors
constructor
- new PosIntervalDomain<Value extends PosIntervalLift = PosIntervalLift>(
value: Value,
): PosIntervalDomain<Value>Type Parameters
- Value extends PosIntervalLift = PosIntervalLift
Parameters
- value: Value
Returns PosIntervalDomain<Value>
Methods
Staticabstract
Parameters
- concrete: typeof Top | ReadonlySet<number>
Returns PosIntervalDomain
Staticbottom
Returns PosIntervalDomain<typeof Bottom>
Statictop
Returns PosIntervalDomain<PosIntervalTop>
abstract
Maps a set of possible concrete values into an abstract value as abstraction function of the abstract domain (should additionally be provided as static function).
Parameters
- concrete: typeof Top | ReadonlySet<number>
Returns PosIntervalDomain
add
Adds another abstract value to the current abstract value by adding the two lower and upper bounds, respectively.
Parameters
- other: IntervalDomain
Returns IntervalDomain
bottom
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).
Returns PosIntervalDomain<typeof Bottom>
concretize
Maps the current abstract value into a set of possible concrete values as concretization function of the abstract domain. The result should be
Topif the number of concrete values would reach thelimitor the resulting set would have infinite many elements.Parameters
- limit: number = DEFAULT_INFERENCE_LIMIT
Returns typeof Top | ReadonlySet<number>
equals
Checks whether the current abstract value equals to another abstract value.
Parameters
- other: IntervalDomain
Returns boolean
extend
Extends the lower bound of the current abstract value down to 0.
Returns PosIntervalDomain
extend
Extends the upper bound of the current abstract value up to +∞.
Returns IntervalDomain
is
Checks whether the current abstract value is the Bottom element of the complete lattice.
Returns this is IntervalDomain<typeof Bottom>
is
Checks whether the current abstract value is the Top element of the complete lattice.
Returns this is PosIntervalDomain<PosIntervalTop>
is
Checks whether the current abstract value is an actual value of the complete lattice (this may include the Top or Bottom element if they are also values and no separate symbols, for example).
Returns this is IntervalDomain<IntervalValue>
join
Joins the current abstract value with other abstract values by creating the least upper bound (LUB) in the lattice.
Parameters
- ...values: IntervalDomain<IntervalLift>[]
Returns IntervalDomain
leq
Checks whether the current abstract value is less than or equal to another abstract value with respect to the partial order of the lattice.
Parameters
- other: IntervalDomain
Returns boolean
max
Creates the maximum between the current abstract value and another abstract value by creating the maximum of the two lower and upper bounds, respectively.
Parameters
- other: IntervalDomain
Returns IntervalDomain
meet
Meets the current abstract value with other abstract values by creating the greatest lower bound (GLB) in the lattice.
Parameters
- ...values: IntervalDomain<IntervalLift>[]
Returns IntervalDomain
min
Creates the minimum between the current abstract value and another abstract value by creating the minimum of the two lower and upper bounds, respectively.
Parameters
- other: IntervalDomain
Returns IntervalDomain
narrow
Narrows the current abstract value with another abstract value as a sound over-approximation of the meet (greatest lower bound) to refine the value after widening.
Parameters
- other: PosIntervalDomain
Returns PosIntervalDomain
subtract
Subtracts another abstract value from the current abstract value by subtracting the two lower and upper bounds from each other, respectively.
Parameters
- other: PosIntervalDomain
Returns PosIntervalDomain
top
Gets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).
Returns PosIntervalDomain<PosIntervalTop>
to
Converts the lattice into a human-readable string.
Returns string
widen
Widens the current abstract value with another abstract value as a sound over-approximation of the join (least upper bound) for fixpoint iteration acceleration.
Parameters
- other: PosIntervalDomain
Returns PosIntervalDomain
Settings
- src
- util
- abstract-interpretation
- data-frame
- mappers
- absint-info.ts
- absint-visitor.ts
- dataframe-domain.ts
- domain.ts
- <internal>
- addInterval
- ColNamesBottom
- ColNamesDomain
- ColNamesTop
- DataFrameBottom
- DataFrameDomain
- DataFrameStateDomain
- DataFrameTop
- equalColNames
- equalDataFrameDomain
- equalDataFrameState
- equalInterval
- extendIntervalToInfinity
- extendIntervalToZero
- IntervalBottom
- IntervalDomain
- IntervalTop
- joinColNames
- joinDataFrames
- joinDataFrameStates
- joinInterval
- leqColNames
- leqInterval
- maxInterval
- meetColNames
- meetDataFrames
- meetDataFrameStates
- meetInterval
- minInterval
- satisfiesColsNames
- satisfiesInterval
- satisfiesLeqInterval
- subtractColNames
- subtractInterval
- wideningColNames
- wideningDataFrames
- wideningDataFrameStates
- wideningInterval
- resolve-args.ts
- semantics.ts
- shape-inference.ts
- domains
- normalized-ast-fold.ts
- data-frame
- benchmark
- stats
- summarizer
- first-phase
- second-phase
- data.ts
- summarizer.ts
- slicer.ts
- stopwatch.ts
- cli
- common
- repl
- commands
- server
- core.ts
- execute.ts
- print-version.ts
- prompt.ts
- script-core
- benchmark-app.ts
- benchmark-helper-app.ts
- export-quads-app.ts
- flowr.ts
- flowr-main-options.ts
- run-script.ts
- slicer-app.ts
- statistics-app.ts
- statistics-helper-app.ts
- summarizer-app.ts
- control-flow
- basic-cfg-guided-visitor.ts
- cfg-dead-code.ts
- cfg-properties.ts
- cfg-simplification.ts
- cfg-to-basic-blocks.ts
- control-flow-graph.ts
- <internal>
- CfgBasicBlockVertex
- CfgControlDependencyEdge
- CfgEdge
- CfgEdgeType
- CfgEndMarkerVertex
- CfgExpressionVertex
- CfgSimpleVertex
- CfgStatementVertex
- CfgVertexType
- CfgWithRoot
- ControlFlowGraph
- ControlFlowInformation
- edgeTypeToString
- emptyControlFlowInformation
- equalVertex
- getVertexRootId
- isMarkerVertex
- ReadOnlyControlFlowGraph
- dfg-cfg-guided-visitor.ts
- diff-cfg.ts
- extract-cfg.ts
- happens-before.ts
- semantic-cfg-guided-visitor.ts
- simple-visitor.ts
- syntax-cfg-guided-visitor.ts
- useless-loop.ts
- core
- steps
- all
- core
- static-slicing
- pipeline
- create-pipeline.ts
- default-pipelines.ts
- createDataflowPipeline
- createNormalizePipeline
- createParsePipeline
- createSlicePipeline
- DEFAULT_DATAFLOW_PIPELINE
- DEFAULT_NORMALIZE_PIPELINE
- DEFAULT_PARSE_PIPELINE
- DEFAULT_SLICE_AND_RECONSTRUCT_PIPELINE
- DEFAULT_SLICE_WITHOUT_RECONSTRUCT_PIPELINE
- DEFAULT_SLICING_PIPELINE
- TREE_SITTER_DATAFLOW_PIPELINE
- TREE_SITTER_NORMALIZE_PIPELINE
- TREE_SITTER_PARSE_PIPELINE
- TREE_SITTER_SLICE_AND_RECONSTRUCT_PIPELINE
- TREE_SITTER_SLICE_WITHOUT_RECONSTRUCT_PIPELINE
- TREE_SITTER_SLICING_PIPELINE
- invalid-pipeline-error.ts
- pipeline.ts
- pipeline-step.ts
- all
- pipeline-executor.ts
- dataflow
- environments
- append.ts
- built-in.ts
- BuiltIn
- BuiltInEvalHandler
- BuiltInEvalHandlerMapper
- builtInId
- BuiltInIdentifierConstant
- BuiltInIdentifierDefinition
- BuiltInIdentifierProcessor
- BuiltInIdentifierProcessorWithConfig
- BuiltInMappingName
- BuiltInMemory
- BuiltInProcessorMapper
- BuiltIns
- ConfigOfBuiltInMappingName
- DefaultBuiltInProcessorConfiguration
- isBuiltIn
- UseAsProcessors
- built-in-config.ts
- clone.ts
- default-builtin-config.ts
- define.ts
- diff.ts
- environment.ts
- identifier.ts
- overwrite.ts
- remove.ts
- resolve-by-name.ts
- scoping.ts
- eval
- resolve
- values
- intervals
- logical
- scalar
- sets
- string
- vectors
- general.ts
- r-value.ts
- graph
- dataflowgraph-builder.ts
- diff-dataflow-graph.ts
- edge.ts
- graph.ts
- invert-dfg.ts
- quads.ts
- resolve-graph.ts
- unknown-replacement.ts
- unknown-side-effect.ts
- vertex.ts
- <internal>
- ContainerIndex
- ContainerIndices
- ContainerIndicesCollection
- ContainerLeafIndex
- ContainerParentIndex
- DataflowGraphVertexArgument
- DataflowGraphVertexAstLink
- DataflowGraphVertexFunctionCall
- DataflowGraphVertexFunctionDefinition
- DataflowGraphVertexInfo
- DataflowGraphVertexUse
- DataflowGraphVertexValue
- DataflowGraphVertexVariableDefinition
- DataflowGraphVertices
- FunctionOriginInformation
- IndexIdentifier
- isAccessed
- isFunctionCallVertex
- isFunctionDefinitionVertex
- isNamedArgumentId
- isParentContainerIndex
- isSameIndex
- isUseVertex
- isValueVertex
- isVariableDefinitionVertex
- NamedArgumentId
- UnnamedArgumentId
- ValidVertexTypeReverse
- ValidVertexTypes
- VertexType
- internal
- process
- functions
- call
- argument
- built-in
- built-in-access.ts
- built-in-apply.ts
- built-in-assignment.ts
- built-in-eval.ts
- built-in-expression-list.ts
- built-in-for-loop.ts
- built-in-function-definition.ts
- built-in-get.ts
- built-in-if-then-else.ts
- built-in-library.ts
- built-in-list.ts
- built-in-pipe.ts
- built-in-quote.ts
- built-in-repeat-loop.ts
- built-in-replacement.ts
- built-in-rm.ts
- built-in-source.ts
- built-in-special-bin-op.ts
- built-in-vector.ts
- built-in-while-loop.ts
- common.ts
- default-call-handling.ts
- known-call-handling.ts
- named-call-handling.ts
- unnamed-call-handling.ts
- process-argument.ts
- process-parameter.ts
- call
- process-named-call.ts
- process-symbol.ts
- process-uninteresting-leaf.ts
- process-value.ts
- functions
- linker.ts
- process
- origin
- cluster.ts
- extractor.ts
- info.ts
- logger.ts
- processor.ts
- environments
- documentation
- data
- doc-util
- doc-auto-gen.ts
- doc-benchmarks.ts
- doc-cfg.ts
- doc-cli-option.ts
- doc-code.ts
- doc-dfg.ts
- doc-docker.ts
- doc-env.ts
- doc-escape.ts
- doc-files.ts
- doc-functions.ts
- doc-general.ts
- doc-issue.ts
- doc-normalized-ast.ts
- doc-print.ts
- doc-query.ts
- doc-repl.ts
- doc-search.ts
- doc-server-message.ts
- doc-structure.ts
- doc-types.ts
- <internal>
- dropGenericsFromTypeName
- followTypeReference
- getDocumentationForType
- getStartLineOfTypeScriptNode
- getTextualCommentsFromTypeScript
- getType
- getTypePathForTypeScript
- getTypePathLink
- GetTypesAsMermaidOption
- getTypeScriptSourceFiles
- getTypesFromFolder
- implSnippet
- mermaidHide
- printCodeOfElement
- printHierarchy
- PrintHierarchyArguments
- removeCommentSymbolsFromTypeScriptComment
- shortLink
- shortLinkFile
- TypeElementInSource
- TypeReport
- print-capabilities-markdown.ts
- print-cfg-wiki.ts
- print-core-wiki.ts
- print-dataflow-graph-wiki.ts
- print-engines-wiki.ts
- print-faq-wiki.ts
- print-interface-wiki.ts
- print-linter-issue.ts
- print-linter-wiki.ts
- print-linting-and-testing-wiki.ts
- print-normalized-ast-wiki.ts
- print-onboarding-wiki.ts
- print-query-wiki.ts
- print-readme.ts
- print-search-wiki.ts
- linter
- queries
- catalog
- call-context-query
- cluster-query
- config-query
- control-flow-query
- dataflow-lens-query
- dataflow-query
- dependencies-query
- df-shape-query
- happens-before-query
- id-map-query
- lineage-query
- linter-query
- location-map-query
- normalized-ast-query
- origin-query
- project-query
- resolve-value-query
- search-query
- static-slice-query
- virtual-query
- base-query-format.ts
- query.ts
- AnyQuerySchema
- CompoundQuerySchema
- executeQueries
- executeQueriesOfSameType
- Queries
- QueriesSchema
- Query
- QueryArgumentsWithType
- QueryExecutor
- QueryResult
- QueryResults
- QueryResultsWithoutMeta
- SupportedQueries
- SupportedQueriesSchema
- SupportedQuery
- SupportedQueryTypes
- SupportedSynchronousQueryTypes
- SynchronousQuery
- VirtualQuerySchema
- query-print.ts
- two-layer-collector.ts
- catalog
- r-bridge
- data
- lang-4.x
- ast
- model
- nodes
- processing
- collect.ts
- model.ts
- operators.ts
- type.ts
- versions.ts
- parser
- json
- main
- internal
- control
- expression
- functions
- loops
- operators
- other
- structure
- values
- normalize-access.ts
- normalize-meta.ts
- normalizer-data.ts
- internal
- model
- tree-sitter
- convert-values.ts
- ast
- init.ts
- parser.ts
- retriever.ts
- shell.ts
- shell-executor.ts
- reconstruct
- search
- search-executor
- search-enrichers.ts
- CallTargetsContent
- CfgInformationArguments
- CfgInformationElementContent
- CfgInformationSearchContent
- enrichElement
- Enrichment
- enrichmentContent
- EnrichmentData
- EnrichmentElementArguments
- EnrichmentElementContent
- Enrichments
- EnrichmentSearchArguments
- EnrichmentSearchContent
- LastCallContent
- QueryDataElementContent
- QueryDataSearchContent
- search-generators.ts
- search-mappers.ts
- search-transformer.ts
- search-enrichers.ts
- search-optimizer
- flowr-search.ts
- flowr-search-builder.ts
- flowr-search-executor.ts
- flowr-search-filters.ts
- flowr-search-printer.ts
- flowr-search-traverse.ts
- search-executor
- slicing
- criterion
- static
- statistics
- features
- supported
- assignments
- comments
- control-flow
- data-access
- defined-functions
- expression-list
- loops
- used-functions
- used-packages
- values
- variables
- common-syntax-probability.ts
- feature.ts
- post-processing.ts
- supported
- output
- summarizer
- first-phase
- post-process
- second-phase
- auto-detect.ts
- summarizer.ts
- meta-statistics.ts
- statistics.ts
- features
- config.ts
- test
- functionality
- _helper
- controlflow
- dataflow
- ast-builder.ts
- label.ts
- linter.ts
- log.ts
- net.ts
- network.ts
- pointer-analysis.ts
- provider.ts
- query.ts
- search.ts
- shell.ts
- <internal>
- assertAst
- assertContainerIndicesDefinition
- assertDataflow
- assertDecoratedAst
- assertOutput
- assertReconstructed
- assertSliced
- assertSlicedF
- defaultTestConfiguration
- retrieveNormalizedAst
- sameForSteps
- skipTestBecauseConfigNotMet
- TestCaseFailType
- TestConfiguration
- TestConfigurationWithOutput
- testWithShell
- withShell
- withTreeSitter
- _helper
- functionality
The positive interval abstract domain as positive intervals with possibly zero lower bounds and infinite upper bounds representing possible numeric values. The Bottom element is defined as Bottom symbol and the Top element is defined as the interval [0, +∞].