1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
;;; flymake-boogiepl.el --- Flymake BoogiePL Extension
;; Copyright (C) 2009, 2010 Valentin Wüstholz
;; Author: Valentin Wüstholz
;; Keywords: flymake, Boogie, BoogiePL
;; Version: 0.1
;; This file is free software: you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published
;; by the Free Software Foundation, either version 3 of the License,
;; or (at your option) any later version.
;;
;; This file 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
;; General Public License for more details.
;;
;; You should have received a copy of the GNU General Public License
;; along with GNU Emacs. If not, see <http://www.gnu.org/licenses/>.
;;; Commentary:
;; This is a Flymake extension for BoogiePL.
;; To install it, you simply have to add the following lines to your .emacs file:
;; (add-to-list 'load-path (expand-file-name "path/to/this/file/"))
;; (require 'flymake-boogiepl)
;; (require 'boogiepl) ; optional
;; (define-key boogiepl-mode-map (kbd "C-c p") 'flymake-goto-prev-error) ; optional
;; (define-key boogiepl-mode-map (kbd "C-c n") 'flymake-goto-next-error) ; optional
;;; Code:
(require 'flymake)
(defcustom flymake-boogiepl-command
"boogie"
"Command to run Boogie"
:type 'string
:group 'boogie
)
(defcustom flymake-boogiepl-prelude-files
nil
"Prelude files"
:group 'boogie
)
(defcustom flymake-boogiepl-flags
(list "/nologo" "/smoke")
"Flags"
:group 'boogie
)
(defun flymake-boogiepl-init ()
(let* ((temp-file (flymake-init-create-temp-buffer-copy
'flymake-create-temp-inplace))
(local-file (file-relative-name
temp-file
(file-name-directory buffer-file-name)))
(files (if (not (member (file-relative-name (buffer-file-name))
flymake-boogiepl-prelude-files))
(cons local-file flymake-boogiepl-prelude-files)
flymake-boogiepl-prelude-files)))
(list flymake-boogiepl-command (append flymake-boogiepl-flags files))))
(defvar flymake-boogiepl-err-line-patterns '(("^\\(.*\.bpl\\)(\\([0-9]+\\),\\([0-9]+\\)): Error\\( \\S-*\\)?: \\(.*\\)$" 1 2 3 5)
("^\\(.*\.bpl\\)(\\([0-9]+\\),\\([0-9]+\\)): Related location: \\(.*\\)$" 1 2 3 4)
("^ \\(.*\.bpl\\)(\\([0-9]+\\),\\([0-9]+\\)): \\(.*\\)$" 1 2 3 4)
("^\\(.*\.bpl\\)(\\([0-9]+\\),\\([0-9]+\\)): syntax error: \\(.*\\)$" 1 2 3 4)
("^\\(found unreachable code\\):$" nil nil nil 1)))
(defvar flymake-boogiepl-allowed-file-name-masks '(("\\.bpl\\'" flymake-boogiepl-init)))
(setq flymake-allowed-file-name-masks
(append flymake-boogiepl-allowed-file-name-masks
flymake-allowed-file-name-masks))
(setq flymake-err-line-patterns
(append flymake-boogiepl-err-line-patterns
flymake-err-line-patterns))
(provide 'flymake-boogiepl)
;;; flymake-boogiepl.el ends here
|
