Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CertiCompil
CompCert-KVX
Commits
8cd40f0b
Unverified
Commit
8cd40f0b
authored
Feb 16, 2018
by
Bernhard Schommer
Browse files
Removed struct passing/return from Configurations
parent
10995833
Changes
3
Hide whitespace changes
Inline
Side-by-side
configure
View file @
8cd40f0b
...
...
@@ -176,8 +176,6 @@ casmruntime=""
clinker_needs_no_pie
=
true
clinker_options
=
""
cprepro_options
=
""
struct_passing
=
""
struct_return
=
""
#
...
...
@@ -205,8 +203,6 @@ if test "$arch" = "arm"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E"
libmath
=
"-lm"
struct_passing
=
"ints"
struct_return
=
"int1-4"
system
=
"linux"
fi
...
...
@@ -228,10 +224,8 @@ if test "$arch" = "powerpc"; then
case
"
$target
"
in
linux
)
abi
=
"linux"
struct_return
=
"ref"
;;
*
)
struct_return
=
"int1-8"
abi
=
"eabi"
;;
esac
...
...
@@ -247,7 +241,6 @@ if test "$arch" = "powerpc"; then
cprepro
=
"
${
toolprefix
}
dcc"
cprepro_options
=
"-E -D__GNUC__"
libmath
=
"-lm"
struct_passing
=
"ref-caller"
system
=
"diab"
responsefile
=
"diab"
;;
...
...
@@ -260,7 +253,6 @@ if test "$arch" = "powerpc"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -U__GNUC__ -E"
libmath
=
"-lm"
struct_passing
=
"ref-caller"
system
=
"linux"
;;
esac
...
...
@@ -283,8 +275,6 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -m32 -U__GNUC__ -E"
libmath
=
"-lm"
struct_passing
=
"ints"
struct_return
=
"int1248"
# to check!
system
=
"bsd"
;;
cygwin
)
...
...
@@ -297,8 +287,6 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -m32 -U__GNUC__ '-D__attribute__(x)=' -E"
libmath
=
"-lm"
struct_passing
=
"ints"
struct_return
=
"ref"
system
=
"cygwin"
;;
linux
)
...
...
@@ -311,8 +299,6 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -m32 -U__GNUC__ -E"
libmath
=
"-lm"
struct_passing
=
"ints"
struct_return
=
"ref"
system
=
"linux"
;;
macosx
)
...
...
@@ -328,8 +314,6 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E"
libmath
=
""
struct_passing
=
"ints"
struct_return
=
"int1248"
system
=
"macosx"
if
[[
$kernel_major
-gt
11
]]
;
then
...
...
@@ -363,8 +347,6 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -m64 -U__GNUC__ -E"
libmath
=
"-lm"
struct_passing
=
"ref-callee"
# wrong!
struct_return
=
"ref"
# to check!
system
=
"bsd"
;;
linux
)
...
...
@@ -377,8 +359,6 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -m64 -U__GNUC__ -E"
libmath
=
"-lm"
struct_passing
=
"ref-callee"
# wrong!
struct_return
=
"ref"
# to check!
system
=
"linux"
;;
macosx
)
...
...
@@ -394,8 +374,6 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E"
libmath
=
""
struct_passing
=
"ref-callee"
# wrong!
struct_return
=
"ref"
# to check!
system
=
"macosx"
;;
*
)
...
...
@@ -424,8 +402,6 @@ if test "$arch" = "riscV"; then
cprepro
=
"
${
toolprefix
}
gcc"
cprepro_options
=
"
$model_options
-std=c99 -U__GNUC__ -E"
libmath
=
"-lm"
struct_passing
=
"ref-callee"
# wrong!
struct_return
=
"ref"
# to check!
system
=
"linux"
fi
...
...
@@ -672,8 +648,6 @@ HAS_RUNTIME_LIB=$has_runtime_lib
HAS_STANDARD_HEADERS=
$has_standard_headers
LIBMATH=
$libmath
MODEL=
$model
STRUCT_PASSING=
$struct_passing
STRUCT_RETURN=
$struct_return
SYSTEM=
$system
RESPONSEFILE=
$responsefile
EOF
...
...
@@ -716,19 +690,6 @@ BITSIZE=
# ENDIANNESS=little # for ARM or x86
ENDIANNESS=
# Default calling conventions for passing structs and unions by value
# See options -fstruct-passing=<style> and -fstruct-return=<style>
# in the CompCert user's manual
#
STRUCT_PASSING=ref_callee
# STRUCT_PASSING=ref_caller
# STRUCT_PASSING=ints
#
STRUCT_RETURN=ref
# STRUCT_RETURN=int1248
# STRUCT_RETURN=int1-4
# STRUCT_RETURN=int1-8
# Target operating system and development environment
#
# Possible choices for PowerPC:
...
...
@@ -808,7 +769,6 @@ CompCert configuration:
Hardware model................
$model
Application binary interface..
$abi
Endianness....................
$endianness
Composite passing conventions. arguments:
$struct_passing
, return values:
$struct_return
OS and development env........
$system
C compiler....................
$cc
C preprocessor................
$cprepro
...
...
driver/Configuration.ml
View file @
8cd40f0b
...
...
@@ -143,34 +143,6 @@ let stdlib_path =
""
let
asm_supports_cfi
=
get_bool_config
"asm_supports_cfi"
type
struct_passing_style
=
|
SP_ref_callee
(* by reference, callee takes copy *)
|
SP_ref_caller
(* by reference, caller takes copy *)
|
SP_split_args
(* by value, as a sequence of ints *)
type
struct_return_style
=
|
SR_int1248
(* return by content if size is 1, 2, 4 or 8 bytes *)
|
SR_int1to4
(* return by content if size is <= 4 *)
|
SR_int1to8
(* return by content if size is <= 8 *)
|
SR_ref
(* always return by assignment to a reference
given as extra argument *)
let
struct_passing_style
=
match
get_config_string
"struct_passing_style"
with
|
"ref-callee"
->
SP_ref_callee
|
"ref-caller"
->
SP_ref_caller
|
"ints"
->
SP_split_args
|
v
->
bad_config
"struct_passing_style"
[
v
]
let
struct_return_style
=
match
get_config_string
"struct_return_style"
with
|
"int1248"
->
SR_int1248
|
"int1-4"
->
SR_int1to4
|
"int1-8"
->
SR_int1to8
|
"ref"
->
SR_ref
|
v
->
bad_config
"struct_return_style"
[
v
]
type
response_file_style
=
|
Gnu
(* responsefiles in gnu compatible syntax *)
|
Diab
(* responsefiles in diab compatible syntax *)
...
...
driver/Configuration.mli
View file @
8cd40f0b
...
...
@@ -46,27 +46,6 @@ val has_runtime_lib: bool
val
has_standard_headers
:
bool
(** True if CompCert's standard header files is available. *)
type
struct_passing_style
=
|
SP_ref_callee
(* by reference, callee takes copy *)
|
SP_ref_caller
(* by reference, caller takes copy *)
|
SP_split_args
(* by value, as a sequence of ints *)
type
struct_return_style
=
|
SR_int1248
(* return by content if size is 1, 2, 4 or 8 bytes *)
|
SR_int1to4
(* return by content if size is <= 4 *)
|
SR_int1to8
(* return by content if size is <= 8 *)
|
SR_ref
(* always return by assignment to a reference
given as extra argument *)
val
struct_passing_style
:
struct_passing_style
(** Calling conventions to use for passing structs and unions as
first-class values *)
val
struct_return_style
:
struct_return_style
(** Calling conventions to use for returning structs and unions as
first-class values *)
type
response_file_style
=
|
Gnu
(* responsefiles in gnu compatible syntax *)
|
Diab
(* responsefiles in diab compatible syntax *)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment