class BoogieLanguage
Constants
- Racc_arg
- Racc_debug_parser
- Racc_token_to_s_table
Attributes
filename[R]
lineno[R]
state[RW]
Public Instance Methods
_next_token()
click to toggle source
# File lib/bpl/lexer.rex.rb, line 58 def _next_token text = @ss.peek(1) @lineno += 1 if text == "\n" token = case @state when nil case when (text = @ss.scan(/\$\$PARSE_DECL\$\$/)) action { [:PARSE_DECL, ""] } when (text = @ss.scan(/\$\$PARSE_PARAM\$\$/)) action { [:PARSE_PARAM, ""] } when (text = @ss.scan(/\$\$PARSE_SPEC\$\$/)) action { [:PARSE_SPEC, ""] } when (text = @ss.scan(/\$\$PARSE_BLOCKS\$\$/)) action { [:PARSE_BLOCKS, ""] } when (text = @ss.scan(/\$\$PARSE_STMT\$\$/)) action { [:PARSE_STMT, ""] } when (text = @ss.scan(/\$\$PARSE_EXPR\$\$/)) action { [:PARSE_EXPR, ""] } when (text = @ss.scan(/\$\$PARSE_TYPE\$\$/)) action { [:PARSE_TYPE, ""] } when (text = @ss.scan(/\/\*((?!\*\/)(.|\n))*\*\//)) ; when (text = @ss.scan(/\/\/.*(?=\n)/)) ; when (text = @ss.scan(/\"[^"]*\"/)) action { [:STRING, text[1..-2]]} when (text = @ss.scan(/\s/)) ; when (text = @ss.scan(/<==>|==>|\|\||&&|==|!=|<:|<=|<|>=|>|\+\+|\+|-|\*|\/|{:|:=|::|:|\|/)) action { [text, text] } when (text = @ss.scan(/\d+bv\d+/)) action { [:BITVECTOR, {value: text[/(\d+)bv/,1].to_i, base: text[/bv(\d+)/,1].to_i}] } when (text = @ss.scan(/\d+/)) action { [:NUMBER, text.to_i] } when (text = @ss.scan(/bv\d+\b/)) action { [:BVTYPE, text[2..-1].to_i] } when (text = @ss.scan(/\b(assert|assume|axiom|bool|break|bv(\d+)|call|complete|const|else|ensures|exists|false|finite|forall|free|function|goto|havoc|if|implementation|int|invariant|modifies|old|procedure|requires|return|returns|then|true|type|unique|var|where|while)\b(?![\w.$\#'`~^\\?])/)) action { [text, Token.new(lineno)] } when (text = @ss.scan(/[a-zA-Z_.$\#'`~^\\?][\w.$\#'`~^\\?]*/)) action { [:IDENTIFIER, text] } when (text = @ss.scan(/./)) action { [text, text] } else text = @ss.string[@ss.pos .. -1] raise ScanError, "can not match: '" + text + "'" end # if else raise ScanError, "undefined state: '" + state.to_s + "'" end # case state token end
_reduce_none(val, _values)
click to toggle source
# File lib/bpl/parser.tab.rb, line 2249 def _reduce_none(val, _values) val[0] end
action() { || ... }
click to toggle source
# File lib/bpl/lexer.rex.rb, line 27 def action yield end
load_file( filename )
click to toggle source
# File lib/bpl/lexer.rex.rb, line 37 def load_file( filename ) @filename = filename open(filename, "r") do |f| scan_setup(f.read) end end
next_token()
click to toggle source
# File lib/bpl/lexer.rex.rb, line 50 def next_token return if @ss.eos? # skips empty actions until token = _next_token or @ss.eos?; end token end
scan_file( filename )
click to toggle source
# File lib/bpl/lexer.rex.rb, line 44 def scan_file( filename ) load_file(filename) do_parse end
scan_setup(str)
click to toggle source
# File lib/bpl/lexer.rex.rb, line 21 def scan_setup(str) @ss = StringScanner.new(str) @lineno = 1 @state = nil end
scan_str(str)
click to toggle source
# File lib/bpl/lexer.rex.rb, line 31 def scan_str(str) scan_setup(str) do_parse end
Also aliased as: scan