class Bpl::AST::CallStatement

Public Instance Methods

abstract() { |{ description: "havocing assignments and modifies", weight: declaration.count, action: proc do replace_with(*map{|id| bpl("havoc #{id};")}) end }| ... } click to toggle source
# File lib/bpl/passes/transformation/abstraction.rb, line 204
def abstract
  if procedure.declaration
    unless assertion_localization.has_assert[procedure.declaration]
      ids = procedure.declaration.modifies
      assignments.each do |expr|
        loop do
          if expr.is_a?(Identifier)
            ids << expr
            break
          else
            expr = expr.map
          end
        end
      end
      yield({
        description: "havocing assignments and modifies",
        weight: procedure.declaration.count,
        action: Proc.new do
          replace_with(*ids.map{|id| bpl("havoc #{id};")})
        end
      })

    else
      decl = each_ancestor.find{|d| d.is_a?(ProcedureDeclaration)}
      yield({
        description: "detaching arguments and returns",
        weight: 0,
        action: Proc.new do
          (arguments + assignments).each do |x|
            v = decl.fresh_var(x.declaration.type)
            x.replace_with(v)
          end
        end
      })
    end
  end
end
forall?() click to toggle source
# File lib/bpl/ast/statement.rb, line 60
def forall?; @assignments.nil? end
show() { |a| ... } click to toggle source
# File lib/bpl/ast/statement.rb, line 62
def show(&blk)
  if @assignments
    rets = @assignments.map{|a| yield a} * ", " + (@assignments.empty? ? '' : ' := ')
  else
    rets = "forall"
  end
  proc = yield @procedure
  args = @arguments.map{|a| yield a} * ", "
  "#{yield :call} #{show_attrs(&blk)} #{rets} #{proc}(#{args});".fmt
end
target() click to toggle source
# File lib/bpl/ast/statement.rb, line 61
def target; @procedure.declaration end
type_check() click to toggle source
# File lib/bpl/passes/analysis/type_checking.rb, line 34
def type_check
  return unless d = @procedure.declaration

  params = d.parameters # .map(&:flatten).flatten
  rets = d.returns # .map(&:flatten).flatten

  unless params.count == arguments.count
    warn "wrong number of arguments in call of #{d.signature}" \
      "\n  #{hilite.underline}"
  end

  arguments.each.with_index do |a,i|
    break unless i < params.count
    unless params[i].type.expand.to_s == a.type.expand.to_s
      warn "invalid type for argument #{i} in call of #{d.signature}" \
        "\n  #{hilite.underline}"
    end
  end

  unless rets.count == assignments.count
    warn "wrong number of return assignments in call of #{d.signature}" \
      "\n  #{hilite.underline}"
  end

  assignments.each.with_index do |a,i|
    break unless i < rets.count
    unless rets[i].type.expand.to_s == a.type.expand.to_s
      warn "invalid type for return assignment #{i} in call of #{d.signature}" \
        "\n  #{hilite.underline}"
    end
  end

end