Merge branch 'new/mbedtls' into 'master'

add mbedtls as case study

See merge request !44

frama-c @ 49876062

-Subproject commit 0da5b24c3e274f126b893a072d9bb6bb440199fa
+Subproject commit 498760623a093ddbed2722fc7001e82df46689ad

mbedtls/.frama-c/fc_stubs.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).            */
+/*                                                                        */
+/**************************************************************************/
+
+// Stub for a main function which reads arguments from the command line, to be
+// used by the Eva plug-in.
+// This stub emulates non-deterministic input of up to 5 arguments, each up
+// to 256 characters long. This is sufficient to ensure arbitrary input in
+// virtually every case.
+// Do not forget to add option '-main eva_main' in order to use this stub.
+
+#ifdef __FRAMAC__
+#include "__fc_builtin.h"
+#include <stdint.h>
+
+int main(int, char **);
+static volatile int nondet;
+int eva_main() {
+  int argc = Frama_C_interval(0, 5);
+  char argv0[256], argv1[256], argv2[256], argv3[256], argv4[256];
+  char *argv[6] = {argv0, argv1, argv2, argv3, argv4, 0};
+  //@ loop unroll 5;
+  for (int i = 0; i < 5; i++) {
+    Frama_C_make_unknown(argv[i], 255);
+    argv[i][255] = 0;
+  }
+  return main(argc, argv);
+}
+
+/*@ assigns \result \from x; */
+uint32_t __builtin_bswap32(uint32_t x);
+
+#endif // __FRAMAC__

mbedtls/.frama-c/path.mk

+../../path.mk
\ No newline at end of file

mbedtls/.frama-c/test_256.c

+#include "mbedtls/sha256.h"
+
+#define LEN 128
+
+/*@ assigns \result \from x; */
+uint32_t __builtin_bswap32(uint32_t x);
+
+extern unsigned char inbuf[LEN];
+
+extern unsigned char outbuf[32];
+
+int main() {
+  mbedtls_sha256_context ctx;
+  mbedtls_sha256_init(&ctx);
+  mbedtls_sha256_starts(&ctx,0);
+  mbedtls_sha256_update(&ctx,inbuf,LEN);
+  mbedtls_sha256_finish(&ctx,outbuf);
+  mbedtls_sha256_free(&ctx);
+}

mbedtls/.gitattributes

+# Classify all '.function' files as C for syntax highlighting purposes
+*.function linguist-language=C

mbedtls/.github/ISSUE_TEMPLATE/bug_report.md

+---
+name: Bug report
+about: To report a bug, please fill this form.
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+### Summary
+
+
+
+### System information
+
+Mbed TLS version (number or commit id): 
+Operating system and version: 
+Configuration (if not default, please attach `mbedtls_config.h`): 
+Compiler and options (if you used a pre-built binary, please indicate how you obtained it): 
+Additional environment information: 
+
+### Expected behavior
+
+
+
+### Actual behavior
+
+
+
+### Steps to reproduce
+
+
+
+### Additional information
+

mbedtls/.github/ISSUE_TEMPLATE/config.yml

+blank_issues_enabled: false
+contact_links:
+    - name: Mbed TLS security team
+      url: mailto:mbed-tls-security@lists.trustedfirmware.org
+      about: Report a security vulnerability.
+    - name: Mbed TLS mailing list
+      url: https://lists.trustedfirmware.org/mailman3/lists/mbed-tls.lists.trustedfirmware.org
+      about: Mbed TLS community support and general discussion.

mbedtls/.github/ISSUE_TEMPLATE/feature_request.md

+---
+name: Enhancement request
+about: To request an enhancement, please fill this form.
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+### Suggested enhancement
+
+
+
+### Justification
+
+Mbed TLS needs this because 
+

mbedtls/.github/pull_request_template.md

