Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

8 files changed, 389 insertions, 0 deletions

diff --git a/test/monniaux/BearSSL/conf/Kalray.mk b/test/monniaux/BearSSL/conf/Kalray.mk
new file mode 100644
index 00000000..6359edd1
--- /dev/null
+++ b/test/monniaux/BearSSL/conf/Kalray.mk
@@ -0,0 +1,69 @@
+# Configuration for a native build on a generic Unix-like system.
+
+# Build directory.
+BUILD = build
+
+# Extension for executable files.
+E =
+
+# Extension for object files.
+O = .o
+
+# Prefix for library file name.
+LP = lib
+
+# Extension for library file name.
+L = .a
+
+# Prefix for DLL file name.
+DP = lib
+
+# Extension for DLL file name.
+D = .so
+
+# Output file names can be overridden directly. By default, they are
+# assembled using the prefix/extension macros defined above.
+# BEARSSLLIB = libbearssl.a
+# BEARSSLDLL = libbearssl.so
+# BRSSL = brssl
+# TESTCRYPTO = testcrypto
+# TESTSPEED = testspeed
+# TESTX509 = testx509
+
+# File deletion tool.
+RM = rm -f
+
+# Directory creation tool.
+MKDIR = mkdir -p
+
+# C compiler and flags.
+CC = k1-cos-gcc
+CFLAGS = -W -Wall -O3
+CCOUT = -c -o 
+
+# Static library building tool.
+AR = ar
+ARFLAGS = -rcs
+AROUT =
+
+# DLL building tool.
+LDDLL = $(CC)
+LDDLLFLAGS = -shared
+LDDLLOUT = -o 
+
+# Static linker.
+LD = $(CC)
+LDFLAGS = 
+LDOUT = -o 
+
+# C# compiler; we assume usage of Mono.
+MKT0COMP = mk$PmkT0.sh
+RUNT0COMP = mono T0Comp.exe
+
+# Set the values to 'no' to disable building of the corresponding element
+# by default. Building can still be invoked with an explicit target call
+# (e.g. 'make dll' to force build the DLL).
+#STATICLIB = no
+DLL = no
+TOOLS = no
+#TESTS = no
diff --git a/test/monniaux/BearSSL/conf/KalrayCompCert.mk b/test/monniaux/BearSSL/conf/KalrayCompCert.mk
new file mode 100644
index 00000000..9b34eed2
--- /dev/null
+++ b/test/monniaux/BearSSL/conf/KalrayCompCert.mk
@@ -0,0 +1,69 @@
+# Configuration for a native build on a generic Unix-like system.
+
+# Build directory.
+BUILD = build
+
+# Extension for executable files.
+E =
+
+# Extension for object files.
+O = .o
+
+# Prefix for library file name.
+LP = lib
+
+# Extension for library file name.
+L = .a
+
+# Prefix for DLL file name.
+DP = lib
+
+# Extension for DLL file name.
+D = .so
+
+# Output file names can be overridden directly. By default, they are
+# assembled using the prefix/extension macros defined above.
+# BEARSSLLIB = libbearssl.a
+# BEARSSLDLL = libbearssl.so
+# BRSSL = brssl
+# TESTCRYPTO = testcrypto
+# TESTSPEED = testspeed
+# TESTX509 = testx509
+
+# File deletion tool.
+RM = rm -f
+
+# Directory creation tool.
+MKDIR = mkdir -p
+
+# C compiler and flags.
+CC = ../../../ccomp -fstruct-passing -fpostpass= ilp -U__SIZEOF_INT128__ -U__SIZEOF_FLOAT128__
+CFLAGS = -W -Wall -Wno-c11-extensions -O3 -D_POSIX_C_SOURCE=200909L
+CCOUT = -c -o 
+
+# Static library building tool.
+AR = ar
+ARFLAGS = -rcs
+AROUT =
+
+# DLL building tool.
+LDDLL = cc
+LDDLLFLAGS = -shared
+LDDLLOUT = -o 
+
+# Static linker.
+LD = $(CC)
+LDFLAGS = ../clock.gcc.k1c.o
+LDOUT = -o 
+
+# C# compiler; we assume usage of Mono.
+MKT0COMP = mk$PmkT0.sh
+RUNT0COMP = mono T0Comp.exe
+
+# Set the values to 'no' to disable building of the corresponding element
+# by default. Building can still be invoked with an explicit target call
+# (e.g. 'make dll' to force build the DLL).
+#STATICLIB = no
+DLL = no
+#TOOLS = no
+#TESTS = no
diff --git a/test/monniaux/BearSSL/conf/Unix.mk b/test/monniaux/BearSSL/conf/Unix.mk
new file mode 100644
index 00000000..02f2b2be
--- /dev/null
+++ b/test/monniaux/BearSSL/conf/Unix.mk
@@ -0,0 +1,69 @@
+# Configuration for a native build on a generic Unix-like system.
+
+# Build directory.
+BUILD = build
+
+# Extension for executable files.
+E =
+
+# Extension for object files.
+O = .o
+
+# Prefix for library file name.
+LP = lib
+
+# Extension for library file name.
+L = .a
+
+# Prefix for DLL file name.
+DP = lib
+
+# Extension for DLL file name.
+D = .so
+
+# Output file names can be overridden directly. By default, they are
+# assembled using the prefix/extension macros defined above.
+# BEARSSLLIB = libbearssl.a
+# BEARSSLDLL = libbearssl.so
+# BRSSL = brssl
+# TESTCRYPTO = testcrypto
+# TESTSPEED = testspeed
+# TESTX509 = testx509
+
+# File deletion tool.
+RM = rm -f
+
+# Directory creation tool.
+MKDIR = mkdir -p
+
+# C compiler and flags.
+CC = cc
+CFLAGS = -W -Wall -Os -fPIC
+CCOUT = -c -o 
+
+# Static library building tool.
+AR = ar
+ARFLAGS = -rcs
+AROUT =
+
+# DLL building tool.
+LDDLL = cc
+LDDLLFLAGS = -shared
+LDDLLOUT = -o 
+
+# Static linker.
+LD = cc
+LDFLAGS = 
+LDOUT = -o 
+
+# C# compiler; we assume usage of Mono.
+MKT0COMP = mk$PmkT0.sh
+RUNT0COMP = mono T0Comp.exe
+
+# Set the values to 'no' to disable building of the corresponding element
+# by default. Building can still be invoked with an explicit target call
+# (e.g. 'make dll' to force build the DLL).
+#STATICLIB = no
+#DLL = no
+#TOOLS = no
+#TESTS = no
diff --git a/test/monniaux/BearSSL/conf/Unix32.mk b/test/monniaux/BearSSL/conf/Unix32.mk
new file mode 100644
index 00000000..0d3bed88
--- /dev/null
+++ b/test/monniaux/BearSSL/conf/Unix32.mk
@@ -0,0 +1,12 @@
+# Example configuration file for compiling on a Unix-like system with
+# GCC, targeting a 32-bit output. Moreover, it enables the "LOMUL" setting
+# to make the code select the "small" integer implementations (i15, m15,
+# ctmul32...), which is not necessarily a good idea for performance, but
+# handy for tests.
+
+include conf/Unix.mk
+
+BUILD = build32
+CFLAGS = -W -Wall -Os -fPIC -m32 -DBR_LOMUL
+LDFLAGS = -m32
+LDDLLFLAGS = -shared -m32
diff --git a/test/monniaux/BearSSL/conf/UnixClang.mk b/test/monniaux/BearSSL/conf/UnixClang.mk
new file mode 100644
index 00000000..3636cf89
--- /dev/null
+++ b/test/monniaux/BearSSL/conf/UnixClang.mk
@@ -0,0 +1,11 @@
+# Example configuration file for compiling on a Unix-like system with
+# clang as compiler instead of gcc.
+
+# We are on a Unix system so we assume a Single Unix compatible 'make'
+# utility, and Unix defaults.
+include conf/Unix.mk
+
+BUILD = bclang
+CC = clang
+LD = clang
+LDDLL = clang
diff --git a/test/monniaux/BearSSL/conf/UnixCompCert.mk b/test/monniaux/BearSSL/conf/UnixCompCert.mk
new file mode 100644
index 00000000..fefb2938
--- /dev/null
+++ b/test/monniaux/BearSSL/conf/UnixCompCert.mk
@@ -0,0 +1,69 @@
+# Configuration for a native build on a generic Unix-like system.
+
+# Build directory.
+BUILD = build
+
+# Extension for executable files.
+E =
+
+# Extension for object files.
+O = .o
+
+# Prefix for library file name.
+LP = lib
+
+# Extension for library file name.
+L = .a
+
+# Prefix for DLL file name.
+DP = lib
+
+# Extension for DLL file name.
+D = .so
+
+# Output file names can be overridden directly. By default, they are
+# assembled using the prefix/extension macros defined above.
+# BEARSSLLIB = libbearssl.a
+# BEARSSLDLL = libbearssl.so
+# BRSSL = brssl
+# TESTCRYPTO = testcrypto
+# TESTSPEED = testspeed
+# TESTX509 = testx509
+
+# File deletion tool.
+RM = rm -f
+
+# Directory creation tool.
+MKDIR = mkdir -p
+
+# C compiler and flags.
+CC = /opt/CompCert/3.4/x86_64-linux/bin/ccomp
+CFLAGS = -W -Wall -O3 -D_POSIX_C_SOURCE=200909L -U__SIZEOF_INT128__ -U__SIZEOF_FLOAT128__ -fstruct-passing
+CCOUT = -c -o 
+
+# Static library building tool.
+AR = ar
+ARFLAGS = -rcs
+AROUT =
+
+# DLL building tool.
+LDDLL = cc
+LDDLLFLAGS = -shared
+LDDLLOUT = -o 
+
+# Static linker.
+LD = $(CC)
+LDFLAGS = 
+LDOUT = -o 
+
+# C# compiler; we assume usage of Mono.
+MKT0COMP = mk$PmkT0.sh
+RUNT0COMP = mono T0Comp.exe
+
+# Set the values to 'no' to disable building of the corresponding element
+# by default. Building can still be invoked with an explicit target call
+# (e.g. 'make dll' to force build the DLL).
+#STATICLIB = no
+DLL = no
+#TOOLS = no
+#TESTS = no
diff --git a/test/monniaux/BearSSL/conf/Win.mk b/test/monniaux/BearSSL/conf/Win.mk
new file mode 100644
index 00000000..2ed4bb68
--- /dev/null
+++ b/test/monniaux/BearSSL/conf/Win.mk
@@ -0,0 +1,70 @@
+# Configuration for a native build on a Windows system with Visual Studio.
+
+# Build directory.
+BUILD = build
+
+# Extension for executable files.
+E = .exe
+
+# Extension for object files.
+O = .obj
+
+# Prefix for static library file name.
+LP =
+
+# Extension for static library file name. We add an 's' so that the
+# name is distinct from the 'import library' generated along with the DLL.
+L = s.lib
+
+# Prefix for DLL file name.
+DP =
+
+# Extension for DLL file name.
+D = .dll
+
+# Output file names can be overridden directly. By default, they are
+# assembled using the prefix/extension macros defined above.
+# BEARSSLLIB = bearssls.lib
+# BEARSSLDLL = bearssl.dll
+# BRSSL = brssl.exe
+# TESTCRYPTO = testcrypto.exe
+# TESTSPEED = testspeed.exe
+# TESTX509 = testx509.exe
+
+# File deletion tool.
+RM = del /Q
+
+# Directory creation tool.
+MKDIR = mkdir
+
+# C compiler and flags.
+CC = cl
+CFLAGS = -nologo -W2 -O2
+CCOUT = -c -Fo
+
+# Static library building tool.
+AR = lib
+ARFLAGS = -nologo
+AROUT = -out:
+
+# DLL building tool.
+LDDLL = cl
+LDDLLFLAGS = -nologo -LD -MT
+LDDLLOUT = -Fe
+
+# Static linker.
+LD = cl
+LDFLAGS = -nologo
+LDOUT = -Fe
+
+# C# compiler.
+MKT0COMP = mk$PmkT0.cmd
+RUNT0COMP = T0Comp.exe
+
+# Set the values to 'no' to disable building of the corresponding element
+# by default. Building can still be invoked with an explicit target call
+# (e.g. 'make dll' to force build the DLL).
+#STATICLIB = no
+#DLL = no
+#TOOLS = no
+#TESTS = no
diff --git a/test/monniaux/BearSSL/conf/samd20.mk b/test/monniaux/BearSSL/conf/samd20.mk
new file mode 100644
index 00000000..5b3d5004
--- /dev/null
+++ b/test/monniaux/BearSSL/conf/samd20.mk
@@ -0,0 +1,20 @@
+# Example configuration file for compiling for an Atmel SAM D20 Xplained
+# Pro evaluation kit, on a Unix-like system, with a GNU toolchain.
+
+# We are on a Unix system so we assume a Single Unix compatible 'make'
+# utility, and Unix defaults.
+include conf/Unix.mk
+
+# We override the build directory.
+BUILD = samd20
+
+# C compiler, linker, and static library builder.
+CC = arm-none-eabi-gcc
+CFLAGS = -W -Wall -Os -mthumb -ffunction-sections -fdata-sections -mcpu=cortex-m0plus -DBR_ARMEL_CORTEXM_GCC
+LD = arm-none-eabi-gcc
+AR = arm-none-eabi-ar
+
+# We compile only the static library.
+DLL = no
+TOOLS = no
+TESTS = no