class Bpl::Preemption

Constants

DEFAULT_PREEMPTION_ANNOTATION

Public Instance Methods

run!(program) click to toggle source
# File lib/bpl/passes/concurrency/preemption.rb, line 16
def run! program
  program.each do |proc|
    next unless proc.is_a?(ProcedureDeclaration)
    next unless proc.body
    next if proc.has_attribute?(atomicity.attribute)
    proc.each do |stmt|
      next unless stmt.is_a?(AssignStatement) | stmt.is_a?(HavocStatement)
      next unless stmt.any? do |g|
        g.is_a?(StorageIdentifier) && g.is_global? && g.is_variable?
      end
      stmt.insert_before bpl("assume {:#{attribute}} true;")
    end
  end

end