+## Description
+
+Please write a few sentences describing the overall goals of the pull request's commits.
+
+
+
+## Gatekeeper checklist
+
+- [ ] **changelog** provided, or not required
+- [ ] **backport** done, or not required
+- [ ] **tests** provided, or not required
+
+
+
+## Notes for the submitter
+
+Please refer to the [contributing guidelines](https://github.com/Mbed-TLS/mbedtls/blob/development/CONTRIBUTING.md), especially the
+checklist for PR contributors.
+

mbedtls/.gitignore

+# Random seed file created by test scripts and sample programs
+seedfile
+
+# CMake build artifacts:
+CMakeCache.txt
+CMakeFiles
+CTestTestfile.cmake
+cmake_install.cmake
+Testing
+# CMake generates *.dir/ folders for in-tree builds (used by MSVC projects), ignore all of those:
+*.dir/
+# MSVC files generated by CMake:
+/*.sln
+/*.vcxproj
+/*.filters
+
+# Test coverage build artifacts:
+Coverage
+*.gcno
+*.gcda
+coverage-summary.txt
+
+# generated by scripts/memory.sh
+massif-*
+
+# Eclipse project files
+.cproject
+.project
+/.settings
+
+# MSVC build artifacts:
+*.exe
+*.pdb
+*.ilk
+*.lib
+
+# Python build artifacts:
+*.pyc
+
+# CMake generates *.dir/ folders for in-tree builds (used by MSVC projects), ignore all of those:
+*.dir/
+
+# Microsoft CMake extension for Visual Studio Code generates a build directory by default
+/build/
+
+# Generated documentation:
+/apidoc
+
+# PSA Crypto compliance test repo, cloned by test_psa_compliance.py
+/psa-arch-tests
+
+# Editor navigation files:
+/GPATH
+/GRTAGS
+/GSYMS
+/GTAGS
+/TAGS
+/cscope*.out
+/tags

mbedtls/.globalrc

+default:\
+    :langmap=c\:.c.h.function:\
+

mbedtls/.mypy.ini

+[mypy]
+mypy_path = scripts
+namespace_packages = True
+warn_unused_configs = True

mbedtls/.pylintrc

+[MASTER]
+init-hook='import sys; sys.path.append("scripts")'
+min-similarity-lines=10
+
+[BASIC]
+# We're ok with short funtion argument names.
+# [invalid-name]
+argument-rgx=[a-z_][a-z0-9_]*$
+
+# Allow filter and map.
+# [bad-builtin]
+bad-functions=input
+
+# We prefer docstrings, but we don't require them on all functions.
+# Require them only on long functions (for some value of long).
+# [missing-docstring]
+docstring-min-length=10
+
+# No upper limit on method names. Pylint <2.1.0 has an upper limit of 30.
+# [invalid-name]
+method-rgx=[a-z_][a-z0-9_]{2,}$
+
+# Allow module names containing a dash (but no underscore or uppercase letter).
+# They are whole programs, not meant to be included by another module.
+# [invalid-name]
+module-rgx=(([a-z_][a-z0-9_]*)|([A-Z][a-zA-Z0-9]+)|[a-z][-0-9a-z]+)$
+
+# Some functions don't need docstrings.
+# [missing-docstring]
+no-docstring-rgx=(run_)?main$
+
+# We're ok with short local or global variable names.
+# [invalid-name]
+variable-rgx=[a-z_][a-z0-9_]*$
+
+[DESIGN]
+# Allow more than the default 7 attributes.
+# [too-many-instance-attributes]
+max-attributes=15
+
+[FORMAT]
+# Allow longer modules than the default recommended maximum.
+# [too-many-lines]
+max-module-lines=2000
+
+[MESSAGES CONTROL]
+# * locally-disabled, locally-enabled: If we disable or enable a message
+#   locally, it's by design. There's no need to clutter the Pylint output
+#   with this information.
+# * logging-format-interpolation: Pylint warns about things like
+#   ``log.info('...'.format(...))``. It insists on ``log.info('...', ...)``.
+#   This is of minor utility (mainly a performance gain when there are
+#   many messages that use formatting and are below the log level).
+#   Some versions of Pylint (including 1.8, which is the version on
+#   Ubuntu 18.04) only recognize old-style format strings using '%',
+#   and complain about something like ``log.info('{}', foo)`` with
+#   logging-too-many-args (Pylint supports new-style formatting if
+#   declared globally with logging_format_style under [LOGGING] but
+#   this requires Pylint >=2.2).
+# * no-else-return: Allow the perfectly reasonable idiom
+#    if condition1:
+#        return value1
+#    else:
+#        return value2
+# * unnecessary-pass: If we take the trouble of adding a line with "pass",
+#   it's because we think the code is clearer that way.
+disable=locally-disabled,locally-enabled,logging-format-interpolation,no-else-return,unnecessary-pass
+
+[REPORTS]
+# Don't diplay statistics. Just the facts.
+reports=no
+
+[VARIABLES]
+# Allow unused variables if their name starts with an underscore.
+# [unused-argument]
+dummy-variables-rgx=_.*
+
+[SIMILARITIES]
+# Ignore imports when computing similarities.
+ignore-imports=yes

mbedtls/.travis.yml

+# Declare python as our language. This way we get our chosen Python version,
+# and pip is available. Gcc and clang are available anyway.
+language: python
+python: 3.5
+sudo: false
+cache: ccache
+
+jobs:
+  include:
+    - name: basic checks and reference configurations
+      addons:
+        apt:
+          packages:
+          - gnutls-bin
+          - doxygen
+          - graphviz
+          - gcc-arm-none-eabi
+          - libnewlib-arm-none-eabi
+          - gcc-arm-linux-gnueabi
+          - libc6-dev-armel-cross
+      script:
+        - tests/scripts/all.sh -k 'check_*'
+        - tests/scripts/all.sh -k test_default_out_of_box
+        - tests/scripts/all.sh -k test_ref_configs
+        - tests/scripts/all.sh -k build_arm_linux_gnueabi_gcc_arm5vte build_arm_none_eabi_gcc_m0plus
+
+    - name: full configuration
+      os: linux
+      dist: focal
+      addons:
+        apt:
+          packages:
+          - clang-10
+          - gnutls-bin
+      script:
+        # Do a manual build+test sequence rather than using all.sh,
+        # because there's no all.sh component that does what we want,
+        # which is a build with Clang >= 10 and ASan, running all the SSL
+        # testing.
+        #   - The clang executable in the default PATH is Clang 7 on
+        #     Travis's focal instances, but we want Clang >= 10.
+        #   - Running all the SSL testing requires a specific set of
+        #     OpenSSL and GnuTLS versions and we don't want to bother
+        #     with those on Travis.
+        # So we explicitly select clang-10 as the compiler, and we
+        # have ad hoc restrictions on SSL testing based on what is
+        # passing at the time of writing. We will remove these limitations
+        # gradually.
+        - make generated_files
+        - make CC=clang-10 CFLAGS='-Werror -Wall -Wextra -fsanitize=address,undefined -fno-sanitize-recover=all -O2' LDFLAGS='-Werror -Wall -Wextra -fsanitize=address,undefined -fno-sanitize-recover=all'
+        - make test
+        - programs/test/selftest
+        - tests/scripts/test_psa_constant_names.py
+        - tests/ssl-opt.sh
+        # Modern OpenSSL does not support null ciphers.
+        - tests/compat.sh -p OpenSSL -e 'NULL'
+        - tests/scripts/travis-log-failure.sh
+        # GnuTLS supports CAMELLIA but compat.sh doesn't properly enable it.
+        - tests/compat.sh -p GnuTLS -e 'CAMELLIA'
+        - tests/scripts/travis-log-failure.sh
+        - tests/context-info.sh
+
+    - name: Windows
+      os: windows
+      # The language 'python' is currently unsupported on the
+      # Windows Build Environment. And 'generic' causes the job to get stuck
+      # on "Booting virtual machine".
+      language: c
+      before_install:
+        - choco install python --version=3.5.4
+      env:
+        # Add the directory where the Choco packages go
+        - PATH=/c/Python35:/c/Python35/Scripts:$PATH
+        - PYTHON=python.exe
+      script:
+        - type perl; perl --version
+        - type python; python --version
+        - scripts/make_generated_files.bat
+        # Logs appear out of sequence on Windows. Give time to catch up.
+        - sleep 5
+        - scripts/windows_msbuild.bat v141 # Visual Studio 2017
+        - visualc/VS2013/x64/Release/selftest.exe
+
+    - name: full configuration on arm64
+      os: linux
+      dist: focal
+      arch: arm64
+      addons:
+        apt:
+          packages:
+          - gcc
+      script:
+        # Do a manual build+test sequence rather than using all.sh.
+        #
+        # On Arm64 host of Travis CI, the time of `test_full_cmake_*` exceeds
+        # limitation of Travis CI. Base on `test_full_cmake_*`, we removed
+        # `ssl-opt.sh` and GnuTLS compat.sh here to meet the time limitation.
+        - scripts/config.py full
+        - make generated_files
+        - make CFLAGS='-O3 -Werror -fsanitize=address,undefined -fno-sanitize-recover=all' LDFLAGS='-Werror -fsanitize=address,undefined -fno-sanitize-recover=all'
+        - make test
+        - programs/test/selftest
+        - tests/scripts/test_psa_constant_names.py
+        # Modern OpenSSL does not support fixed ECDH or null ciphers.
+        - tests/compat.sh -p OpenSSL -e 'NULL\|ECDH_'
+        - tests/scripts/travis-log-failure.sh
+        - tests/context-info.sh
+
+    - name: full configuration(GnuTLS compat tests) on arm64
+      os: linux
+      dist: focal
+      arch: arm64
+      addons:
+        apt:
+          packages:
+          - clang
+          - gnutls-bin
+      script:
+        # Do a manual build+test sequence rather than using all.sh.
+        #
+        # On Arm64 host of Travis CI, the time of `test_full_cmake_*` exceeds
+        # limitation of Travis CI. Base on `test_full_cmake_*`, we removed
+        # `ssl-opt.sh` and OpenSSl compat.sh here to meet the time limitation.
+        - scripts/config.py full
+        - make generated_files
+        - make CC=clang CFLAGS='-O3 -Werror -fsanitize=address,undefined -fno-sanitize-recover=all' LDFLAGS='-Werror -fsanitize=address,undefined -fno-sanitize-recover=all'
+        # GnuTLS supports CAMELLIA but compat.sh doesn't properly enable it.
+        - tests/compat.sh -p GnuTLS -e 'CAMELLIA'
+        - tests/scripts/travis-log-failure.sh
+        - tests/context-info.sh
+
+after_failure:
+- tests/scripts/travis-log-failure.sh
+
+env:
+  global:
+    - SEED=1
+    - secure: "JECCru6HASpKZ0OLfHh8f/KXhKkdrCwjquZghd/qbA4ksxsWImjR7KEPERcaPndXEilzhDbKwuFvJiQX2duVgTGoq745YGhLZIjzo1i8tySkceCVd48P8WceYGz+F/bmY7r+m6fFNuxDSoGGSVeA4Lnjvmm8PFUP45YodDV9no4="
+
+install:
+  - $PYTHON scripts/min_requirements.py
+
+addons:
+  apt:
+    packages:
+    - gnutls-bin
+  coverity_scan:
+    project:
+      name: "ARMmbed/mbedtls"
+    notification_email: support-mbedtls@arm.com
+    build_command_prepend:
+    build_command: make
+    branch_pattern: coverity_scan

mbedtls/.uncrustify.cfg

+# Configuration options for Uncrustify specifying the Mbed TLS code style.
+#
+# Note: The code style represented by this file has not yet been introduced
+# to Mbed TLS.
+#
+# Copyright The Mbed TLS Contributors
+# SPDX-License-Identifier: Apache-2.0
+#
+# Licensed under the Apache License, Version 2.0 (the "License"); you may
+# not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+# http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+# WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+
+# Wrap lines at 100 characters
+code_width = 100
+
+# Allow splitting long for statements between the condition statements
+ls_for_split_full = true
+
+# Allow splitting function calls between arguments
+ls_func_split_full = true
+
+input_tab_size = 4
+
+# Spaces-only indentation
+indent_with_tabs = 0
+
+indent_columns = 4
+
+# Indent 'case' 1 level from 'switch'
+indent_switch_case = indent_columns
+
+# Line-up strings broken by '\'
+indent_align_string = true
+
+# Braces on the same line (Egyptian-style braces)
+nl_enum_brace = remove
+nl_union_brace = remove
+nl_struct_brace = remove
+nl_do_brace = remove
+nl_if_brace = remove
+nl_for_brace = remove
+nl_else_brace = remove
+nl_while_brace = remove
+nl_switch_brace = remove
+
+# Braces on same line as keywords that follow them - 'else' and the 'while' in 'do {} while ()';
+nl_brace_else = remove
+nl_brace_while = remove
+# Space before else on the same line
+sp_brace_else = add
+# If else is on the same line as '{', force exactly 1 space between them
+sp_else_brace = force
+
+# Functions are the exception and have braces on the next line
+nl_fcall_brace = add
+nl_fdef_brace = add
+
+# Force exactly one space between ')' and '{' in statements
+sp_sparen_brace = force
+
+# At least 1 space around assignment
+sp_assign = add
+
+# Remove spaces around the preprocessor '##' token-concatenate
+sp_pp_concat = ignore
+
+# At least 1 space around '||' and '&&'
+sp_bool = add
+
+# But no space after the '!' operator
+sp_not = remove
+
+# No space after the bitwise-not '~' operator
+sp_inv = remove
+
+# No space after the addressof '&' operator
+sp_addr = remove
+
+# No space around the member '.' and '->' operators
+sp_member = remove
+
+# No space after the dereference '*' operator
+sp_deref = remove
+
+# No space after a unary negation '-'
+sp_sign = remove
+
+# No space between the '++'/'--' operator and its operand
+sp_incdec = remove
+
+# At least 1 space around comparison operators
+sp_compare = add
+
+# Remove spaces inside all kinds of parentheses:
+
+# Remove spaces inside parentheses
+sp_inside_paren = remove
+
+# No spaces inside statement parentheses
+sp_inside_sparen = remove
+
+# No spaces inside cast parentheses '( char )x' -> '(char)x'
+sp_inside_paren_cast = remove
+
+# No spaces inside function parentheses
+sp_inside_fparen = remove
+# (The case where the function has no parameters/arguments)
+sp_inside_fparens = remove
+
+# No spaces inside the first parentheses in a function type
+sp_inside_tparen = remove
+
+# (Uncrustify >= 0.74.0) No spaces inside parens in for statements
+sp_inside_for = remove
+
+# Remove spaces between nested parentheses '( (' -> '(('
+sp_paren_paren = remove
+# (Uncrustify >= 0.74.0)
+sp_sparen_paren = remove
+
+# Remove spaces between ')' and adjacent '('
+sp_cparen_oparen = remove
+
+# (Uncrustify >= 0.73.0) space between 'do' and '{'
+sp_do_brace_open = force
+
+# (Uncrustify >= 0.73.0) space between '}' and 'while'
+sp_brace_close_while = force
+
+# At least 1 space before a '*' pointer star
+sp_before_ptr_star = add
+
+# Remove spaces between pointer stars
+sp_between_ptr_star = remove
+
+# No space after a pointer star
+sp_after_ptr_star = remove
+
+# But allow a space in the case of e.g. char * const x;
+sp_after_ptr_star_qualifier = ignore
+
+# Remove space after star in a function return type
+sp_after_ptr_star_func = remove
+
+# At least 1 space after a type in variable definition etc
+sp_after_type = add
+
+# Force exactly 1 space between a statement keyword (e.g. 'if') and an opening parenthesis
+sp_before_sparen = force
+
+# Remove a space before a ';'
+sp_before_semi = remove
+# (Uncrustify >= 0.73.0) Remove space before a semi in a non-empty for
+sp_before_semi_for = remove
+# (Uncrustify >= 0.73.0) Remove space in empty first statement of a for
+sp_before_semi_for_empty = remove
+# (Uncrustify >= 0.74.0) Remove space in empty middle statement of a for
+sp_between_semi_for_empty = remove
+
+# Add a space after a ';' (unless a comment follows)
+sp_after_semi = add
+# (Uncrustify >= 0.73.0) Add a space after a semi in non-empty for statements
+sp_after_semi_for = add
+# (Uncrustify >= 0.73.0) No space after final semi in empty for statements
+sp_after_semi_for_empty = remove
+
+# Remove spaces on the inside of square brackets '[]'
+sp_inside_square = remove
+
+# Must have at least 1 space after a comma
+sp_after_comma = add
+
+# Must not have a space before a comma
+sp_before_comma = remove
+
+# No space before the ':' in a case statement
+sp_before_case_colon = remove
+
+# Must have space after a cast - '(char)x' -> '(char) x'
+sp_after_cast = add
+
+# No space between 'sizeof' and '('
+sp_sizeof_paren = remove
+
+# At least 1 space inside '{ }'
+sp_inside_braces = add
+
+# At least 1 space inside '{ }' in an enum
+sp_inside_braces_enum = add
+
+# At least 1 space inside '{ }' in a struct
+sp_inside_braces_struct = add
+
+# At least 1 space between a function return type and the function name
+sp_type_func = add
+
+# No space between a function name and its arguments/parameters
+sp_func_proto_paren = remove
+sp_func_def_paren = remove
+sp_func_call_paren = remove
+
+# No space between '__attribute__' and '('
+sp_attribute_paren = remove
+
+# No space between 'defined' and '(' in preprocessor conditions
+sp_defined_paren = remove
+
+# At least 1 space between a macro's name and its definition
+sp_macro = add
+sp_macro_func = add
+
+# Force exactly 1 space between a '}' and the name of a typedef if on the same line
+sp_brace_typedef = force
+
+# At least 1 space before a '\' line continuation
+sp_before_nl_cont = add
+
+# At least 1 space around '?' and ':' in ternary statements
+sp_cond_colon = add
+sp_cond_question = add
+
+# Space between #else/#endif and comment afterwards
+sp_endif_cmt = add
+
+# Remove newlines at the start of a file
+nl_start_of_file = remove
+
+# At least 1 newline at the end of a file
+nl_end_of_file = add
+nl_end_of_file_min = 1
+
+# Add braces in single-line statements
+mod_full_brace_do = add
+mod_full_brace_for = add
+mod_full_brace_if = add
+mod_full_brace_while = add
+
+# Remove parentheses from return statements
+mod_paren_on_return = remove
+
+# Disable removal of leading spaces in a multi-line comment if the first and
+# last lines are the same length
+cmt_multi_check_last = false

mbedtls/3rdparty/.gitignore

+/Makefile

mbedtls/3rdparty/CMakeLists.txt

+execute_process(COMMAND ${MBEDTLS_PYTHON_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/config.py -f ${CMAKE_CURRENT_SOURCE_DIR}/../include/mbedtls/mbedtls_config.h get MBEDTLS_ECDH_VARIANT_EVEREST_ENABLED RESULT_VARIABLE result)
+
+if(${result} EQUAL 0)
+    add_subdirectory(everest)
+endif()

mbedtls/3rdparty/Makefile.inc

+THIRDPARTY_DIR = $(dir $(lastword $(MAKEFILE_LIST)))
+include $(THIRDPARTY_DIR)/everest/Makefile.inc