[machdep] support for time_t in new machdep

share/machdeps/machdep-schema.yaml

@@ -238,6 +238,12 @@ ssize_t:
 
   type: string
 
+time_t:
+
+  description: definition of 'time_t' (in time.h)
+
+  type: string
+
 tmp_max:
 
   description: value of 'TMP_MAX' macro

share/machdeps/machdep_avr_16.yaml

@@ -40,6 +40,7 @@ sizeof_ptr: 2
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: int
+time_t: long
 tmp_max: '238328'
 uintptr_t: unsigned int
 version: clang version 15.0.7

share/machdeps/machdep_gcc_x86_16.yaml

@@ -30,6 +30,7 @@ sizeof_ptr: 4
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: int
+time_t: long
 uintptr_t: unsigned long
 version: none
 wchar_t: int

share/machdeps/machdep_gcc_x86_32.yaml

@@ -38,6 +38,7 @@ sizeof_ptr: 4
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: int
+time_t: long
 tmp_max: '238328'
 uintptr_t: unsigned int
 version: gcc (GCC) 12.2.1 20230201

share/machdeps/machdep_gcc_x86_64.yaml

@@ -38,6 +38,7 @@ sizeof_ptr: 8
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: long
+time_t: long
 tmp_max: '238328'
 uintptr_t: unsigned long
 version: gcc (GCC) 12.2.1 20230201

share/machdeps/machdep_msvc_x86_64.yaml

@@ -31,6 +31,7 @@ sizeof_ptr: 8
 sizeof_short: 2
 sizeof_void: 0
 ssize_t: long long
+time_t: long long
 uintptr_t: unsigned long long
 version: MSVC - X86-64bits mode
 wchar_t: unsigned short

share/machdeps/machdep_ppc_32.yaml

@@ -40,6 +40,7 @@ sizeof_ptr: 4
 sizeof_short: 2
 sizeof_void: 1
 ssize_t: int
+time_t: long
 tmp_max: '238328'
 uintptr_t: unsigned int
 version: clang version 15.0.7

share/machdeps/machdep_x86_16.yaml

@@ -30,6 +30,7 @@ sizeof_ptr: 4
 sizeof_short: 2
 sizeof_void: -1
 ssize_t: int
+time_t: long
 uintptr_t: unsigned long
 version: none
 wchar_t: int

share/machdeps/machdep_x86_32.yaml

@@ -38,6 +38,7 @@ sizeof_ptr: 4
 sizeof_short: 2
 sizeof_void: -1
 ssize_t: int
+time_t: long
 tmp_max: '238328'
 uintptr_t: unsigned int
 version: gcc (GCC) 12.2.1 20230201

share/machdeps/machdep_x86_64.yaml

@@ -38,6 +38,7 @@ sizeof_ptr: 8
 sizeof_short: 2
 sizeof_void: -1
 ssize_t: long
+time_t: long
 tmp_max: '238328'
 uintptr_t: unsigned long
 version: gcc (GCC) 12.2.1 20230201

share/machdeps/make_machdep/make_machdep.py

@@ -173,6 +173,7 @@ source_files = [
     ("uintptr_t.c", "type"),
     ("wint_t.c", "type"),
     ("sig_atomic_t.c", "type"),
+    ("time_t.c", "type"),
     ("char_is_unsigned.c", "bool"),
     ("little_endian.c", "bool"),
     ("has__builtin_va_list.c", "has__builtin_va_list"),

share/machdeps/make_machdep/time_t.c

+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2023                                               */
+/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
+/*         alternatives)                                                  */
+/*                                                                        */
+/*  you can redistribute it and/or modify it under the terms of the GNU   */
+/*  Lesser General Public License as published by the Free Software       */
+/*  Foundation, version 2.1.                                              */
+/*                                                                        */
+/*  It 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.  See the         */
+/*  GNU Lesser General Public License for more details.                   */
+/*                                                                        */
+/*  See the GNU Lesser General Public License version 2.1                 */
+/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
+/*                                                                        */
+/**************************************************************************/
+
+#include "make_machdep_common.h"
+#include <time.h>
+
+#define TEST_TYPE time_t
+
+TEST_TYPE_IS(unsigned int)
+TEST_TYPE_IS(int)
+TEST_TYPE_IS(unsigned long)
+TEST_TYPE_IS(long)
+TEST_TYPE_IS(unsigned long long)
+TEST_TYPE_IS(long long)
+
+// Technically, C standard speaks of a 'real' type, not an 'integer' one
+
+TEST_TYPE_IS(float)
+TEST_TYPE_IS(double)
+TEST_TYPE_IS(long double)

src/kernel_internals/runtime/machdep.ml

@@ -246,7 +246,7 @@ let gen_all_defines fmt mach =
   gen_define_macro fmt "__FC_RAND_MAX" mach.rand_max;
   gen_define_macro fmt "__FC_MB_CUR_MAX" mach.mb_cur_max;
   (* TODO: __FC_E*, errno enumeration *)
-  (* TODO: __FC_TIME_T *)
+  gen_define_macro fmt "__FC_TIME_T" mach.time_t;
   (* TODO: __FC_NSIG *)
   (* TODO: __FC__NSIG *)
   (* TODO: gcc builtins *)

src/kernel_services/ast_data/cil_types.ml

@@ -1883,6 +1883,7 @@ type mach = {
   uintptr_t: string;      (* Type of "uintptr_t" *)
   wint_t: string;          (* Type of "wint_t" *)
   sig_atomic_t: string;   (* Type of "sig_atomic_t" *)
+  time_t: string;          (* Type of "time_t" *)
   alignof_short: int;     (* Alignment of "short" *)
   alignof_int: int;       (* Alignment of "int" *)
   alignof_long: int;      (* Alignment of "long" *)

src/kernel_services/ast_queries/cil_datatype.ml

@@ -2647,6 +2647,7 @@ let dummy_machdep =
     uintptr_t = "unsigned long";      (* Type of "uintptr_t" *)
     wint_t = "int";
     sig_atomic_t = "int";
+    time_t = "long";
     alignof_short = 2;
     alignof_int = 4;
     alignof_long = 8;

tests/misc/custom_machdep.ml

@@ -23,6 +23,7 @@ let mach =
     wchar_t = "int";
     ptrdiff_t = "int";
     sig_atomic_t = "int";
+    time_t = "long";
     alignof_short = 2;
     alignof_int = 3;
     alignof_long = 4;

tests/misc/custom_machdep.yaml

@@ -44,3 +44,4 @@ tmp_max: '255'
 rand_max: '0xFFFFFE'
 mb_cur_max: 16
 sig_atomic_t: int
+time_t: long

tests/syntax/machdep_char_unsigned.ml

@@ -35,6 +35,7 @@ let md = {
   ptrdiff_t = "int";
   wint_t = "long";
   sig_atomic_t = "int";
+  time_t = "long";
   has__builtin_va_list = true;
   weof = "(-1L)";
   wordsize = "16";