// -*- C++ -*- (c) 2016 Henrich Lauko #pragma once DIVINE_RELAX_WARNINGS #include DIVINE_UNRELAX_WARNINGS #include #include #include #include #include #include #include #include #include #include #include #include #include #include namespace lart::abstract { using SubstitutionPass = ChainedPass< Concretization, Tainting, Synthesize >; struct PassWrapper { static PassMeta meta() { return passMeta< PassWrapper >( "Abstraction", "Abstract annotated values to given domains." ); } void run( llvm::Module & m ) { auto passes = make_chained_pass( CreateAbstractMetadata() , VPA() , Decast() , VPA() // run once more to propagate through decasted functions , StashingPass() , Syntactic() , LowerToBool() , AddAssumes() , SubstitutionPass() , CallInterrupt() , Cleanup() ); passes.run( m ); } }; inline std::vector< PassMeta > passes() { return { PassWrapper::meta() }; } } // namespace lart::abstract