class Bpl::Inlining
Public Instance Methods
run!(program)
click to toggle source
# File lib/bpl/passes/transformation/inlining.rb, line 7 def run! program $temp << source = "bam.#{Time.now.to_f}.bpl" $temp << inlined = "bam.inlined.#{Time.now.to_f}.bpl" File.write(source,program) cmd = "#{boogie} /noVerify /printInlined #{source} 1> #{inlined} 2>&1" abort "Failed to invoke Boogie for inlining" unless system cmd inlined = File.read(inlined) 2.times do inlined = inlined.slice(inlined.index("\n") + 1 .. inlined.rindex("\n")-1) end inlined = timed 'Parsing' do BoogieLanguage.new.parse(inlined) end program.declarations.each do |decl| next if decl.is_a?(ProcedureDeclaration) && decl.body inlined.declarations << decl end resolve! inlined correct_modifies! inlined return inlined end