Merge upstream 3.0 from 'development' in ARMmbed/mbedtls

Signed-off-by: Yuto Takano <yuto.takano@arm.com>
diff --git a/tests/scripts/all.sh b/tests/scripts/all.sh
index f8e43c8..efcb554 100755
--- a/tests/scripts/all.sh
+++ b/tests/scripts/all.sh
@@ -733,7 +733,7 @@
 
 component_check_names () {
     msg "Check: declared and exported names (builds the library)" # < 3s
-    record_status tests/scripts/check-names.sh -v
+    record_status tests/scripts/check-names.py -v
 }
 
 component_check_test_cases () {
diff --git a/tests/scripts/check-names.py b/tests/scripts/check-names.py
new file mode 100755
index 0000000..8a8e2db
--- /dev/null
+++ b/tests/scripts/check-names.py
@@ -0,0 +1,270 @@
+#!/usr/bin/env python2
+"""
+This file is part of Mbed TLS (https://tls.mbed.org)
+
+Copyright (c) 2018, Arm Limited, All Rights Reserved
+
+Purpose
+
+This script confirms that the naming of all symbols and identifiers in mbed
+TLS are consistent with the house style and are also self-consistent.
+"""
+import os
+import sys
+import traceback
+import re
+import shutil
+import subprocess
+import logging
+
+
+class NameCheck(object):
+    def __init__(self):
+        self.log = None
+        self.setup_logger()
+        self.check_repo_path()
+        self.return_code = 0
+        self.excluded_files = ["compat-1.3.h"]
+        self.header_files = self.get_files(os.path.join("include", "mbedtls"))
+        self.library_files = self.get_files("library")
+        self.macros = []
+        self.MBED_names = []
+        self.enum_consts = []
+        self.identifiers = []
+        self.actual_macros = []
+        self.symbols = []
+        self.macro_pattern = r"#define (?P<macro>\w+)"
+        self.MBED_pattern = r"\bMBED.+?_[A-Z0-9_]*"
+        self.symbol_pattern = r"^\S+( [0-9A-Fa-f]+)* . _*(?P<symbol>\w+)"
+        self.identifier_check_pattern = r"^mbedtls_[0-9a-z_]*[0-9a-z]$"
+        self.decls_pattern = (
+            r"^(extern \"C\"|(typedef )?(struct|enum)( {)?$|};?$|$)"
+        )
+        self.macro_const_check_pattern = (
+            r"^MBEDTLS_[0-9A-Z_]*[0-9A-Z]$|^YOTTA_[0-9A-Z_]*[0-9A-Z]$"
+        )
+        self.typo_check_pattern = r"XXX|__|_$|^MBEDTLS_.*CONFIG_FILE$"
+        self.non_macros = (
+            "asm", "inline", "EMIT", "_CRT_SECURE_NO_DEPRECATE", "MULADDC_"
+        )
+
+    def set_return_code(self, return_code):
+        if return_code > self.return_code:
+            self.return_code = return_code
+
+    def setup_logger(self):
+        self.log = logging.getLogger()
+        self.log.setLevel(logging.INFO)
+        self.log.addHandler(logging.StreamHandler())
+
+    def check_repo_path(self):
+        current_dir = os.path.realpath('.')
+        root_dir = os.path.dirname(os.path.dirname(
+            os.path.dirname(os.path.realpath(__file__))))
+        if current_dir != root_dir:
+            raise Exception("Must be run from Mbed TLS root")
+
+    def get_files(self, directory):
+        filenames = []
+        for root, dirs, files in sorted(os.walk(directory)):
+            for filename in sorted(files):
+                if (filename not in self.excluded_files and
+                        filename.endswith((".c", ".h"))):
+                    filenames.append(os.path.join(root, filename))
+        return filenames
+
+    def get_macros(self):
+        for header_file in self.header_files:
+            with open(header_file, "r") as header:
+                for line in iter(header.readline, ""):
+                    macro = re.search(self.macro_pattern, line)
+                    if (macro and not
+                            macro.group("macro").startswith(self.non_macros)):
+                        self.macros.append((macro.group("macro"), header_file))
+        self.macros = list(set(self.macros))
+
+    def get_MBED_names(self):
+        for file_group in [self.header_files, self.library_files]:
+            for filename in file_group:
+                with open(filename, "r") as f:
+                    for line in iter(f.readline, ""):
+                        mbed_names = re.findall(self.MBED_pattern, line)
+                        if mbed_names:
+                            for name in mbed_names:
+                                self.MBED_names.append((name, filename))
+        self.MBED_names = list(set(self.MBED_names))
+
+    def get_enum_consts(self):
+        for header_file in self.header_files:
+            state = 0
+            with open(header_file, "r") as header:
+                for line in iter(header.readline, ""):
+                    if state is 0 and re.match(r"^(typedef )?enum {", line):
+                        state = 1
+                    elif state is 0 and re.match(r"^(typedef )?enum", line):
+                        state = 2
+                    elif state is 2 and re.match(r"^{", line):
+                        state = 1
+                    elif state is 1 and re.match(r"^}", line):
+                        state = 0
+                    elif state is 1:
+                        enum_const = re.match(r"^\s*(?P<enum_const>\w+)", line)
+                        if enum_const:
+                            self.enum_consts.append(
+                                (enum_const.group("enum_const"), header_file)
+                            )
+
+    def line_contains_declaration(self, line):
+        return (re.match(r"^[^ /#{]", line)
+                and not re.match(self.decls_pattern, line))
+
+    def get_identifier_from_declaration(self, declaration):
+        identifier = re.search(
+            r"([a-zA-Z_][a-zA-Z0-9_]*)\(|"
+            r"\(\*(.+)\)\(|"
+            r"(\w+)\W*$",
+            declaration
+        )
+        if identifier:
+            for group in identifier.groups():
+                if group:
+                    return group
+        self.log.error(declaration)
+        raise Exception("No identifier found")
+
+    def get_identifiers(self):
+        for header_file in self.header_files:
+            with open(header_file, "r") as header:
+                for line in iter(header.readline, ""):
+                    if self.line_contains_declaration(line):
+                        self.identifiers.append(
+                            (self.get_identifier_from_declaration(line),
+                             header_file)
+                        )
+
+    def get_symbols(self):
+        try:
+            shutil.copy("include/mbedtls/config.h",
+                        "include/mbedtls/config.h.bak")
+            subprocess.check_output(
+                ["perl", "scripts/config.pl", "full"],
+                universal_newlines=True,
+            )
+            my_environment = os.environ.copy()
+            my_environment["CFLAGS"] = "-fno-asynchronous-unwind-tables"
+            subprocess.check_output(
+                ["make", "clean", "lib"],
+                env=my_environment,
+                universal_newlines=True,
+                stderr=subprocess.STDOUT,
+            )
+            shutil.move("include/mbedtls/config.h.bak",
+                        "include/mbedtls/config.h")
+            nm_output = ""
+            for lib in ["library/libmbedcrypto.a",
+                        "library/libmbedtls.a",
+                        "library/libmbedx509.a"]:
+                nm_output += subprocess.check_output(
+                    ["nm", "-og", lib],
+                    universal_newlines=True,
+                    stderr=subprocess.STDOUT,
+                )
+            for line in nm_output.splitlines():
+                if not re.match(r"^\S+: +U |^$|^\S+:$", line):
+                    symbol = re.match(self.symbol_pattern, line)
+                    if symbol:
+                        self.symbols.append(symbol.group('symbol'))
+                    else:
+                        self.log.error(line)
+            self.symbols.sort()
+            subprocess.check_output(
+                ["make", "clean"],
+                universal_newlines=True,
+            )
+        except subprocess.CalledProcessError as error:
+            self.log.error(error)
+            self.set_return_code(2)
+
+    def check_symbols_declared_in_header(self):
+        identifiers = [x[0] for x in self.identifiers]
+        bad_names = []
+        for symbol in self.symbols:
+            if symbol not in identifiers:
+                bad_names.append(symbol)
+        if bad_names:
+            self.set_return_code(1)
+            self.log.info("Names of identifiers: FAIL")
+            for name in bad_names:
+                self.log.info(name)
+        else:
+            self.log.info("Names of identifiers: PASS")
+
+    def check_group(self, group_to_check, check_pattern, name):
+        bad_names = []
+        for item in group_to_check:
+            if not re.match(check_pattern, item[0]):
+                bad_names.append("{} - {}".format(item[0], item[1]))
+        if bad_names:
+            self.set_return_code(1)
+            self.log.info("Names of {}: FAIL".format(name))
+            for name in bad_names:
+                self.log.info(name)
+        else:
+            self.log.info("Names of {}: PASS".format(name))
+
+    def check_for_typos(self):
+        bad_names = []
+        all_caps_names = list(set(
+            [x[0] for x in self.actual_macros + self.enum_consts]
+        ))
+        for name in self.MBED_names:
+            if name[0] not in all_caps_names:
+                if not re.search(self.typo_check_pattern, name[0]):
+                    bad_names.append("{} - {}".format(name[0], name[1]))
+        if bad_names:
+            self.set_return_code(1)
+            self.log.info("Likely typos: FAIL")
+            for name in bad_names:
+                self.log.info(name)
+        else:
+            self.log.info("Likely typos: PASS")
+
+    def get_names_from_source_code(self):
+        self.log.info("Analysing source code...")
+        self.get_macros()
+        self.get_enum_consts()
+        self.get_identifiers()
+        self.get_symbols()
+        self.get_MBED_names()
+        self.actual_macros = list(set(self.macros) - set(self.identifiers))
+        self.log.info("{} macros".format(len(self.macros)))
+        self.log.info("{} enum-consts".format(len(self.enum_consts)))
+        self.log.info("{} identifiers".format(len(self.identifiers)))
+        self.log.info("{} exported-symbols".format(len(self.symbols)))
+
+    def check_names(self):
+        self.check_symbols_declared_in_header()
+        for group, check_pattern, name in [
+                (self.actual_macros, self.macro_const_check_pattern,
+                 "actual-macros"),
+                (self.enum_consts, self.macro_const_check_pattern,
+                 "enum-consts"),
+                (self.identifiers, self.identifier_check_pattern,
+                 "identifiers")]:
+            self.check_group(group, check_pattern, name)
+        self.check_for_typos()
+
+
+def run_main():
+    try:
+        name_check = NameCheck()
+        name_check.get_names_from_source_code()
+        name_check.check_names()
+        sys.exit(name_check.return_code)
+    except Exception:
+        traceback.print_exc()
+        sys.exit(2)
+
+
+if __name__ == "__main__":
+    run_main()
diff --git a/tests/scripts/check-names.sh b/tests/scripts/check-names.sh
deleted file mode 100755
index 2a06adc..0000000
--- a/tests/scripts/check-names.sh
+++ /dev/null
@@ -1,129 +0,0 @@
-#!/bin/sh
-#
-# 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.
-
-set -eu
-
-if [ $# -ne 0 ] && [ "$1" = "--help" ]; then
-    cat <<EOF
-$0 [-v]
-This script confirms that the naming of all symbols and identifiers in mbed
-TLS are consistent with the house style and are also self-consistent.
-
-  -v    If the script fails unexpectedly, print a command trace.
-EOF
-    exit
-fi
-
-trace=
-if [ $# -ne 0 ] && [ "$1" = "-v" ]; then
-  shift
-  trace='-x'
-  exec 2>check-names.err
-  trap 'echo "FAILED UNEXPECTEDLY, status=$?";
-        cat check-names.err' EXIT
-  set -x
-fi
-
-printf "Analysing source code...\n"
-
-sh $trace tests/scripts/list-macros.sh
-tests/scripts/list-enum-consts.pl
-sh $trace tests/scripts/list-identifiers.sh
-sh $trace tests/scripts/list-symbols.sh
-
-FAIL=0
-
-printf "\nExported symbols declared in header: "
-UNDECLARED=$( diff exported-symbols identifiers | sed -n -e 's/^< //p' )
-if [ "x$UNDECLARED" = "x" ]; then
-    echo "PASS"
-else
-    echo "FAIL"
-    echo "$UNDECLARED"
-    FAIL=1
-fi
-
-diff macros identifiers | sed -n -e 's/< //p' > actual-macros
-
-for THING in actual-macros enum-consts; do
-    printf 'Names of %s: ' "$THING"
-    test -r $THING
-    BAD=$( grep -E -v '^(MBEDTLS|PSA)_[0-9A-Z_]*[0-9A-Z]$' $THING || true )
-    UNDERSCORES=$( grep -E '.*__.*' $THING || true )
-
-    if [ "x$BAD" = "x" ] && [ "x$UNDERSCORES" = "x" ]; then
-        echo "PASS"
-    else
-        echo "FAIL"
-        echo "$BAD"
-        echo "$UNDERSCORES"
-        FAIL=1
-    fi
-done
-
-for THING in identifiers; do
-    printf 'Names of %s: ' "$THING"
-    test -r $THING
-    BAD=$( grep -E -v '^(mbedtls|psa)_[0-9a-z_]*[0-9a-z]$' $THING || true )
-    if [ "x$BAD" = "x" ]; then
-        echo "PASS"
-    else
-        echo "FAIL"
-        echo "$BAD"
-        FAIL=1
-    fi
-done
-
-printf "Likely typos: "
-sort -u actual-macros enum-consts > _caps
-HEADERS=$( ls include/mbedtls/*.h include/psa/*.h | egrep -v 'compat-2\.x\.h' )
-HEADERS="$HEADERS library/*.h"
-HEADERS="$HEADERS 3rdparty/everest/include/everest/everest.h 3rdparty/everest/include/everest/x25519.h"
-LIBRARY="$( ls library/*.c )"
-LIBRARY="$LIBRARY 3rdparty/everest/library/everest.c 3rdparty/everest/library/x25519.c"
-NL='
-'
-cat $HEADERS $LIBRARY \
-    | grep -v -e '//no-check-names' -e '#error' \
-    | sed -n 's/MBED..._[A-Z0-9_]*/\'"$NL"'&\'"$NL"/gp \
-    | grep MBEDTLS | sort -u > _MBEDTLS_XXX
-TYPOS=$( diff _caps _MBEDTLS_XXX | sed -n 's/^> //p' \
-            | egrep -v 'XXX|__|_$|^MBEDTLS_.*CONFIG_FILE$' || true )
-rm _MBEDTLS_XXX _caps
-if [ "x$TYPOS" = "x" ]; then
-    echo "PASS"
-else
-    echo "FAIL"
-    echo "$TYPOS"
-    FAIL=1
-fi
-
-if [ -n "$trace" ]; then
-  set +x
-  trap - EXIT
-  rm check-names.err
-fi
-
-printf "\nOverall: "
-if [ "$FAIL" -eq 0 ]; then
-    rm macros actual-macros enum-consts identifiers exported-symbols
-    echo "PASSED"
-    exit 0
-else
-    echo "FAILED"
-    exit 1
-fi
diff --git a/tests/scripts/list-enum-consts.pl b/tests/scripts/list-enum-consts.pl
deleted file mode 100755
index 6d93693..0000000
--- a/tests/scripts/list-enum-consts.pl
+++ /dev/null
@@ -1,53 +0,0 @@
-#!/usr/bin/env perl
-#
-# 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.
-
-use warnings;
-use strict;
-
-use utf8;
-use open qw(:std utf8);
-
--d 'include/mbedtls' or die "$0: must be run from root\n";
-
-@ARGV = grep { ! /compat-2\.x\.h/ } <include/mbedtls/*.h>;
-push @ARGV, "3rdparty/everest/include/everest/everest.h";
-push @ARGV, "3rdparty/everest/include/everest/x25519.h";
-push @ARGV, glob("library/*.h");
-
-my @consts;
-my $state = 'out';
-while (<>)
-{
-    if( $state eq 'out' and /^(typedef )?enum \{/ ) {
-        $state = 'in';
-    } elsif( $state eq 'out' and /^(typedef )?enum/ ) {
-        $state = 'start';
-    } elsif( $state eq 'start' and /{/ ) {
-        $state = 'in';
-    } elsif( $state eq 'in' and /}/ ) {
-        $state = 'out';
-    } elsif( $state eq 'in' and not /^#/) {
-        s/=.*//; s!/\*.*!!; s/,.*//; s/\s+//g; chomp;
-        push @consts, $_ if $_;
-    }
-}
-
-open my $fh, '>', 'enum-consts' or die;
-print $fh "$_\n" for sort @consts;
-close $fh or die;
-
-printf "%8d enum-consts\n", scalar @consts;
diff --git a/tests/scripts/list-identifiers.sh b/tests/scripts/list-identifiers.sh
deleted file mode 100755
index 9698fc8..0000000
--- a/tests/scripts/list-identifiers.sh
+++ /dev/null
@@ -1,78 +0,0 @@
-#!/bin/bash
-#
-# Create a file named identifiers containing identifiers from internal header
-# files or all header files, based on --internal flag.
-# Outputs the line count of the file to stdout.
-#
-# Usage: list-identifiers.sh [ -i | --internal ]
-#
-# 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.
-
-set -eu
-
-if [ -d include/mbedtls ]; then :; else
-    echo "$0: must be run from root" >&2
-    exit 1
-fi
-
-INTERNAL=""
-
-until [ -z "${1-}" ]
-do
-  case "$1" in
-    -i|--internal)
-      INTERNAL="1"
-      ;;
-    *)
-      # print error
-      echo "Unknown argument: '$1'"
-      exit 1
-      ;;
-  esac
-  shift
-done
-
-if [ $INTERNAL ]
-then
-    HEADERS=$( ls include/mbedtls/*_internal.h library/*.h | egrep -v 'compat-2\.x\.h' )
-else
-    HEADERS=$( ls include/mbedtls/*.h include/psa/*.h library/*.h | egrep -v 'compat-2\.x\.h' )
-    HEADERS="$HEADERS 3rdparty/everest/include/everest/everest.h 3rdparty/everest/include/everest/x25519.h"
-fi
-
-rm -f identifiers
-
-grep '^[^ /#{]' $HEADERS | \
-    sed -e 's/^[^:]*://' | \
-    egrep -v '^(extern "C"|(typedef )?(struct|union|enum)( {)?$|};?$)' \
-    > _decls
-
-if true; then
-sed -n -e 's/.* \**\([a-zA-Z_][a-zA-Z0-9_]*\)(.*/\1/p' \
-       -e 's/.*(\*\(.*\))(.*/\1/p' _decls
-grep -v '(' _decls | sed -e 's/\([a-zA-Z0-9_]*\)[;[].*/\1/' -e 's/.* \**//'
-fi > _identifiers
-
-if [ $( wc -l < _identifiers ) -eq $( wc -l < _decls ) ]; then
-    rm _decls
-    egrep -v '^(u?int(16|32|64)_t)$' _identifiers | sort > identifiers
-    rm _identifiers
-else
-    echo "$0: oops, lost some identifiers" 2>&1
-    exit 1
-fi
-
-wc -l identifiers
diff --git a/tests/scripts/list-macros.sh b/tests/scripts/list-macros.sh
deleted file mode 100755
index 2e62359..0000000
--- a/tests/scripts/list-macros.sh
+++ /dev/null
@@ -1,39 +0,0 @@
-#!/bin/sh
-#
-# 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.
-
-set -eu
-
-if [ -d include/mbedtls ]; then :; else
-    echo "$0: must be run from root" >&2
-    exit 1
-fi
-
-HEADERS=$( ls include/mbedtls/*.h include/psa/*.h tests/include/test/drivers/*.h | egrep -v 'compat-2\.x\.h' )
-HEADERS="$HEADERS library/*.h"
-HEADERS="$HEADERS 3rdparty/everest/include/everest/everest.h 3rdparty/everest/include/everest/x25519.h"
-
-sed -n -e 's/.*#define \([a-zA-Z0-9_]*\).*/\1/p' $HEADERS \
-    | egrep -v '^(asm|inline|EMIT|_CRT_SECURE_NO_DEPRECATE)$|^MULADDC_' \
-    | sort -u > macros
-
-# For include/mbedtls/config_psa.h need to ignore the MBEDTLS_xxx define
-# in that file since they may not be defined in include/psa/crypto_config.h
-# This line renames the potentially missing defines to ones that should
-# be present.
-sed -ne 's/^MBEDTLS_PSA_BUILTIN_/MBEDTLS_PSA_ACCEL_/p' <macros >>macros
-
-wc -l macros
diff --git a/tests/scripts/list-symbols.sh b/tests/scripts/list-symbols.sh
deleted file mode 100755
index 4a5d035..0000000
--- a/tests/scripts/list-symbols.sh
+++ /dev/null
@@ -1,54 +0,0 @@
-#!/bin/sh
-#
-# 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.
-
-set -eu
-
-if [ -d include/mbedtls ]; then :; else
-    echo "$0: must be run from root" >&2
-    exit 1
-fi
-
-if grep -i cmake Makefile >/dev/null; then
-    echo "$0: not compatible with cmake" >&2
-    exit 1
-fi
-
-cp include/mbedtls/mbedtls_config.h include/mbedtls/mbedtls_config.h.bak
-scripts/config.py full
-make clean
-make_ret=
-CFLAGS=-fno-asynchronous-unwind-tables make lib \
-      >list-symbols.make.log 2>&1 ||
-  {
-    make_ret=$?
-    echo "Build failure: CFLAGS=-fno-asynchronous-unwind-tables make lib"
-    cat list-symbols.make.log >&2
-  }
-rm list-symbols.make.log
-mv include/mbedtls/mbedtls_config.h.bak include/mbedtls/mbedtls_config.h
-if [ -n "$make_ret" ]; then
-    exit "$make_ret"
-fi
-
-if uname | grep -F Darwin >/dev/null; then
-    nm -gUj library/libmbed*.a 2>/dev/null | sed -n -e 's/^_//p' | grep -v -e ^FStar -e ^Hacl
-elif uname | grep -F Linux >/dev/null; then
-    nm -og library/libmbed*.a | grep -v '^[^ ]*: *U \|^$\|^[^ ]*:$' | sed 's/^[^ ]* . //' | grep -v -e ^FStar -e ^Hacl
-fi | sort > exported-symbols
-make clean
-
-wc -l exported-symbols