diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml index 38d83deb0998fd6d36fffa862af9723ca19a8eaa..b4d47f81ac0787990bffa986236ff8311e10269c 100644 --- a/share/machdeps/machdep-schema.yaml +++ b/share/machdeps/machdep-schema.yaml @@ -136,6 +136,12 @@ has__builtin_va_list: type: boolean +host_name_max: + + description: expansion of 'HOST_NAME_MAX' POSIX macro + + type: string + int_fast8_t: description: definition of 'int_fast8_t' @@ -197,6 +203,12 @@ nsig: type: string +path_max: + + description: expansion of 'PATH_MAX' POSIX macro + + type: string + posix_version: description: | value of the macro '_POSIX_VERSION' @@ -304,6 +316,12 @@ tmp_max: type: string +tty_name_max: + + description: value of 'TTY_NAME_MAX' POSIX macro + + type: string + uint_fast8_t: description: definition of 'uint_fast8_t' diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml index 9d27004bf797a7b0212f9bf2675f0fc7d73cc285..31f2b2ee060324a50c9c701617402d1b7deecd72 100644 --- a/share/machdeps/machdep_avr_16.yaml +++ b/share/machdeps/machdep_avr_16.yaml @@ -141,6 +141,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: int int_fast32_t: int int_fast64_t: long long @@ -151,6 +152,7 @@ little_endian: true machdep_name: machdep_avr_16 mb_cur_max: ((size_t)16) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: int rand_max: '2147483647' @@ -169,6 +171,7 @@ sizeof_void: 1 ssize_t: int time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned int uint_fast32_t: unsigned int uint_fast64_t: unsigned long long diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml index 999181ba2de6423381fc81ccafb975f119461115..49022b0b99be09e9b897a25b8e65b5e1a822d293 100644 --- a/share/machdeps/machdep_gcc_x86_16.yaml +++ b/share/machdeps/machdep_gcc_x86_16.yaml @@ -172,6 +172,9 @@ bufsiz: '8192' eof: '(-1)' fopen_max: '16' filename_max: '2048' +path_max: '256' +host_name_max: '64' +tty_name_max: '32' l_tmpnam: '2048' tmp_max: '0xFFFFFFFF' rand_max: '32767' diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml index 53620c5a55d9a2df7d099dc9ddcfafc3f7493cdc..d474ec51725a67b1c91fe4ce4468e996a55aa1f0 100644 --- a/share/machdeps/machdep_gcc_x86_32.yaml +++ b/share/machdeps/machdep_gcc_x86_32.yaml @@ -139,6 +139,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: int int_fast32_t: int int_fast64_t: long long @@ -149,6 +150,7 @@ little_endian: true machdep_name: machdep_gcc_x86_32 mb_cur_max: ((size_t) 16 ) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: int rand_max: '2147483647' @@ -167,6 +169,7 @@ sizeof_void: 1 ssize_t: int time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned int uint_fast32_t: unsigned int uint_fast64_t: unsigned long long diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml index 762187987d19204e676c1f4495f040d42ffe365a..10ba75b7f1397b4c2d052ee916b8e3a3c1b0dea1 100644 --- a/share/machdeps/machdep_gcc_x86_64.yaml +++ b/share/machdeps/machdep_gcc_x86_64.yaml @@ -139,6 +139,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: long int_fast32_t: long int_fast64_t: long @@ -149,6 +150,7 @@ little_endian: true machdep_name: machdep_gcc_x86_64 mb_cur_max: ((size_t) 16 ) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: long rand_max: '2147483647' @@ -167,6 +169,7 @@ sizeof_void: 1 ssize_t: long time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned long uint_fast32_t: unsigned long uint_fast64_t: unsigned long diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml index 39aaae34bab110b374fe2808eed10f57f25e4b6b..fd6b258012059b960719e6523947b150aa707be6 100644 --- a/share/machdeps/machdep_msvc_x86_64.yaml +++ b/share/machdeps/machdep_msvc_x86_64.yaml @@ -134,6 +134,9 @@ posix_version: '' bufsiz: '8192' eof: '(-1)' fopen_max: '16' +host_name_max: '255' +path_max: '256' +tty_name_max: '32' filename_max: '2048' l_tmpnam: '20' tmp_max: '0xFFFFFFFF' diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml index 57d62e62f9bfd2426b4a9f6487fc4e19bb9489d3..a9dfce1010a52ee80cd1134b904263bd889e6233 100644 --- a/share/machdeps/machdep_ppc_32.yaml +++ b/share/machdeps/machdep_ppc_32.yaml @@ -141,6 +141,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: int int_fast32_t: int int_fast64_t: long long @@ -151,6 +152,7 @@ little_endian: false machdep_name: machdep_ppc_32 mb_cur_max: ((size_t)16) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: int rand_max: '2147483647' @@ -169,6 +171,7 @@ sizeof_void: 1 ssize_t: int time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned int uint_fast32_t: unsigned int uint_fast64_t: unsigned long long diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml index 5f90098938e0b6f584f3dc9604018e2f13432d53..00cd07f7ebfd890a74fc76537bf640d978382240 100644 --- a/share/machdeps/machdep_x86_16.yaml +++ b/share/machdeps/machdep_x86_16.yaml @@ -172,6 +172,9 @@ bufsiz: '8192' eof: '(-1)' fopen_max: '16' filename_max: '2048' +path_max: '256' +host_name_max: '64' +tty_name_max: '32' l_tmpnam: '2048' tmp_max: '0xFFFFFFFF' rand_max: '32767' diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml index 63513825a26e61f5717e3ccc4925c79e1925558f..d06c7f607bb03a326aade29e1484a89821bbab41 100644 --- a/share/machdeps/machdep_x86_32.yaml +++ b/share/machdeps/machdep_x86_32.yaml @@ -139,6 +139,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: int int_fast32_t: int int_fast64_t: long long @@ -149,6 +150,7 @@ little_endian: true machdep_name: machdep_x86_32 mb_cur_max: ((size_t) 16 ) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: int rand_max: '2147483647' @@ -167,6 +169,7 @@ sizeof_void: -1 ssize_t: int time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned int uint_fast32_t: unsigned int uint_fast64_t: unsigned long long diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml index 7852eb877a8e33f7454f963b27c611a741fce581..049407efe1bd55dde36914ae7fe57c12c77d8858 100644 --- a/share/machdeps/machdep_x86_64.yaml +++ b/share/machdeps/machdep_x86_64.yaml @@ -139,6 +139,7 @@ errno: filename_max: '4096' fopen_max: '16' has__builtin_va_list: true +host_name_max: '64' int_fast16_t: long int_fast32_t: long int_fast64_t: long @@ -149,6 +150,7 @@ little_endian: true machdep_name: machdep_x86_64 mb_cur_max: ((size_t) 16 ) nsig: (64 + 1) +path_max: '4096' posix_version: 200809L ptrdiff_t: long rand_max: '2147483647' @@ -167,6 +169,7 @@ sizeof_void: -1 ssize_t: long time_t: long tmp_max: '238328' +tty_name_max: '32' uint_fast16_t: unsigned long uint_fast32_t: unsigned long uint_fast64_t: unsigned long diff --git a/share/machdeps/make_machdep/limits_macros.c b/share/machdeps/make_machdep/limits_macros.c new file mode 100644 index 0000000000000000000000000000000000000000..fdef911d18e06251bb29a530f9d091a33a5cc054 --- /dev/null +++ b/share/machdeps/make_machdep/limits_macros.c @@ -0,0 +1,5 @@ +#include <limits.h> + +int path_max_is = PATH_MAX; +int tty_name_max_is = TTY_NAME_MAX; +int host_name_max_is = HOST_NAME_MAX; diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py index 8c49b8e495b2e3d2154dc1c2a5e32074ca175911..9f8dd0b3f7bebe7c9982ea9fc2aeeb94d90975f9 100755 --- a/share/machdeps/make_machdep/make_machdep.py +++ b/share/machdeps/make_machdep/make_machdep.py @@ -203,6 +203,7 @@ source_files = [ ("weof.c", "macro"), ("wordsize.c", "macro"), ("posix_version.c", "macro"), + ("limits_macros.c", "macro"), ("stdio_macros.c", "macro"), ("stdlib_macros.c", "macro"), ("nsig.c", "macro"), diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml index 127f612a11ebf2100dd0f4f560d1e2e3d5a4f8d4..8b6a81c693d4859666c2882ced19cc7b3e1b29df 100644 --- a/src/kernel_internals/runtime/machdep.ml +++ b/src/kernel_internals/runtime/machdep.ml @@ -272,6 +272,9 @@ let gen_all_defines fmt mach = gen_define_macro fmt "__FC_TMP_MAX" mach.tmp_max; gen_define_macro fmt "__FC_RAND_MAX" mach.rand_max; gen_define_macro fmt "__FC_MB_CUR_MAX" mach.mb_cur_max; + gen_define_macro fmt "__FC_PATH_MAX" mach.path_max; + gen_define_macro fmt "__FC_HOST_NAME_MAX" mach.host_name_max; + gen_define_macro fmt "__FC_TTY_NAME_MAX" mach.tty_name_max; List.iter (gen_define_errno_macro fmt) mach.errno; gen_define_macro fmt "__FC_TIME_T" mach.time_t; gen_define_macro fmt "__FC_NSIG" mach.nsig; diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml index 55986d1421ae90c05864b561a67c9c5d72a2094a..e1c9e7270e8c6adab7ead93d43edd65ebe2cbf55 100644 --- a/src/kernel_services/ast_data/cil_types.ml +++ b/src/kernel_services/ast_data/cil_types.ml @@ -1918,7 +1918,10 @@ type mach = { eof: string; (* expansion of EOF macro *) fopen_max: string; (* expansion of FOPEN_MAX macro *) filename_max: string; (* expansion of FILENAME_MAX macro *) + host_name_max: string; (* expansion of HOST_NAME_MAX macro *) + tty_name_max: string; (* expansion of TTY_NAME_MAX macro *) l_tmpnam: string; (* expansion of L_tmpnam macro *) + path_max: string; (* expansion of PATH_MAX macro *) tmp_max: string; (* expansion of TMP_MAX macro *) rand_max: string; (* expansion of RAND_MAX macro *) mb_cur_max: string; (* expansion of MB_CUR_MAX macro *) diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml index 80698e872333b3d78c8c0a3bcd63ecaf2dc0b617..35810382a3064e5dac0c362b78ba51fba0d4f5b2 100644 --- a/src/kernel_services/ast_queries/cil_datatype.ml +++ b/src/kernel_services/ast_queries/cil_datatype.ml @@ -2680,6 +2680,9 @@ let dummy_machdep = eof = "(-1)"; fopen_max = "255"; filename_max = "4095"; + path_max = "256"; + tty_name_max = "255"; + host_name_max = "255"; l_tmpnam = "63"; tmp_max = "1024"; rand_max = "0xFFFFFFFE"; diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index 3f8d916dac75ec90f93aac3df321ae6c3473ff3d..e9d681ce0af064f8407d6b716239ffdf9e42f063 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -398,7 +398,10 @@ type mach = Cil_types.mach = { eof: string; fopen_max: string; filename_max: string; + host_name_max: string; + tty_name_max: string; l_tmpnam: string; + path_max: string; tmp_max: string; rand_max: string; mb_cur_max: string; diff --git a/tests/builtins/oracle/realloc_multiple.0.res.oracle b/tests/builtins/oracle/realloc_multiple.0.res.oracle index 90a945812a66a13ef7723e9c41c1291ebedb8c47..5908db2b9e507a91de87ff057e31832be7b548e8 100644 --- a/tests/builtins/oracle/realloc_multiple.0.res.oracle +++ b/tests/builtins/oracle/realloc_multiple.0.res.oracle @@ -21,7 +21,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -56,7 +56,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -105,7 +105,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -142,7 +142,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -196,7 +196,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -238,7 +238,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -280,7 +280,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle index 831c3434213e54c9259aee81a7a24548c3d49be5..052f0f273fa2a1f63c42e4ef5be7fa27b6c5d044 100644 --- a/tests/builtins/oracle/realloc_multiple.1.res.oracle +++ b/tests/builtins/oracle/realloc_multiple.1.res.oracle @@ -29,7 +29,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -64,7 +64,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -95,7 +95,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -150,7 +150,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -187,7 +187,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -222,7 +222,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -280,7 +280,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -326,7 +326,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} @@ -368,7 +368,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} diff --git a/tests/builtins/oracle/strnlen.res.oracle b/tests/builtins/oracle/strnlen.res.oracle index 0853c554d1693daa487e1b60d57214326cceee9a..06fce1695a9043d52dd273ac7e84a54f3d19a130 100644 --- a/tests/builtins/oracle/strnlen.res.oracle +++ b/tests/builtins/oracle/strnlen.res.oracle @@ -37,7 +37,7 @@ # cvalue: __fc_heap_status ∈ [--..--] __fc_random_counter ∈ [--..--] - __fc_rand_max ∈ {32767} + __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} __fc_random48_counter[0..2] ∈ [--..--] __fc_p_random48_counter ∈ {{ &__fc_random48_counter[0] }} diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml index 974683a3127e067263f421bf5edbb834b5595dc4..5997c0388e3d4f7148c8fa10f67e1a3764660782 100644 --- a/tests/misc/custom_machdep.ml +++ b/tests/misc/custom_machdep.ml @@ -53,6 +53,9 @@ let mach = eof = "(-1)"; fopen_max = "128"; filename_max = "1023"; + path_max = "255"; + tty_name_max = "255"; + host_name_max = "255"; l_tmpnam = "255"; tmp_max = "4095"; rand_max = "0xFFFFFFFE"; diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml index 1fe7b404a4303ff226df04a6635ec877c825c100..1f6ef8d4b4ec055b30ca765ab0885417fa6f9a8a 100644 --- a/tests/misc/custom_machdep.yaml +++ b/tests/misc/custom_machdep.yaml @@ -49,6 +49,9 @@ fopen_max: '128' filename_max: '1023' l_tmpnam: '255' tmp_max: '255' +tty_name_max: '255' +host_name_max: '255' +path_max: '255' rand_max: '0xFFFFFE' mb_cur_max: '16' sig_atomic_t: int diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml index 66f8c989e2a92d2c79f6f42597ddcf8f039a489c..98030ed439835239d31f45aff0238f843986811f 100644 --- a/tests/syntax/machdep_char_unsigned.ml +++ b/tests/syntax/machdep_char_unsigned.ml @@ -51,6 +51,9 @@ let md = { bufsiz = "8192"; eof = "(-1)"; fopen_max = "16"; + host_name_max = "255"; + tty_name_max = "255"; + path_max = "255"; filename_max = "2048"; l_tmpnam = "2048"; tmp_max = "0xFFFFFFFF";