(**************************************************************************)
(*  This file is part of BINSEC.                                          *)
(*                                                                        *)
(*  Copyright (C) 2016-2021                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

  | "while"                   { WHILE }
  | "do"                      { DO }
  | "for"                     { FOR }
  | "in"                      { IN }
  | "to"                      { TO }
  | "case"                    { CASE }
  | "is"                      { IS }
  | "as"                      { AS }
  | ";"                       { SEMICOLON }
  | "end"                     { END }
  | "assert"                  { ASSERT }
  | "assume"                  { ASSUME }
  | ":="                      { ASSIGN }
  | "goto"                    { GOTO }
  | "jump"                    { JUMP }
  | "halt"                    { HALT }
  | "abort"                   { ABORT }
  | "undef"                   { UNDEF }
  | "nondet"                  { NONDET }
  | "at"                      { AT }
  | "if"                      { IF }
  | "then"                    { THEN }
  | "else"                    { ELSE }
  | "true"                    { CONST Bitvector.one }
  | "false"                   { CONST Bitvector.zero }
  | "+"                       { PLUS }
  | "-"                       { MINUS }
  | "*"                       { MUL }
  | '/' 'u'?                  { UDIV }
  | "/s"                      { SDIV }
  | '%' 'u'?                  { UMOD }
  | "%s"                      { SMOD }
  | "="                       { EQUAL }
  | "<>"                      { DIFF }
  | "<=" 'u'?                 { ULE }
  | '<' 'u'?                  { ULT }
  | ">=" 'u'?                 { UGE }
  | '>' 'u'?                  { UGT }
  | "<=s"                     { SLE }
  | "<s"                      { SLT }
  | ">=s"                     { SGE }
  | ">s"                      { SGT }
  | "~"
  | "!"                       { NOT }
  | "&"                       { AND }
  | "|"                       { OR }
  | "^"                       { XOR }
  | "lsl"                     { LSL }
  | "lsr"                     { LSR }
  | "asr"                     { ASR }
  | "rol"                     { ROL }
  | "ror"                     { ROR }
  | "::"                      { CONCAT }
  | "&&"                      { LAND }
  | "||"                      { LOR }
  | "@["                      { LMEM }
  | "]"                       { RMEM }
  | "<-"                      { LARROW }
  | "->"                      { RARROW }
  | "("                       { LPAR }
  | ")"                       { RPAR }
  | "?"                       { QMARK }
  | ":"                       { COLON }
  | ","                       { COMMA }
  | "_"                       { ANY }
  | "uext" (digit+ as s)
    	   { ZEXT (int_of_string s) }
  | "sext" (digit+ as s)
    	   { SEXT (int_of_string s) }
  | '<' (wident as s) ":last>"
    	   { SYMBOL (s, Dba.VarTag.Last) }
  | '<' (wident as s) ":size>"
    	   { SYMBOL (s, Dba.VarTag.Size) }
  | '<' (wident as s) ":value"? '>'
    	   { SYMBOL (s, Dba.VarTag.Value) }
  | '.' (ident as s)
    	   { LABEL s }
  | (ident as s) '<' (digit+ as i) '>'
    	   { IDENT (s, int_of_string i) }
  | ident as s
    	   { IDENT (s, -1) }
  | '-'? digit+ as s
    	   { INT (Z.of_string s) }
  | '{' space* (digit+ as hi) space* ".." space* (digit+ as lo) '}'
    	   { RANGE { Interval.hi=int_of_string hi; lo=int_of_string lo } }
  | bin | hex as s
           { INT (Z.of_string s) }
  | '"' ([^'"']* as s) '"'
           { let s = Scanf.unescaped s in
	     CONST (Bitvector.create (Z.of_bits s) (String.length s * 8)) }
  | '"' ([^'"']* as s) '"' 'z'
           { let s = Scanf.unescaped s in
	     CONST (Bitvector.create (Z.of_bits s)
	     	   ((String.length s + 1) * 8)) }
  | space+          { token lexbuf }
  | '#' [^'\n']* '\n'
  | "\n"            { Lexing.new_line lexbuf; token lexbuf }
  | eof             { EOF }
  | _
      {
        let open Lexing in
        let line = (lexeme_start_p lexbuf).pos_lnum in
        let msg =
          Format.asprintf "Unkown lexeme %s at line %d" (lexeme lexbuf) line in
        failwith msg }