module Kernel

Public Instance Methods

abort(str) click to toggle source
# File lib/bam/prelude.rb, line 84
def abort(str)
  old_abort("Error: #{str}".red)
end
Also aliased as: old_abort
boogie() click to toggle source
# File lib/bam/prelude.rb, line 112
def boogie
  ['Boogie','boogie','Boogie.exe','boogie.exe'].each do |b|
    return "#{b}" if not `which #{b}`.empty?
  end
  abort "'Boogie' missing from executable path.\n" \
    "Verification requires Boogie; please install it."
end
bpl(str) click to toggle source
# File lib/bam/prelude.rb, line 120
def bpl(str)
  BoogieLanguage.new.parse_str(str)
end
bpl_expr(str) click to toggle source
# File lib/bam/prelude.rb, line 124
def bpl_expr(str)
  BoogieLanguage.new.parse_expr(str)
end
bpl_type(str) click to toggle source
# File lib/bam/prelude.rb, line 128
def bpl_type(str)
  BoogieLanguage.new.parse_type(str)
end
info(*args) click to toggle source
# File lib/bam/prelude.rb, line 88
def info(*args)
  args = [""] if args.empty?
  args.each do |str|
    puts ($stdout.tty? ? str.light_black : str.comment) unless $quiet
  end
end
old_abort(str)
Alias for: abort
smack() click to toggle source
# File lib/bam/prelude.rb, line 105
def smack
  abort "'smackgen.py' missing from executable path.\n" \
    "The C/LLVM front end requires SMACK; please install it." \
  if `which smackgen.py`.empty?
  'smackgen.py --verifier=boogie-plain'
end
warn(*args) click to toggle source
# File lib/bam/prelude.rb, line 95
def warn(*args)
  return unless $show_warnings
  args.each do |str|
    unless $warnings.include? str
      $stderr.puts "Warning: #{str}".yellow
      $warnings << str
    end
  end
end