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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
(**************************************************************************)
(* *)
(* The Why platform for program certification *)
(* *)
(* Copyright (C) 2002-2011 *)
(* *)
(* Jean-Christophe FILLIATRE, CNRS & Univ. Paris-sud 11 *)
(* Claude MARCHE, INRIA & Univ. Paris-sud 11 *)
(* Yannick MOY, Univ. Paris-sud 11 *)
(* Romain BARDOU, Univ. Paris-sud 11 *)
(* *)
(* Secondary contributors: *)
(* *)
(* Thierry HUBERT, Univ. Paris-sud 11 (former Caduceus front-end) *)
(* Nicolas ROUSSET, Univ. Paris-sud 11 (on Jessie & Krakatoa) *)
(* Ali AYAD, CNRS & CEA Saclay (floating-point support) *)
(* Sylvie BOLDO, INRIA (floating-point support) *)
(* Jean-Francois COUCHOT, INRIA (sort encodings, hyps pruning) *)
(* Mehdi DOGGUY, Univ. Paris-sud 11 (Why GUI) *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
(*i $Id: cpp.mll,v 1.22 2008-11-05 14:03:13 filliatr Exp $ i*)
(* C-preprocessor for Caduceus *)
{
open Coptions
open Printf
open Lexing
let channel_out = ref stdout
let print s = output_string !channel_out s
let start_of_comment_string = "start_of_comment_string_multiple_lines"
let start_of_comment_string_one_line = "start_of_comment_string_one_line"
let end_of_comment_string = "end_of_comment_string"
}
let start_of_comment_string = "start_of_comment_string_multiple_lines"
let start_of_comment_string_one_line = "start_of_comment_string_one_line"
let end_of_comment_string = "end_of_comment_string"
rule before = parse
| "/*@" { print start_of_comment_string; before lexbuf }
(* | "*/" { print end_of_comment_string; before lexbuf } *)
| "//@" { print start_of_comment_string_one_line; before lexbuf }
| "# 1 \"<" [^'\n''>']* ">\"\n#define" [^'\n']* '\n' { before lexbuf }
| "#define __" [^'\n']* '\n' { before lexbuf }
| _ { print (lexeme lexbuf); before lexbuf }
| eof { () }
and after = parse
| start_of_comment_string_one_line { print "//@"; after lexbuf }
| start_of_comment_string { print "/*@"; after lexbuf }
| end_of_comment_string { print "*/"; after lexbuf }
| _ { print (lexeme lexbuf); after lexbuf }
| eof { () }
{
let rec local_temp_file basename suffix =
let i = Random.int 536870912 in
let f = basename ^ string_of_int i ^ suffix in
if Sys.file_exists f then local_temp_file basename suffix else f
(* [translate_using filter f] translates file [f] using lexer rule [filter]
and returns the translated file *)
let translate_using filter f =
let cin = open_in f in
let lb = from_channel cin in
let pf = local_temp_file (Filename.basename f) ".c" in
let cout = open_out pf in
fprintf cout "# 1 \"%s\"\n" f;
channel_out := cout;
filter lb;
close_in cin;
close_out cout;
pf
let before_cpp = translate_using before
let after_cpp = translate_using after
(* [external_cpp f] runs an external C preprocessor on file [f];
returns the preprocessed file. *)
let external_cpp f =
let ppf = local_temp_file (Filename.basename f) ".i" in
let cmd = sprintf "%s %s > %s" cpp_command f ppf in
ignore (Sys.command cmd);
ppf
(* [first_cpp f] runs an external C preprocessor on file [f] and preserves the definitions in trace;
returns the preprocessed file. *)
let first_cpp f =
let ppf = local_temp_file (Filename.basename f) ".c" in
ignore (Sys.command (sprintf "%s -dD %s > %s" cpp_command f ppf));
(* ignore (Sys.command (sprintf "LANG=en ; %s -dD %s > %s" cpp_command f ppf)); *)
ppf
(* [translate f] preprocesses file [f]; returns the preprocessed file and a
finalizer to be called when the preprocessed file has been used. *)
let translate f =
if with_cpp then begin
let inlinedf = first_cpp f in
let pf = before_cpp inlinedf in
let ppf = external_cpp pf in
Sys.remove inlinedf;
Sys.remove pf;
let pppf = after_cpp ppf in
Sys.remove ppf;
(* if not debug then *) at_exit (fun () -> Sys.remove pppf);
pppf
end else begin
f
end
let dump f =
let cin = open_in f in
try
while true do printf "%s\n" (input_line cin) done
with End_of_file ->
close_in cin
let cpp f =
let pf = translate f in
if cpp_dump then begin dump pf; exit 0 end;
pf
}
|
