diff --git a/divine/rt/dios-cc.cpp b/divine/rt/dios-cc.cpp index 5a32729b0f09c6362616a94f8e398bc090df52be..5a797b33a1bced224bee1de1cb34b8a3ac41fafd 100644 --- a/divine/rt/dios-cc.cpp +++ b/divine/rt/dios-cc.cpp @@ -91,7 +91,24 @@ auto NativeDiosCC::link_dios_native( bool cxx ) std::unique_ptr< llvm::Module > NativeDiosCC::link_bitcode() { - return cc::link_bitcode< rt::DiosCC, true >( _files, _clang, _po.libSearchPath ); + auto drv = std::make_unique< DiosCC >( _clang.context() ); + std::unique_ptr< llvm::Module > m = Native::do_link_bitcode< rt::DiosCC >(); + drv->link( std::move( m ) ); + drv->linkLibs( DiosCC::defaultDIVINELibs ); + + m = drv->takeLinked(); + + for ( auto& func : *m ) + if ( func.isDeclaration() && !whitelisted( func ) ) + throw cc::CompileError( "Symbol undefined (function): " + func.getName().str() ); + + for ( auto& val : m->globals() ) + if ( auto G = dyn_cast< llvm::GlobalVariable >( &val ) ) + if ( !G->hasInitializer() && !whitelisted( *G ) ) + throw cc::CompileError( "Symbol undefined (global variable): " + G->getName().str() ); + + verifyModule( *m ); + return m; } void NativeDiosCC::link()