class Bpl::AST::Trace
Attributes
src_file[RW]
steps[RW]
Public Class Methods
new(trace_file, program, model)
click to toggle source
# File lib/bpl/ast/trace.rb, line 7 def initialize(trace_file, program, model) @program = program @model = model @steps = [] lines = File.read(trace_file).lines lines.shift until lines.first =~ /Execution trace:/ num_blocks = 0 while lines.first !~ /Boogie program verifier finished/ line = lines.shift next if line.empty? line.match /([^\s]+)\((\d+),(\d+)\): ([^\s]+)/ do |m| src_file, line, col, label = m[1], m[2].to_i, m[3].to_i, m[4] src_file = File.join(File.dirname(trace_file), src_file) case label when /Entry/, /Return/ else block = get_block(src_file,line-1) proc = get_proc(src_file,line-1) @steps << {file: src_file, line: line, col: col, proc: proc, label: label, block: block} end end end end
Public Instance Methods
svg_craziness()
click to toggle source
# File lib/bpl/ast/trace.rb, line 82 def svg_craziness end
to_s()
click to toggle source
# File lib/bpl/ast/trace.rb, line 59 def to_s gs = @program.global_variables.map{|g| g.names}.flatten num_steps_shown = 0 ("-" * 80) + "\n" + @model.constants.map{|c,v| "const #{c} = #{value_to_s(v)}"} * "\n" + "\n" + @model.functions.map{|f,v| "function #{f}\n#{value_to_s(v)}"} * "\n" + "\n" + ("-" * 80) + "\n" + steps = @steps.map.with_index do |step,i| vars = @model.variables(i).select{|v,_| gs.include?(v)} next if vars.empty? num_steps_shown += 1 "step #{i} / line #{step[:line]} / proc #{step[:proc]} / label #{step[:label]}\n" + ("-" * 80) + "\n" + "#{vars.map{|x,v| " var #{x} = #{value_to_s(v)}"} * "\n"}" + "\n" + "\n" + step[:block].first(10).join + (step[:block].count > 10 ? " ...\n" : "") + ("-" * 80) end.compact * "\n" + "(#{@steps.count - num_steps_shown} steps omitted)" end
value_to_s(value)
click to toggle source
# File lib/bpl/ast/trace.rb, line 36 def value_to_s value if value.is_a?(Hash) && value.include?(:map) "[" + value.reject{|k,_| k == :map}.map do |k,v| "#{k || "*"}:#{value_to_s(v)}" end * ", " + "]" elsif value.is_a?(Hash) " " + value.map do |ks,v| case ks when nil; "else" when Array; "(#{ks.map{|k| value_to_s(k)} * ","})" else ks.to_s end + " -> #{value_to_s(v)}" end * "\n " elsif value.to_s =~ /T@U!val!\d+/ id = value.to_s.match(/T@U!val!(\d+)/)[1] "unknown/#{id}" else value.to_s end end