From 4cf2fc41657fac51d806c14fdf481c7047e39df3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Jul 2020 10:38:18 +0200 Subject: Add support for __builtin_fabsf --- cfrontend/C2C.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 7f796fe3..75eeaf21 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -183,6 +183,8 @@ let builtins_generic = { (* Floating-point absolute value *) "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + "__builtin_fabsf", + (TFloat(FFloat, []), [TFloat(FFloat, [])], false); (* Float arithmetic *) "__builtin_fsqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); -- cgit From bc20d7c0d16d07790fb6eb608bf608237b0abbc3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Jul 2020 17:47:25 +0200 Subject: Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml These functions are now available on all targets. --- cfrontend/C2C.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 75eeaf21..c7cd4937 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -180,6 +180,18 @@ let builtins_generic = { (TInt(IUInt, []), [TInt(IUInt, [])], false); "__builtin_bswap16", (TInt(IUShort, []), [TInt(IUShort, [])], false); + "__builtin_clz", + (TInt(IInt, []), [TInt(IUInt, [])], false); + "__builtin_clzl", + (TInt(IInt, []), [TInt(IULong, [])], false); + "__builtin_clzll", + (TInt(IInt, []), [TInt(IULongLong, [])], false); + "__builtin_ctz", + (TInt(IInt, []), [TInt(IUInt, [])], false); + "__builtin_ctzl", + (TInt(IInt, []), [TInt(IULong, [])], false); + "__builtin_ctzll", + (TInt(IInt, []), [TInt(IULongLong, [])], false); (* Floating-point absolute value *) "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); -- cgit From 77ce8ba291afa9f5629a160df440f9af6614f3ef Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 27 Jul 2020 09:54:00 +0200 Subject: Add __builtin_sqrt as synonymous for __builtin_fsqrt __builtin_sqrt (no "f") is the name used by GCC and Clang. --- cfrontend/C2C.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c7cd4937..2386eed9 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -200,6 +200,8 @@ let builtins_generic = { (* Float arithmetic *) "__builtin_fsqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + "__builtin_sqrt", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); (* Block copy *) "__builtin_memcpy_aligned", (TVoid [], -- cgit From b1b853a2e9f7f2143fedd58772a702bc9c6a8ba1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 30 Oct 2020 18:32:04 +0100 Subject: Add -main option to specify entrypoint function in interpreter mode (#374) When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0. --- cfrontend/C2C.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 2386eed9..ef028255 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1495,7 +1495,7 @@ let convertProgram p = let p' = { prog_defs = gl2; prog_public = public_globals gl2; - prog_main = intern_string "main"; + prog_main = intern_string !Clflags.main_function_name; prog_types = typs; prog_comp_env = ce } in Diagnostics.check_errors (); -- cgit