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
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