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