文件名称:SPARTA:SPARTA是一个提供基于抽象解释构建高性能静态代码分析器的基本模块的库
文件大小:206KB
文件格式:ZIP
更新时间:2024-05-27 13:24:52
C++
斯帕塔 SPARTA是一个软件组件库,专门根据抽象解释理论构建高性能的静态分析仪。 抽象解释 是一种语义近似理论,为静态程序分析器的设计提供了基础框架。 遵循抽象解释方法构建的静态分析器在数学上是可靠的,即,保证它们计算的语义信息在考虑的所有可能执行上下文中都可以保存。 此外,这些分析仪能够推断出程序的复杂属性,可以对它们的表达方式进行微调以控制分析时间。 例如,通常使用基于抽象解释的静态分析器对航空软件中的飞行软件进行形式验证。 为什么选择SPARTA? 从头开始构建基于抽象解释的工业级静态分析工具是一项艰巨的任务,需要本领域专家的关注。 SPARTA的目的是通过提供一组具有简单API,高性能和易于组装的软件组件来大大简化抽象解释的工程流程,从而构建出生产质量的静态分析器。 通过封装抽象解释的复杂实现细节,SPARTA使工具开发人员可以专注于分析设计中的三个基本轴: 语义:要分析的
【文件预览】:
SPARTA-master
----run_all_tests.sh(698B)
----test()
--------PatriciaTreeMapTest.cpp(7KB)
--------HashedAbstractEnvironmentTest.cpp(6KB)
--------DisjointUnionAbstractDomainTest.cpp(2KB)
--------HashedSetAbstractDomainTest.cpp(5KB)
--------PatriciaTreeMapAbstractEnvironmentTest.cpp(9KB)
--------WeakPartialOrderingTest.cpp(42KB)
--------SparseSetAbstractDomainTest.cpp(5KB)
--------LiftedDomainTest.cpp(1KB)
--------PatriciaTreeOverUnderSetAbstractDomainTest.cpp(21KB)
--------S_ExpressionTest.cpp(8KB)
--------ReducedProductAbstractDomainTest.cpp(6KB)
--------WeakTopologicalOrderingTest.cpp(7KB)
--------AbstractDomainPropertyTest.h(6KB)
--------FiniteAbstractDomainTest.cpp(4KB)
--------InterproceduralAnalyzerTest.cpp(20KB)
--------MonotonicFixpointIteratorTest.cpp(28KB)
--------IntervalDomainTest.cpp(4KB)
--------PatriciaTreeSetAbstractDomainTest.cpp(7KB)
--------SpartaWorkQueueTest.cpp(2KB)
--------SetTest.cpp(8KB)
--------HashedAbstractPartitionTest.cpp(6KB)
--------DirectProductAbstractDomainTest.cpp(5KB)
--------PatriciaTreeMapAbstractPartitionTest.cpp(8KB)
--------SmallSortedSetAbstractDomainTest.cpp(7KB)
----get_boost.sh(395B)
----include()
--------S_Expression.h(24KB)
--------SparseSetAbstractDomain.h(7KB)
--------Arity.h(2KB)
--------SmallSortedSetAbstractDomain.h(5KB)
--------WeakTopologicalOrdering.h(12KB)
--------FixpointIterator.h(5KB)
--------PatriciaTreeSet.h(34KB)
--------PatriciaTreeMapAbstractPartition.h(6KB)
--------PatriciaTreeMapAbstractEnvironment.h(9KB)
--------PatriciaTreeMap.h(43KB)
--------Analyzer.h(10KB)
--------FiniteAbstractDomain.h(17KB)
--------Exceptions.h(1KB)
--------DisjointUnionAbstractDomain.h(10KB)
--------PatriciaTreeUtil.h(1KB)
--------PatriciaTreeSetAbstractDomain.h(4KB)
--------ReducedProductAbstractDomain.h(8KB)
--------IntervalDomain.h(7KB)
--------WeakPartialOrdering.h(21KB)
--------MonotonicFixpointIterator.h(27KB)
--------AbstractDomain.h(21KB)
--------PowersetAbstractDomain.h(6KB)
--------LiftedDomain.h(5KB)
--------SpartaWorkQueue.h(11KB)
--------ConstantAbstractDomain.h(4KB)
--------FlatSet.h(6KB)
--------PatriciaTreeOverUnderSetAbstractDomain.h(7KB)
--------HashedAbstractPartition.h(9KB)
--------DirectProductAbstractDomain.h(9KB)
--------HashedSetAbstractDomain.h(5KB)
--------HashedAbstractEnvironment.h(13KB)
----LICENSE(1KB)
----CONTRIBUTING.md(2KB)
----cmake_modules()
--------Commons.cmake(4KB)
--------gtest.cmake.in(539B)
----SPARTA.png(74KB)
----.clang-format(1KB)
----.gitignore(86B)
----CMakeLists.txt(2KB)
----.circleci()
--------config.yml(1KB)
----CODE_OF_CONDUCT.md(3KB)
----README.md(5KB)