Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

driver_lexer.mll 3.68 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12

{
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
13
  open Format
14 15
  open Lexing
  open Driver_parser
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
16

17 18 19 20 21 22
  exception IllegalCharacter of char

  let () = Exn_printer.register (fun fmt e -> match e with
    | IllegalCharacter c -> fprintf fmt "illegal character %c" c
    | _ -> raise e)

Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
23
  let keywords = Hashtbl.create 97
24 25
  let () =
    List.iter
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
26 27
      (fun (x,y) -> Hashtbl.add keywords x y)
      [ "theory", THEORY;
28 29 30 31 32 33 34 35
        "end", END;
        "syntax", SYNTAX;
        "remove", REMOVE;
        "meta", META;
        "prelude", PRELUDE;
        "printer", PRINTER;
        "valid", VALID;
        "invalid", INVALID;
36
        "timeout", TIMEOUT;
37
        "outofmemory", OUTOFMEMORY;
38
        "time",    TIME;
39 40
        "unknown", UNKNOWN;
        "fail", FAIL;
41
        "constant", CONSTANT;
42 43
        "function", FUNCTION;
        "predicate", PREDICATE;
44 45
        "type", TYPE;
        "prop", PROP;
46
        "filename", FILENAME;
47
        "transformation", TRANSFORM;
48 49 50 51 52 53
        "plugin", PLUGIN;
        "blacklist", BLACKLIST;
        (* WhyML *)
        "module", MODULE;
        "exception", EXCEPTION;
        "val", VAL;
54
        "converter", CONVERTER;
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
55 56
      ]

57 58
}

Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
59 60 61 62 63
let space = [' ' '\t' '\r']
let alpha = ['a'-'z' 'A'-'Z' '_']
let digit = ['0'-'9']
let ident = alpha (alpha | digit | '\'')*

64 65 66
let op_char = ['=' '<' '>' '~' '+' '-' '*' '/' '%'
               '!' '$' '&' '?' '@' '^' '.' ':' '|' '#']

67
rule token = parse
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
68
  | '\n'
69
      { Lexlib.newline lexbuf; token lexbuf }
70
  | space+
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
71
      { token lexbuf }
72 73
  | "(*)"
      { LEFTPAR_STAR_RIGHTPAR }
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
74
  | "(*"
75
      { Lexlib.comment lexbuf; token lexbuf }
76
  | '_'
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
77 78 79
      { UNDERSCORE }
  | ident as id
      { try Hashtbl.find keywords id with Not_found -> IDENT id }
80 81
  | digit+ as i
      { INTEGER (int_of_string i) }
82 83 84 85 86 87
  | "<-"
      { LARROW }
  | "["
      { LEFTSQ }
  | "]"
      { RIGHTSQ }
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
88 89 90 91 92 93
  | "("
      { LEFTPAR }
  | ")"
      { RIGHTPAR }
  | "."
      { DOT }
94 95
  | ","
      { COMMA }
96 97
  | "'"
      { QUOTE }
98 99
  | op_char+ as op
      { OPERATOR op }
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
100
  | "\""
101
      { STRING (Lexlib.string lexbuf) }
102
  | "import" space*  "\""
103
      { INPUT (Lexlib.string lexbuf) }
104
  | eof
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
105 106
      { EOF }
  | _ as c
107
      { raise (IllegalCharacter c) }
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
108 109

{
110
  let parse_file_gen parse input_lexbuf lexbuf =
111 112 113 114 115 116 117 118
    let s = Stack.create () in
    Stack.push lexbuf s;
    let rec multifile lex_dumb =
      let lexbuf = Stack.top s in
      let tok = token lexbuf in
      Loc.transfer_loc lexbuf lex_dumb;
      match tok with
        | INPUT filename ->
119 120
          let dirname = Filename.dirname lexbuf.lex_curr_p.pos_fname in
          let filename = Sysutil.absolutize_filename dirname filename in
121 122 123 124 125 126 127
          Stack.push (input_lexbuf filename) s;
          multifile lex_dumb
        | EOF -> ignore (Stack.pop s);
          if Stack.is_empty s then EOF else multifile lex_dumb
        | _ -> tok in
    let lex_dumb = Lexing.from_function (fun _ _ -> assert false) in
    Loc.transfer_loc lexbuf lex_dumb;
128
    Loc.with_location (parse multifile) lex_dumb
129 130 131

  let parse_file = parse_file_gen Driver_parser.file
  let parse_file_extract = parse_file_gen Driver_parser.file_extract
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
132
}