// -*- C++ -*- (c) 2016 Henrich Lauko #pragma once DIVINE_RELAX_WARNINGS #include DIVINE_UNRELAX_WARNINGS #include #include #include #include #include namespace lart { namespace abstract { struct Abstraction : lart::Pass { virtual ~Abstraction() {} static PassMeta meta() { return passMeta< Abstraction >( "Abstraction", "Substitutes annotated values by abstract values." ); } llvm::PreservedAnalyses run( llvm::Module & ) override; private: void init( llvm::Module & ); void preprocess( llvm::Function * ); void process( llvm::Instruction * ); void process( llvm::Argument * ); void process( llvm::Function *, std::vector< llvm::Value * > const& ); void processAllocas( llvm::Function * ); void propagate( llvm::Value * ); void propagateFromCall( llvm::CallInst * ); llvm::Function * changeReturn( llvm::Function * ); AbstractBuilder builder; AbstractWalker walker; std::set< llvm::Function * > _unused; }; static inline PassMeta abstraction_pass() { return Abstraction::meta(); } } // namespace abstract } // namespace lart