Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
1c8e6b22
Commit
1c8e6b22
authored
2 years ago
by
Andre Maroneze
Browse files
Options
Downloads
Patches
Plain Diff
[Kernel] change configurator/fc_config settings to avoid warnings with Cygwin
parent
7057d326
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
configurator.ml
+62
-46
62 additions, 46 deletions
configurator.ml
src/kernel_internals/runtime/fc_config.ml.in
+7
-1
7 additions, 1 deletion
src/kernel_internals/runtime/fc_config.ml.in
with
69 additions
and
47 deletions
configurator.ml
+
62
−
46
View file @
1c8e6b22
...
...
@@ -55,52 +55,69 @@ module Temp = struct (* Almost copied from configurator *)
try_name
0
end
module
C_
compile
r
=
struct
(* This could be put in Dune? *)
module
C_
preprocesso
r
=
struct
(* This could be put in Dune? *)
type
t
=
{
compiler
:
string
{
preprocessor
:
string
;
pp_opt
:
string
option
;
is_gnu
:
bool
}
let
find_compiler
configurator
=
let
cc_env
=
try
Sys
.
getenv
"CC"
with
Not_found
->
""
in
if
cc_env
<>
""
then
cc_env
let
stdout_contains
out
str
=
let
re
=
Str
.
regexp_string
str
in
try
ignore
(
Str
.
search_forward
re
out
0
);
true
with
Not_found
->
false
let
find_preprocessor
configurator
=
let
cc_env
=
try
Sys
.
getenv
"CPP"
with
Not_found
->
""
in
if
cc_env
<>
""
then
(
cc_env
,
None
)
(* assume default CPP needs no args *)
else
let
finder
compiler
=
C
.
which
configurator
compiler
|>
Option
.
is_some
in
try
List
.
find
finder
[
"gcc"
;
"cc"
;
"cl.exe"
]
with
Not_found
->
C
.
die
"Could not find a C compiler"
let
finder
(
command
,
_pp_opt
)
=
C
.
which
configurator
command
|>
Option
.
is_some
in
(* Note: We could add 'cl.exe' to the list, but since it requires
'/<opt>' and not '-<opt>' for its options, it will fail in every
check anyway. So the user may manually specify it if they want it,
but having it here brings no benefit.
Note: 'cpp' is NOT the POSIX way to call the preprocessor, and it
behaves VERY badly on macOS (as if using '-traditional', see
https://stackoverflow.com/questions/9508159).
Therefore, we try `gcc -E` and `cc -E`, but not 'cpp'.
*)
try
List
.
find
finder
[(
"gcc"
,
Some
"-E"
);
(
"cc"
,
Some
"-E"
)]
with
Not_found
->
C
.
die
"Could not find a C preprocessor"
let
write_file
name
code
=
let
out
=
open_out
name
in
Printf
.
fprintf
out
"%s"
code
;
close_out
out
let
call
configurator
compile
r
options
code
=
let
call
configurator
preprocesso
r
options
code
=
let
dir
=
Temp
.
create_dir
()
in
let
file
=
Temp
.
create
~
dir
~
suffix
:
".c"
(
fun
name
->
write_file
name
code
)
in
C
.
Process
.
run
configurator
~
dir
compiler
(
options
@
[
file
])
C
.
Process
.
run
configurator
~
dir
preprocessor
(
options
@
[
file
])
let
preprocess_flag
=
"-E"
let
is_gnu
configurator
compiler
=
let
code
=
{
|#
ifndef
__GNUC__
this
is
not
a
gnuc
compiler
let
is_gnu
configurator
preprocessor
=
let
code
=
{
|#
ifdef
_FC_UNDEFINED_SYMBOL
#
error
This
should
not
remain
after
preprocessing
#
endif
int
kept_after_preprocessing
=
42
;
|
}
in
(
call
configurator
compiler
[
"-c"
]
code
)
.
exit_code
=
0
(* GNU preprocessors are always compatible with '-E'.
For 'cpp', the '-E' flag is unnecessary, but still works. *)
let
result
=
call
configurator
preprocessor
[
"-E"
]
code
in
result
.
exit_code
=
0
&&
stdout_contains
result
.
stdout
"kept_after_preprocessing"
&&
not
(
stdout_contains
result
.
stdout
"should not remain"
)
let
get
configurator
=
let
compiler
=
find_compiler
configurator
in
let
is_gnu
=
is_gnu
configurator
compiler
in
{
compiler
;
is_gnu
}
let
preprocess
configurator
t
options
=
call
configurator
t
.
compiler
(
preprocess_flag
::
options
)
let
preprocessor
,
pp_opt
=
find_preprocessor
configurator
in
let
is_gnu
=
is_gnu
configurator
preprocessor
in
{
preprocessor
;
pp_opt
;
is_gnu
}
let
_compile
configurator
t
options
=
call
configurator
t
.
compiler
(
"-c"
::
options
)
let
preprocess
configurator
t
options
code
=
call
configurator
t
.
preprocessor
(
Option
.
to_list
t
.
pp_opt
@
options
)
code
end
(* Frama-C specific part *)
...
...
@@ -113,40 +130,39 @@ module Cpp = struct
int
main
()
{}
|
}
let
check
configurator
compile
r
=
let
check
configurator
preprocesso
r
=
let
options
=
[
"-dD"
;
"-nostdinc"
]
in
(
C_
compile
r
.
preprocess
configurator
compile
r
options
code
)
.
exit_code
=
0
(
C_
preprocesso
r
.
preprocess
configurator
preprocesso
r
options
code
)
.
exit_code
=
0
end
module
KeepComments
=
struct
let
code
=
{
|/*
Check
whether
comments
are
kept
in
output
*/|
}
let
check
configurator
compiler
options
=
let
result
=
C_compiler
.
preprocess
configurator
compiler
options
code
in
result
.
exit_code
=
0
&&
let
re
=
Str
.
regexp_string
"kept"
in
try
ignore
(
Str
.
search_forward
re
result
.
stdout
0
);
true
with
Not_found
->
false
let
keep_comments_option
=
"-C"
let
check
configurator
preprocessor
=
let
result
=
C_preprocessor
.
preprocess
configurator
preprocessor
[
keep_comments_option
]
code
in
result
.
exit_code
=
0
&&
C_preprocessor
.
stdout_contains
result
.
stdout
"kept"
end
module
Archs
=
struct
let
opt_m_code
value
=
Format
.
asprintf
{
|/*
Check
if
preprocessor
supports
option
-
m
%
s
*/|
}
value
let
check
configurator
compile
r
arch
=
let
check
configurator
preprocesso
r
arch
=
let
code
=
opt_m_code
arch
in
let
options
=
[
Format
.
asprintf
"-m%s"
arch
]
in
if
(
C_
compile
r
.
preprocess
configurator
compile
r
options
code
)
.
exit_code
=
0
if
(
C_
preprocesso
r
.
preprocess
configurator
preprocesso
r
options
code
)
.
exit_code
=
0
then
Some
arch
else
None
let
supported_archs
configurator
compile
r
archs
=
let
check
=
check
configurator
compile
r
in
let
supported_archs
configurator
preprocesso
r
archs
=
let
check
=
check
configurator
preprocesso
r
in
List
.
map
(
fun
s
->
"-m"
^
s
)
@@
List
.
filter_map
check
archs
end
type
t
=
{
compiler
:
C_compile
r
.
t
{
preprocessor
:
C_preprocesso
r
.
t
;
default_args
:
string
list
;
is_gnu_like
:
bool
;
keep_comments
:
bool
...
...
@@ -154,13 +170,13 @@ int main(){}
}
let
get
configurator
=
let
compiler
=
C_compile
r
.
get
configurator
in
let
default_args
=
[
"-C"
;
"-I."
]
in
let
is_gnu_like
=
GnuLike
.
check
configurator
compile
r
in
let
keep_comments
=
KeepComments
.
check
configurator
compiler
[
"-C"
]
in
let
preprocessor
=
C_preprocesso
r
.
get
configurator
in
let
default_args
=
Option
.
to_list
preprocessor
.
pp_opt
@
[
"-C"
;
"-I."
]
in
let
is_gnu_like
=
GnuLike
.
check
configurator
preprocesso
r
in
let
keep_comments
=
KeepComments
.
check
configurator
preprocessor
in
let
supported_archs_opts
=
Archs
.
supported_archs
configurator
compile
r
[
"16"
;
"32"
;
"64"
]
in
{
compile
r
;
default_args
;
is_gnu_like
;
keep_comments
;
supported_archs_opts
}
Archs
.
supported_archs
configurator
preprocesso
r
[
"16"
;
"32"
;
"64"
]
in
{
preprocesso
r
;
default_args
;
is_gnu_like
;
keep_comments
;
supported_archs_opts
}
let
pp_flags
fmt
=
let
pp_sep
fmt
()
=
Format
.
fprintf
fmt
" "
in
...
...
@@ -168,8 +184,8 @@ int main(){}
let
pp_default_cpp
fmt
cpp
=
Format
.
fprintf
fmt
"%s %a"
cpp
.
compiler
.
compile
r
pp_flags
(
C_compiler
.
preprocess_flag
::
cpp
.
default_args
)
cpp
.
preprocessor
.
preprocesso
r
pp_flags
cpp
.
default_args
let
pp_archs
fmt
cpp
=
let
pp_arch
fmt
arch
=
Format
.
fprintf
fmt
"
\"
%s
\"
"
arch
in
...
...
This diff is collapsed.
Click to expand it.
src/kernel_internals/runtime/fc_config.ml.in
+
7
−
1
View file @
1c8e6b22
...
...
@@ -63,7 +63,13 @@ let preprocessor = env_or_default (fun x -> x) default_cpp
let using_default_cpp = env_or_default (fun _ -> false) true
let preprocessor_is_gnu_like =
env_or_default (fun _ -> false) @FRAMAC_GNU_CPP@
env_or_default
(fun _ ->
(* be more lenient when trying to determine if the preprocessor
is gnu-like: in Cygwin, for instance, CC is "<prefix>-gcc" but
CPP is "<prefix>-cpp", so this extra test allows proper detection. *)
let env = Sys.getenv "CC" ^ default_cpp_args in
env=default_cpp) @FRAMAC_GNU_CPP@
let preprocessor_supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@]
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment