Specifications source code for LSB Core 3.1

/*
 * Copyright (c) 2005-2006 Institute for System Programming
 * Russian Academy of Sciences
 * All rights reserved.
 *
 * 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.
 */

/*
 * Portions of this text are reprinted and reproduced in electronic form
 * from IEEE Std 1003.1, 2004 Edition, Standard for Information Technology
 * -- Portable Operating System Interface (POSIX), The Open Group Base
 * Specifications Issue 6, Copyright (C) 2001-2004 by the Institute of
 * Electrical and Electronics Engineers, Inc and The Open Group. In the
 * event of any discrepancy between this version and the original IEEE and
 * The Open Group Standard, the original IEEE and The Open Group Standard
 * is the referee document. The original Standard can be obtained online at
 * http://www.opengroup.org/unix/online.html.
 */


#include "config/interpretation.seh"
#include "fs/ftw/ftw_config.h"
#include "config/system_config.seh"
#include "data/errno_model.seh"
#include "fs/dir/dir_model.seh"
#include "fs/ftw/ftw_model.seh"
#include "fs/meta/meta_model.seh"
#include "process/process/process_model.seh"
#include "process/process/process_common.seh"
#include "system/system/system_model.seh"

#pragma SEC subsystem ftw "fs.ftw"

/*
   The group of functions 'fs.ftw' consists of:
       ftw      [SUSv3]
       ftw64    [LFS]
       nftw     [SUSv3]
       nftw64   [LFS]
 */

/*****************************************************************************/
/**                           Interface Functions                           **/
/*****************************************************************************/

/*
Linux Standard Base Core Specification 3.0
Copyright (c) 2004, 2005 Free Standards Group

 refers

The Open Group Base Specifications Issue 6
IEEE Std 1003.1, 2004 Edition
Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved

NAME

    ftw - traverse (walk) a file tree

SYNOPSIS

    #include <ftw.h>

    int ftw(const char *path, int (*fn)(const char *,
        const struct stat *ptr, int flag), int ndirs);

DESCRIPTION

    The ftw() function shall recursively descend the directory hierarchy rooted
    in path. For each object in the hierarchy, ftw() shall call the function
    pointed to by fn, passing it a pointer to a null-terminated character
    string containing the name of the object, a pointer to a stat structure
    containing information about the object, and an integer. Possible values of
    the integer, defined in the <ftw.h> header, are:

    FTW_D
        For a directory.
    FTW_DNR
        For a directory that cannot be read.
    FTW_F
        For a file.
    FTW_SL
        For a symbolic link (but see also FTW_NS below).
    FTW_NS
        For an object other than a symbolic link on which stat() could not
        successfully be executed. If the object is a symbolic link and stat()
        failed, it is unspecified whether ftw() passes FTW_SL or FTW_NS to the
        user-supplied function.

    If the integer is FTW_DNR, descendants of that directory shall not be
    processed. If the integer is FTW_NS, the stat structure contains undefined
    values. An example of an object that would cause FTW_NS to be passed to the
    function pointed to by fn would be a file in a directory with read but
    without execute (search) permission.

    The ftw() function shall visit a directory before visiting any of its
    descendants.

    The ftw() function shall use at most one file descriptor for each level in
    the tree.

    The argument ndirs should be in the range [1, {OPEN_MAX}].

    The tree traversal shall continue until either the tree is exhausted, an
    invocation of fn returns a non-zero value, or some error, other than
    [EACCES], is detected within ftw().

    The ndirs argument shall specify the maximum number of directory streams or
    file descriptors or both available for use by ftw() while traversing the
    tree. When ftw() returns it shall close any directory streams and file
    descriptors it uses not counting any opened by the application-supplied fn
    function.

    The results are unspecified if the application-supplied fn function does
    not preserve the current working directory.

    The ftw() function need not be reentrant. A function that is not required
    to be reentrant is not required to be thread-safe.

RETURN VALUE

    If the tree is exhausted, ftw() shall return 0. If the function pointed to
    by fn returns a non-zero value, ftw() shall stop its tree traversal and
    return whatever value was returned by the function pointed to by fn. If
    ftw() detects an error, it shall return -1 and set errno to indicate the
    error.

    If ftw() encounters an error other than [EACCES] (see FTW_DNR and FTW_NS
    above), it shall return -1 and set errno to indicate the error. The
    external variable errno may contain any error value that is possible when a
    directory is opened or when one of the stat functions is executed on a
    directory or file.

ERRORS

    The ftw() function shall fail if:

    [EACCES]
        Search permission is denied for any component of path or read
        permission is denied for path.
    [ELOOP]
        A loop exists in symbolic links encountered during resolution of the
        path argument.
    [ENAMETOOLONG]
        The length of the path argument exceeds {PATH_MAX} or a pathname
        component is longer than {NAME_MAX}.
    [ENOENT]
        A component of path does not name an existing file or path is an empty
        string.
    [ENOTDIR]
        A component of path is not a directory.
    [EOVERFLOW]
        A field in the stat structure cannot be represented correctly in the
        current programming environment for one or more files found in the file
        hierarchy.

    The ftw() function may fail if:

    [EINVAL]
        The value of the ndirs argument is invalid.
    [ELOOP]
        More than {SYMLOOP_MAX} symbolic links were encountered during
        resolution of the path argument.
    [ENAMETOOLONG]
        Pathname resolution of a symbolic link produced an intermediate result
        whose length exceeds {PATH_MAX}.

    In addition, if the function pointed to by fn encounters system errors,
    errno may be set accordingly.
*/
specification
IntT ftw_spec(CallContext context, CString *path, FTWFunction *fn, IntT ndirs,
              ErrorCode *errno)
{
    bool uptodate;
    Bool3 isELOOP;

    FileSystem *file_system = getFileSystem(context);

    Set *file_tree = getFileTree_FTW_Path(context, path, &uptodate);

    CString *absolute_path = resolvePath_Ext(context, file_system, path, &isELOOP);

    FILTER("ftw");

    pre
    {
        /* [Consistency of test suite] */
        REQ("", "The fn function is valid", (fn != NULL) => !fn->nftw);

        if( POSIX_FTW_FAILS_WITH_EINVAL == 0 ) /* MAY */
        {
            /* The argument ndirs should be in the range [1, {OPEN_MAX}] */
            REQ("app.ftw.01", "The ndirs should be in the range [1, {OPEN_MAX}]",
            (
                 checkFileDescriptorsLimit(context, ndirs) == True_Bool3
            ));

        } /* endif POSIX_FTW_FAILS_WITH_EINVAL */

        /*
         * The results are unspecified if the application-supplied fn function
         * does not preserve the current working directory.
         */
        REQ("app.ftw.02", "The fn function shall preserve the cwd", true);

        return true;
    }
    coverage C
    {
        if(!uptodate)
        {
            return { DirectoriesAreNotUptodate, "Directories are not uptodate" };
        }
        else
        {
            return { DirectoriesAreUptodate, "Directories are uptodate" };
        }
    }
    post
    {
        bool fn_returned_minus_one = false;

        Set *processed_file_tree, *non_processed_file_tree;

        if(!uptodate)
        {
            return true;
        }

        processed_file_tree = getProcessedFileTree_FTWFunction(fn);
        non_processed_file_tree = getNonProcessedFileTree_FTWFunction(context, fn);

        traceFormattedUserInfo("ftw_spec: file tree=$(obj)", file_tree);
        traceFormattedUserInfo("ftw_spec: processed file tree=$(obj)", processed_file_tree);
        traceFormattedUserInfo("ftw_spec: non-processed file tree=$(obj)", non_processed_file_tree);

        /*
         * The tree traversal shall continue until either the tree is
         * exhausted, an invocation of fn returns a non-zero value, or some
         * error, other than [EACCES], is detected within ftw().
         */
        if(returnedNonZero_FTWFunction(fn))
        {
            int non_zero_call_number = getNonZeroCallNumber_FTWFunction(fn);
            FTWFunctionCall *non_zero_call = getCall_FTWFunction(fn, non_zero_call_number);

            /*
             * If the function pointed to by fn returns a non-zero value, ftw()
             * shall stop its tree traversal and return whatever value was
             * returned by the function pointed to by fn.
             */
            REQ("ftw.08.02", "ftw() shall stop and return value returned by the fn",
            (
                non_zero_call_number == getCallsNumber_FTWFunction(fn) - 1 &&
                ftw_spec == non_zero_call->result
            ));

            fn_returned_minus_one = non_zero_call->result == -1;
        }
        else if(equals(processed_file_tree, file_tree))
        {
            /* If the tree is exhausted, ftw() shall return 0 */
            REQ("ftw.08.02", "ftw() shall return 0", ftw_spec == 0);
        }


        /*
         * If ftw() detects an error, it shall return -1 and set errno to
         * indicate the error.
         *
         * If ftw() encounters an error other than [EACCES] (see FTW_DNR
         * and FTW_NS above), it shall return -1 and set errno to indicate
         * the error.
         */
        if (*errno==SUT_EACCES)
        {
            REQ("ftw.08.03", "On [EACCES] function should return 0 or fn returns non-zero",
            (
                ftw_spec == 0 || returnedNonZero_FTWFunction(fn)
            ));
        }

        /*
         * If ftw() detects an error, it shall return -1 and set errno to
         * indicate the error.
         *
         * If ftw() encounters an error other than [EACCES] (see FTW_DNR and
         * FTW_NS above), it shall return -1 and set errno to indicate the
         * error.
         */
        ERROR_BEGIN(POSIX_FTW, "", !fn_returned_minus_one && ftw_spec == -1, *errno);

            /*
             * The ftw() function shall fail if:
             *
             * [ELOOP]
             *
             * A loop exists in symbolic links encountered during resolution of
             * the path argument.
             */
            ERROR_SHALL3(POSIX_FTW, ELOOP, "ftw.12.02", isELOOP);

            /*
             * The ftw() function shall fail if:
             *
             * [ENAMETOOLONG]
             *
             * The length of the path argument exceeds {PATH_MAX} or a pathname
             * component is longer than {NAME_MAX}.
             */
            ERROR_SHALL3(POSIX_FTW, ENAMETOOLONG, "ftw.12.03",
            (
                isENAMETOOLONG(context, path)
            ));

            /*
             * The ftw() function shall fail if:
             *
             * [ENOENT]
             *
             * A component of path does not name an existing file or path is an
             * empty string.
             */
            ERROR_SHALL3(POSIX_FTW, ENOENT, "ftw.12.04",
            (
                length_CString(path) == 0 ? True_Bool3 :
                    not_Bool3(doesFileExist_FileSystem(file_system, path))
            ));

            /*
             * The ftw() function shall fail if:
             *
             * [ENOTDIR]
             *
             * A component of path is not a directory.
             */
            ERROR_SHALL3(POSIX_FTW, ENOTDIR, "ftw.12.05",
            (
                isENOTDIR_dir(context, file_system, path)
            ));

            /*
             * The ftw() function shall fail if:
             *
             * [EOVERFLOW]
             *
             * A field in the stat structure cannot be represented correctly in
             * the current programming environment for one or more files found
             * in the file hierarchy.
             */
            ERROR_SHALL3(POSIX_FTW, EOVERFLOW, "ftw.12.06",
            (
                Unknown_Bool3
            ));

            /*
             * The ftw() function may fail if:
             *
             * [EINVAL]
             *
             * The value of the ndirs argument is invalid.
             */
            ERROR_MAY3(POSIX_FTW, EINVAL, "ftw.13.01",
            (
                not_Bool3(checkFileDescriptorsLimit(context, ndirs))
            ));

            /*
             * The ftw() function may fail if:
             *
             * [ELOOP]
             *
             * More than {SYMLOOP_MAX} symbolic links were encountered during
             * resolution of the path argument.
             */
            ERROR_MAY3(POSIX_FTW, ELOOP, "ftw.13.02", isELOOP);

            /*
             * The ftw() function may fail if:
             *
             * [ENAMETOOLONG]
             *
             * Pathname resolution of a symbolic link produced an intermediate
             * result whose length exceeds {PATH_MAX}.
             */
            ERROR_MAY3(POSIX_FTW, ENAMETOOLONG, "ftw.13.03",
            (
                isENAMETOOLONG(context, absolute_path)
            ));

        ERROR_END();

        /* [Implicit requirement] */
        REQ("", "No duplicates",
        (
            size_Set(processed_file_tree) == getCallsNumber_FTWFunction(fn)
        ));

        /*
         * The ftw() function shall recursively descend the directory hierarchy
         * rooted in path.
         */
        addAll_Set(processed_file_tree, non_processed_file_tree);

        REQ("ftw.01", "ftw() function shall recursively descent the path",
        (
            returnedNonZero_FTWFunction(fn) ?
                containsAll_Set(file_tree, processed_file_tree) :
                equals(processed_file_tree, file_tree)
        ));

        /*
         * For each object in the hierarchy, ftw() shall call the function
         * pointed to by fn, passing it a pointer to a null-terminated
         * character string containing the name of the object, a pointer to a
         * stat structure containing information about the object, and an
         * integer.
         */
        REQ("ftw.02", "ftw() shall call fn for objects in file tree",
        (
            checkCallsFlags_FTWFunction(context, fn) &&
            checkCallsOrder_FTWFunction(context, fn)
        ));

        /*
         * The ftw() function shall use at most one file descriptor for each
         * level in the tree.
         */
        REQ("ftw.07", "ftw() shall use at most one file descriptor for each level", TODO_REQ());

        /*
         * The ndirs argument shall specify the maximum number of directory
         * streams or file descriptors or both available for use by ftw() while
         * traversing the tree.
         */
        REQ("ftw.09", "The ndirs shall specify the maximum number of streams",
            TODO_REQ()
        );

        /*
         * When ftw() returns it shall close any directory streams and file
         * descriptors it uses not counting any opened by the
         * application-supplied fn function.
         */
        REQ("ftw.10", "ftw() shall close any directory streams",
            TODO_REQ()
        );

        /*
         * The external variable errno may contain any error value that is
         * possible when a directory is opened or when one of the stat
         * functions is executed on a directory or file.
         */
        REQ("ftw.11", "errno be set to any error", true);

        /*
         * In addition, if the function pointed to by fn encounters system
         * errors, errno may be set accordingly.
         */
        REQ("ftw.14", "errno may be set to system error", true);

        return true;
    }

    FILTER_CLEAN;

}

void onFTW(CallContext context, CString *path, FTWFunction *fn, IntT ndirs,
           ErrorCode *errno, IntT ftw_spec)
{
    FileSystem *file_system = getFileSystem(context);
    File *file = getFile_FileSystem(file_system, path);

    if(file != NULL && file->kind == DirectoryFile && !isUptodate_Directory(file))
    {
        int i, size;

        size = getCallsNumber_FTWFunction(fn);
        for(i = 0; i < size; i++)
        {
            FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

            if(fn_call->flag != SUT_FTW_NS)
            {
                file = registerFile_FileStatus(file_system, fn_call->path, fn_call->file_stat);

                if(file != NULL)
                {
                    if(file->kind == DirectoryFile)
                    {
                        setUptodate_Directory(file, fn_call->flag != SUT_FTW_DNR);
                    }
                }
            }
            else
            {
                file = registerFile(file_system, fn_call->path);
            }
        }
    }
}

specification
IntT ftw64_spec(CallContext context, CString *path, FTWFunction *fn, IntT ndirs,
                ErrorCode *errno)
{
    bool uptodate;
    Bool3 isELOOP;

    FileSystem *file_system = getFileSystem(context);

    Set *file_tree = getFileTree_FTW_Path(context, path, &uptodate);

    CString *absolute_path = resolvePath_Ext(context, file_system, path, &isELOOP);

    FILTER("ftw64");

    pre
    {
        /* [Consistency of test suite] */
        REQ("", "The fn function is valid", fn != NULL && !fn->nftw);

        if(LSB_FTW64_FAILS_WITH_EINVAL == 0) /* MAY */
        {
            /* The argument ndirs should be in the range [1, {OPEN_MAX}] */
            REQ("app.ftw64.01", "The ndirs should be in the range [1, {OPEN_MAX}]",
            (
                 checkFileDescriptorsLimit(context, ndirs) == True_Bool3
            ));

        } /* endif LSB_FTW64_FAILS_WITH_EINVAL */

        /*
         * The results are unspecified if the application-supplied fn function
         * does not preserve the current working directory.
         */
        REQ("app.ftw64.02", "The fn function shall preserve the cwd", true);

        return true;
    }
    coverage C
    {
        if(!uptodate)
        {
            return { DirectoriesAreNotUptodate, "Directories are not uptodate" };
        }
        else
        {
            return { DirectoriesAreUptodate, "Directories are uptodate" };
        }
    }
    post
    {
        bool fn_returned_minus_one = false;

        Set *processed_file_tree, *non_processed_file_tree;

        if(!uptodate)
        {
            return true;
        }

        processed_file_tree = getProcessedFileTree_FTWFunction(fn);
        non_processed_file_tree = getNonProcessedFileTree_FTWFunction(context, fn);

        traceFormattedUserInfo("ftw64_spec: file tree=$(obj)", file_tree);
        traceFormattedUserInfo("ftw64_spec: processed file tree=$(obj)", processed_file_tree);
        traceFormattedUserInfo("ftw64_spec: non-processed file tree=$(obj)", non_processed_file_tree);

        /*
         * The tree traversal shall continue until either the tree is
         * exhausted, an invocation of fn returns a non-zero value, or some
         * error, other than [EACCES], is detected within ftw().
         */
        if(returnedNonZero_FTWFunction(fn))
        {
            int non_zero_call_number = getNonZeroCallNumber_FTWFunction(fn);
            FTWFunctionCall *non_zero_call = getCall_FTWFunction(fn, non_zero_call_number);

            /*
             * If the function pointed to by fn returns a non-zero value, ftw()
             * shall stop its tree traversal and return whatever value was
             * returned by the function pointed to by fn.
             */
            REQ("ftw64.08.02", "ftw64() shall stop and return value returned by the fn",
            (
                non_zero_call_number == getCallsNumber_FTWFunction(fn) - 1 &&
                ftw64_spec == non_zero_call->result
            ));

            fn_returned_minus_one = non_zero_call->result == -1;
        }
        else if(equals(processed_file_tree, file_tree))
        {
            /* If the tree is exhausted, ftw() shall return 0 */
            REQ("ftw64.08.02", "ftw64() shall return 0", ftw64_spec == 0);
        }

        if (*errno==SUT_EACCES)
        {
            /*
             * If ftw() detects an error, it shall return -1 and set errno to
             * indicate the error.
             *
             * If ftw() encounters an error other than [EACCES] (see FTW_DNR
             * and FTW_NS above), it shall return -1 and set errno to indicate
             * the error.
             */
            REQ("ftw64.08.03", "On [EACCES] function should return 0",
            (
                ftw64_spec == 0
            ));
        }

        /*
         * If ftw() detects an error, it shall return -1 and set errno to
         * indicate the error.
         *
         * If ftw() encounters an error other than [EACCES] (see FTW_DNR and
         * FTW_NS above), it shall return -1 and set errno to indicate the
         * error.
         */
        ERROR_BEGIN(LSB_FTW64, "", !fn_returned_minus_one && ftw64_spec == -1, *errno);

            /*
             * The ftw() function shall fail if:
             *
             * [ELOOP]
             *
             * A loop exists in symbolic links encountered during resolution of
             * the path argument.
             */
            ERROR_SHALL3(LSB_FTW64, ELOOP, "ftw64.12.02", isELOOP);

            /*
             * The ftw() function shall fail if:
             *
             * [ENAMETOOLONG]
             *
             * The length of the path argument exceeds {PATH_MAX} or a pathname
             * component is longer than {NAME_MAX}.
             */
            ERROR_SHALL3(LSB_FTW64, ENAMETOOLONG, "ftw64.12.03",
            (
                isENAMETOOLONG(context, path)
            ));

            /*
             * The ftw() function shall fail if:
             *
             * [ENOENT]
             *
             * A component of path does not name an existing file or path is an
             * empty string.
             */
            ERROR_SHALL3(LSB_FTW64, ENOENT, "ftw64.12.04",
            (
                length_CString(path) == 0 ? True_Bool3 :
                    not_Bool3(doesFileExist_FileSystem(file_system, path))
            ));

            /*
             * The ftw() function shall fail if:
             *
             * [ENOTDIR]
             *
             * A component of path is not a directory.
             */
            ERROR_SHALL3(LSB_FTW64, ENOTDIR, "ftw64.12.05",
            (
                isENOTDIR_dir(context, file_system, path)
            ));

            /*
             * The ftw() function shall fail if:
             *
             * [EOVERFLOW]
             *
             * A field in the stat structure cannot be represented correctly in
             * the current programming environment for one or more files found
             * in the file hierarchy.
             */
            ERROR_SHALL(LSB_FTW64, EOVERFLOW, "ftw64.12.06",
                TODO_ERR(EOVERFLOW)
            );

            /*
             * The ftw() function may fail if:
             *
             * [EINVAL]
             *
             * The value of the ndirs argument is invalid.
             */
            ERROR_MAY3(LSB_FTW64, EINVAL, "ftw64.13.01",
            (
                not_Bool3(checkFileDescriptorsLimit(context, ndirs))
            ));

            /*
             * The ftw() function may fail if:
             *
             * [ELOOP]
             *
             * More than {SYMLOOP_MAX} symbolic links were encountered during
             * resolution of the path argument.
             */
            ERROR_MAY3(LSB_FTW64, ELOOP, "ftw64.13.02", isELOOP);

            /*
             * The ftw() function may fail if:
             *
             * [ENAMETOOLONG]
             *
             * Pathname resolution of a symbolic link produced an intermediate
             * result whose length exceeds {PATH_MAX}.
             */
            ERROR_MAY3(LSB_FTW64, ENAMETOOLONG, "ftw64.13.03",
            (
                isENAMETOOLONG(context, absolute_path)
            ));

        ERROR_END();

        /* [Implicit requirement] */
        REQ("", "No duplicates",
        (
            size_Set(processed_file_tree) == getCallsNumber_FTWFunction(fn)
        ));

        /*
         * The ftw() function shall recursively descend the directory hierarchy
         * rooted in path.
         */
        addAll_Set(processed_file_tree, non_processed_file_tree);

        REQ("ftw64.01", "ftw64() function shall recursively descent the path",
        (
            returnedNonZero_FTWFunction(fn) ?
                containsAll_Set(file_tree, processed_file_tree) :
                equals(processed_file_tree, file_tree)
        ));

        /*
         * For each object in the hierarchy, ftw() shall call the function
         * pointed to by fn, passing it a pointer to a null-terminated
         * character string containing the name of the object, a pointer to a
         * stat structure containing information about the object, and an
         * integer.
         */
        REQ("ftw64.02", "ftw64() shall call fn for objects in file tree",
        (
            checkCallsFlags_FTWFunction(context, fn) &&
            checkCallsOrder_FTWFunction(context, fn)
        ));

        /*
         * The ftw() function shall use at most one file descriptor for each
         * level in the tree.
         */
        REQ("ftw64.07", "ftw64() shall use at most one file descriptor for each level",
            TODO_REQ()
        );

        /*
         * The ndirs argument shall specify the maximum number of directory
         * streams or file descriptors or both available for use by ftw() while
         * traversing the tree.
         */
        REQ("ftw64.09", "The ndirs shall specify the maximum number of streams",
            TODO_REQ()
        );

        /*
         * When ftw() returns it shall close any directory streams and file
         * descriptors it uses not counting any opened by the
         * application-supplied fn function.
         */
        REQ("ftw64.10", "ftw64() shall close any directory streams",
            TODO_REQ()
        );

        /*
         * The external variable errno may contain any error value that is
         * possible when a directory is opened or when one of the stat
         * functions is executed on a directory or file.
         */
        REQ("ftw64.11", "errno be set to any error", true);

        /*
         * In addition, if the function pointed to by fn encounters system
         * errors, errno may be set accordingly.
         */
        REQ("ftw64.14", "errno may be set to system error", true);

        return true;
    }

    FILTER_CLEAN;
}

void onFTW64(CallContext context, CString *path, FTWFunction *fn, IntT ndirs,
             ErrorCode *errno, IntT ftw64_spec)
{
    onFTW(context, path, fn, ndirs, errno, ftw64_spec);
}

/*
Linux Standard Base Core Specification 3.0
Copyright (c) 2004, 2005 Free Standards Group

 refers

The Open Group Base Specifications Issue 6
IEEE Std 1003.1, 2004 Edition
Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved

NAME

    nftw - walk a file tree

SYNOPSIS

    #include <ftw.h>

    int nftw(const char *path, int (*fn)(const char *,
        const struct stat *, int, struct FTW *), int fd_limit, int flags);

DESCRIPTION

    The nftw() function shall recursively descend the directory hierarchy
    rooted in path. The nftw() function has a similar effect to ftw() except
    that it takes an additional argument flags, which is a bitwise-inclusive OR
    of zero or more of the following flags:

    FTW_CHDIR
        If set, nftw() shall change the current working directory to each
        directory as it reports files in that directory. If clear, nftw() shall
        not change the current working directory.
    FTW_DEPTH
        If set, nftw() shall report all files in a directory before reporting
        the directory itself. If clear, nftw() shall report any directory
        before reporting the files in that directory.
    FTW_MOUNT
        If set, nftw() shall only report files in the same file system as path.
        If clear, nftw() shall report all files encountered during the walk.
    FTW_PHYS
        If set, nftw() shall perform a physical walk and shall not follow
        symbolic links.

    If FTW_PHYS is clear and FTW_DEPTH is set, nftw() shall follow links
    instead of reporting them, but shall not report any directory that would be
    a descendant of itself. If FTW_PHYS is clear and FTW_DEPTH is clear, nftw()
    shall follow links instead of reporting them, but shall not report the
    contents of any directory that would be a descendant of itself.

    At each file it encounters, nftw() shall call the user-supplied function fn
    with four arguments:

    The first argument is the pathname of the object.

    The second argument is a pointer to the stat buffer containing information
    on the object.

    The third argument is an integer giving additional information. Its value
    is one of the following:

    FTW_F
        The object is a file.
    FTW_D
        The object is a directory.
    FTW_DP
        The object is a directory and subdirectories have been visited. (This
        condition shall only occur if the FTW_DEPTH flag is included in flags.)
    FTW_SL
        The object is a symbolic link. (This condition shall only occur if the
        FTW_PHYS flag is included in flags.)
    FTW_SLN
        The object is a symbolic link that does not name an existing file.
        (This condition shall only occur if the FTW_PHYS flag is not included
        in flags.)
    FTW_DNR
        The object is a directory that cannot be read. The fn function shall
        not be called for any of its descendants.
    FTW_NS
        The stat() function failed on the object because of lack of appropriate
        permission. The stat buffer passed to fn is undefined. Failure of
        stat() for any other reason is considered an error and nftw() shall
        return -1.

    The fourth argument is a pointer to an FTW structure. The value of base is
    the offset of the object's filename in the pathname passed as the first
    argument to fn. The value of level indicates depth relative to the root of
    the walk, where the root level is 0.

    The results are unspecified if the application-supplied fn function does
    not preserve the current working directory.

    The argument fd_limit sets the maximum number of file descriptors that
    shall be used by nftw() while traversing the file tree. At most one file
    descriptor shall be used for each directory level.

    The nftw() function need not be reentrant. A function that is not required
    to be reentrant is not required to be thread-safe.

RETURN VALUE

    The nftw() function shall continue until the first of the following
    conditions occurs:

    An invocation of fn shall return a non-zero value, in which case nftw()
    shall return that value.

    The nftw() function detects an error other than [EACCES] (see FTW_DNR and
    FTW_NS above), in which case nftw() shall return -1 and set errno to
    indicate the error.

    The tree is exhausted, in which case nftw() shall return 0.

ERRORS

    The nftw() function shall fail if:

    [EACCES]
        Search permission is denied for any component of path or read
        permission is denied for path, or fn returns -1 and does not reset
        errno.
    [ELOOP]
        A loop exists in symbolic links encountered during resolution of the
        path argument.
    [ENAMETOOLONG]
        The length of the path argument exceeds {PATH_MAX} or a pathname
        component is longer than {NAME_MAX}.
    [ENOENT]
        A component of path does not name an existing file or path is an empty
        string.
    [ENOTDIR]
        A component of path is not a directory.
    [EOVERFLOW]
        A field in the stat structure cannot be represented correctly in the
        current programming environment for one or more files found in the file
        hierarchy.

    The nftw() function may fail if:

    [ELOOP]
        More than {SYMLOOP_MAX} symbolic links were encountered during
        resolution of the path argument.
    [EMFILE]
        {OPEN_MAX} file descriptors are currently open in the calling process.
    [ENAMETOOLONG]
        Pathname resolution of a symbolic link produced an intermediate result
        whose length exceeds {PATH_MAX}.
    [ENFILE]
        Too many files are currently open in the system.

    In addition, errno may be set if the function pointed to by fn causes errno
    to be set.
*/
specification
IntT nftw_spec(CallContext context, CString *path, FTWFunction *fn, IntT fd_limit,
               NFTWFlags flags, ErrorCode *errno)
{
    bool uptodate;
    Bool3 isELOOP;

    ProcessState *process_state = getProcessState_CallContext(context);

    FileSystem *file_system = getFileSystem(context);

    Set *file_tree = getFileTree_NFTW_Path(context, path, flags, &uptodate);

    CString *absolute_path = resolvePath_Ext(context, file_system, path, &isELOOP);

    CString *cwd = isWrong_FileId(process_state->meta.workdir) ? NULL :
        getPath_File(file_system, getFile_FileId(process_state->meta.workdir));

    FILTER("nftw");

    pre
    {
        /* [Consistency of test suite] */
        REQ("", "The fn function is valid", fn != NULL && fn->nftw);

        /*
         * The results are unspecified if the application-supplied fn function
         * does not preserve the current working directory.
         */
        REQ("app.nftw.01", "The fn function shall preserve the cwd", true);

        return true;
    }
    coverage C
    {
        if(!uptodate)
        {
            return { DirectoriesAreNotUptodate, "Directories are not uptodate" };
        }
        else
        {
            return { DirectoriesAreUptodate, "Directories are uptodate" };
        }
    }
    post
    {
        bool fn_returned_minus_one = false;

        Set *processed_file_tree, *non_processed_file_tree;

        if(!uptodate)
        {
            return true;
        }

        processed_file_tree = getProcessedFileTree_FTWFunction(fn);
        non_processed_file_tree = getNonProcessedFileTree_FTWFunction(context, fn);

        traceFormattedUserInfo("nftw_spec: file tree=$(obj)", file_tree);
        traceFormattedUserInfo("nftw_spec: processed file tree=$(obj)", processed_file_tree);
        traceFormattedUserInfo("nftw_spec: non-processed file tree=$(obj)", non_processed_file_tree);

        /*
         * The nftw() function shall continue until the first of the following
         * conditions occurs:
         */
        if(returnedNonZero_FTWFunction(fn))
        {
            int non_zero_call_number = getNonZeroCallNumber_FTWFunction(fn);
            FTWFunctionCall *non_zero_call = getCall_FTWFunction(fn, non_zero_call_number);

            /*
             * An invocation of fn shall return a non-zero value, in which case
             * nftw() shall return that value.
             */
            REQ("nftw.06.01", "nftw() shall stop and return value returned by the fn",
            (
                non_zero_call_number == getCallsNumber_FTWFunction(fn) - 1 &&
                nftw_spec == non_zero_call->result
            ));

            fn_returned_minus_one = non_zero_call->result == -1;
        }
        else if(equals(processed_file_tree, file_tree))
        {
            /* The tree is exhausted, in which case nftw() shall return 0 */
            REQ("nftw.06.03", "nftw() shall return 0", nftw_spec == 0);
        }

        if(*errno == SUT_EACCES)
        {
            /*
             * The nftw() function detects an error other than [EACCES] (see
             * FTW_DNR and FTW_NS above), in which case nftw() shall return -1
             * and set errno to indicate the error.
             */
            REQ("nftw.06.02", "On [EACCES] function should return 0",
            (
                nftw_spec == 0 || returnedNonZero_FTWFunction(fn)
            ));
        }

        ERROR_BEGIN(POSIX_NFTW, "nftw.07.01", !fn_returned_minus_one && nftw_spec == -1, *errno);

            /*
             * The nftw() function shall fail if:
             *
             * [EACCES]
             *
             * Search permission is denied for any component of path or read
             * permission is denied for path, or fn returns -1 and does not
             * reset errno.
             */
            ERROR_SHALL3(POSIX_NFTW, EACCES, "nftw.07.01",
            (
                isEACCES_dir_open(context, file_system, absolute_path)
            ));

            /*
             * The nftw() function shall fail if:
             *
             * [ELOOP]
             *
             * A loop exists in symbolic links encountered during resolution of
             * the path argument.
             */
            ERROR_SHALL3(POSIX_NFTW, ELOOP, "nftw.07.02", isELOOP);

            /*
             * The nftw() function shall fail if:
             *
             * [ENAMETOOLONG]
             *
             * The length of the path argument exceeds {PATH_MAX} or a pathname
             * component is longer than {NAME_MAX}.
             */
            ERROR_SHALL3(POSIX_NFTW, ENAMETOOLONG, "nftw.07.03",
            (
                isENAMETOOLONG(context, path)
            ));

            /*
             * The nftw() function shall fail if:
             *
             * [ENOENT]
             *
             * A component of path does not name an existing file or path is an
             * empty string.
             */
            ERROR_SHALL3(POSIX_NFTW, ENOENT, "nftw.07.04",
            (
                length_CString(path) == 0 ? True_Bool3 :
                    not_Bool3(doesFileExist_FileSystem(file_system, absolute_path))
            ));

            /*
             * The nftw() function shall fail if:
             *
             * [ENOTDIR]
             *
             * A component of path is not a directory.
             */
            ERROR_SHALL3(POSIX_NFTW, ENOTDIR, "nftw.07.05",
            (
                isENOTDIR_dir(context, file_system, path)
            ));

            /*
             * The nftw() function shall fail if:
             *
             * [EOVERFLOW]
             *
             * A field in the stat structure cannot be represented correctly in
             * the current programming environment for one or more files found
             * in the file hierarchy.
             */
            ERROR_SHALL3(POSIX_NFTW, EOVERFLOW, "nftw.07.06",
            (
                // TODO:
                Unknown_Bool3
            ));

            /*
             * The nftw() function may fail if:
             *
             * [ELOOP]
             *
             * More than {SYMLOOP_MAX} symbolic links were encountered during
             * resolution of the path argument.
             */
            ERROR_MAY3(POSIX_NFTW, ELOOP, "nftw.08.01", isELOOP);

            /*
             * The nftw() function may fail if:
             *
             * [EMFILE]
             *
             * {OPEN_MAX} file descriptors are currently open in the calling
             * process.
             */
            ERROR_MAY3(POSIX_NFTW, EMFILE, "nftw.08.02",
            (
                @isOpenFileDescNumberExceedMax(context)
            ));

            /*
             * The nftw() function may fail if:
             *
             * [ENAMETOOLONG]
             *
             * Pathname resolution of a symbolic link produced an intermediate
             * result whose length exceeds {PATH_MAX}.
             */
            ERROR_MAY3(POSIX_NFTW, ENAMETOOLONG, "nftw.08.03",
            (
                isENAMETOOLONG(context, absolute_path)
            ));

            /*
             * The nftw() function may fail if:
             *
             * [ENFILE]
             *
             * Too many files are currently open in the system.
             */
            ERROR_MAY3(POSIX_NFTW, ENFILE, "nftw.08.04", Unknown_Bool3);

        ERROR_END();

        /* [Implicit requirement] */
        REQ("", "No duplicates",
        (
            size_Set(processed_file_tree) == getCallsNumber_FTWFunction(fn)
        ));

        /*
         * The nftw() function shall recursively descend the directory
         * hierarchy rooted in path.
         */
        addAll_Set(processed_file_tree, non_processed_file_tree);

        REQ("nftw.01", "nftw() function shall recursively descent the path",
        (
            *errno == SUT_EACCES
            ||
            (
                returnedNonZero_FTWFunction(fn) ?
                    containsAll_Set(file_tree, processed_file_tree) :
                    equals(processed_file_tree, file_tree)
            )
        ));

        /*
         * At each file it encounters, nftw() shall call the user-supplied
         * function fn with four arguments:
         */
        REQ( "nftw.03", "nftw() shall call fn for objects in file tree",
             ( traceFunctionCall( context,
                                  checkCallsFlags_NFTWFunction( context, path, fn, flags, cwd, * errno == SUT_EACCES ),
                                  true,
                                  "checkCallsFlags_NFTWFunction in req nftw.03",
                                  "path", toString( path ),
                                  "fn", toString( fn ),
                                  "flags.phys ", valueOfBool_String( flags.phys  ),
                                  "flags.mount", valueOfBool_String( flags.mount ),
                                  "flags.depth", valueOfBool_String( flags.depth ),
                                  "flags.chdir", valueOfBool_String( flags.chdir ),
                                  "cwd", toString( cwd ),
                                  "* errno == SUT_EACCES", valueOfBool_String( * errno == SUT_EACCES ),
                                  NULL
                                ) &&
               traceFunctionCall( context,
                                  checkCallsOrder_NFTWFunction( context, fn, flags ),
                                  true,
                                  "checkCallsOrder_NFTWFunction in req nftw.03",
                                  "fn", toString( fn ),
                                  "flags.phys ", valueOfBool_String( flags.phys  ),
                                  "flags.mount", valueOfBool_String( flags.mount ),
                                  "flags.depth", valueOfBool_String( flags.depth ),
                                  "flags.chdir", valueOfBool_String( flags.chdir ),
                                  NULL
                                )
             )
           );

        /*
         * The argument fd_limit sets the maximum number of file descriptors
         * that shall be used by nftw() while traversing the file tree.
         */
        REQ("nftw.04", "The fd_limit shall specify the maximum number of file descriptors",
            TODO_REQ()
        );

        /*
         * At most one file descriptor shall be used for each directory level.
         */
        REQ("nftw.05", "At moust one file descriptor shall be used for each directory level",
            TODO_REQ()
        );

        /*
         * In addition, errno may be set if the function pointed to by fn
         * causes errno to be set.
         */
        REQ("nftw.09", "errno may be set to any error", true);

        return true;
    }

    FILTER_CLEAN;
}

void onNFTW(CallContext context, CString *path, FTWFunction *fn, IntT fd_limit,
            NFTWFlags flags, ErrorCode *errno, IntT nftw_spec)
{
    onFTW(context, path, fn, fd_limit, errno, nftw_spec);
}

specification
IntT nftw64_spec(CallContext context, CString *path, FTWFunction *fn, IntT fd_limit,
                 NFTWFlags flags, ErrorCode *errno)
{
    bool uptodate;
    Bool3 isELOOP;

    ProcessState *process_state = getProcessState_CallContext(context);

    FileSystem *file_system = getFileSystem(context);

    Set *file_tree = getFileTree_NFTW_Path(context, path, flags, &uptodate);

    CString *absolute_path = resolvePath_Ext(context, file_system, path, &isELOOP);

    CString *cwd = isWrong_FileId(process_state->meta.workdir) ? NULL :
        getPath_File(file_system, getFile_FileId(process_state->meta.workdir));

    FILTER("nftw64");

    pre
    {
        /* [Consistency of test suite] */
        REQ("", "The fn function is valid", fn != NULL && fn->nftw);

        /*
         * The results are unspecified if the application-supplied fn function
         * does not preserve the current working directory.
         */
        REQ("app.nftw64.01", "The fn function shall preserve the cwd", true);

        return true;
    }
    coverage C
    {
        if(!uptodate)
        {
            return { DirectoriesAreNotUptodate, "Directories are not uptodate" };
        }
        else
        {
            return { DirectoriesAreUptodate, "Directories are uptodate" };
        }
    }
    post
    {
        bool fn_returned_minus_one = false;

        Set *processed_file_tree, *non_processed_file_tree;

        if(!uptodate)
        {
            return true;
        }

        processed_file_tree = getProcessedFileTree_FTWFunction(fn);
        non_processed_file_tree = getNonProcessedFileTree_FTWFunction(context, fn);

        traceFormattedUserInfo("nftw64_spec: file tree=$(obj)", file_tree);
        traceFormattedUserInfo("nftw64_spec: processed file tree=$(obj)", processed_file_tree);
        traceFormattedUserInfo("nftw64_spec: non-processed file tree=$(obj)", non_processed_file_tree);

        /*
         * The nftw() function shall continue until the first of the following
         * conditions occurs:
         */
        if(returnedNonZero_FTWFunction(fn))
        {
            int non_zero_call_number = getNonZeroCallNumber_FTWFunction(fn);
            FTWFunctionCall *non_zero_call = getCall_FTWFunction(fn, non_zero_call_number);

            /*
             * An invocation of fn shall return a non-zero value, in which case
             * nftw() shall return that value.
             */
            REQ("nftw64.06.01", "nftw64() shall stop and return value returned by the fn",
            (
                non_zero_call_number == getCallsNumber_FTWFunction(fn) - 1 &&
                nftw64_spec == non_zero_call->result
            ));

            fn_returned_minus_one = non_zero_call->result == -1;
        }
        else if(equals(processed_file_tree, file_tree))
        {
            /* The tree is exhausted, in which case nftw() shall return 0 */
            REQ("nftw64.06.03", "nftw64() shall return 0", nftw64_spec == 0);
        }

        if(*errno==SUT_EACCES)
        {
            /*
             * The nftw() function detects an error other than [EACCES] (see
             * FTW_DNR and FTW_NS above), in which case nftw() shall return -1
             * and set errno to indicate the error.
             */
            REQ("nftw64.06.02", "On [EACCES] function should return 0",
            (
                nftw64_spec == 0 || returnedNonZero_FTWFunction(fn)
            ));
        }

        ERROR_BEGIN(LSB_NFTW64, "nftw64.07.01", !fn_returned_minus_one && nftw64_spec == -1, *errno);

            /*
             * The nftw() function shall fail if:
             *
             * [EACCES]
             *
             * Search permission is denied for any component of path or read
             * permission is denied for path, or fn returns -1 and does not
             * reset errno.
             */
            ERROR_SHALL3(LSB_NFTW64, EACCES, "nftw64.07.01",
            (
                isEACCES_dir_open(context, file_system, absolute_path)
            ));

            /*
             * The nftw() function shall fail if:
             *
             * [ELOOP]
             *
             * A loop exists in symbolic links encountered during resolution of
             * the path argument.
             */
            ERROR_SHALL3(LSB_NFTW64, ELOOP, "nftw64.07.02", isELOOP);

            /*
             * The nftw() function shall fail if:
             *
             * [ENAMETOOLONG]
             *
             * The length of the path argument exceeds {PATH_MAX} or a pathname
             * component is longer than {NAME_MAX}.
             */
            ERROR_SHALL3(LSB_NFTW64, ENAMETOOLONG, "nftw64.07.03",
            (
                isENAMETOOLONG(context, path)
            ));

            /*
             * The nftw() function shall fail if:
             *
             * [ENOENT]
             *
             * A component of path does not name an existing file or path is an
             * empty string.
             */
            ERROR_SHALL3(LSB_NFTW64, ENOENT, "nftw64.07.04",
            (
                length_CString(path) == 0 ? True_Bool3 :
                    not_Bool3(doesFileExist_FileSystem(file_system, absolute_path))
            ));

            /*
             * The nftw() function shall fail if:
             *
             * [ENOTDIR]
             *
             * A component of path is not a directory.
             */
            ERROR_SHALL3(LSB_NFTW64, ENOTDIR, "nftw64.07.05",
            (
                isENOTDIR_dir(context, file_system, path)
            ));

            /*
             * The nftw() function shall fail if:
             *
             * [EOVERFLOW]
             *
             * A field in the stat structure cannot be represented correctly in
             * the current programming environment for one or more files found
             * in the file hierarchy.
             */
            ERROR_SHALL3(LSB_NFTW64, EOVERFLOW, "nftw64.07.06",
            (
                // TODO:
                Unknown_Bool3
            ));

            /*
             * The nftw() function may fail if:
             *
             * [ELOOP]
             *
             * More than {SYMLOOP_MAX} symbolic links were encountered during
             * resolution of the path argument.
             */
            ERROR_MAY3(LSB_NFTW64, ELOOP, "nftw64.08.01", isELOOP);

            /*
             * The nftw() function may fail if:
             *
             * [EMFILE]
             *
             * {OPEN_MAX} file descriptors are currently open in the calling
             * process.
             */
            ERROR_MAY3(LSB_NFTW64, EMFILE, "nftw64.08.02",
            (
                @isOpenFileDescNumberExceedMax(context)
            ));

            /*
             * The nftw() function may fail if:
             *
             * [ENAMETOOLONG]
             *
             * Pathname resolution of a symbolic link produced an intermediate
             * result whose length exceeds {PATH_MAX}.
             */
            ERROR_MAY3(LSB_NFTW64, ENAMETOOLONG, "nftw64.08.03",
            (
                isENAMETOOLONG(context, absolute_path)
            ));

            /*
             * The nftw() function may fail if:
             *
             * [ENFILE]
             *
             * Too many files are currently open in the system.
             */
            ERROR_MAY3(LSB_NFTW64, ENFILE, "nftw64.08.04", Unknown_Bool3);

        ERROR_END();

        /* [Implicit requirement] */
        REQ("", "No duplicates",
        (
            size_Set(processed_file_tree) == getCallsNumber_FTWFunction(fn)
        ));

        /*
         * The nftw() function shall recursively descend the directory
         * hierarchy rooted in path.
         */
        addAll_Set(processed_file_tree, non_processed_file_tree);

        REQ("nftw64.01", "nftw64() function shall recursively descent the path",
        (
            *errno == SUT_EACCES
            ||
            (
                returnedNonZero_FTWFunction(fn) ?
                    containsAll_Set(file_tree, processed_file_tree) :
                    equals(processed_file_tree, file_tree)
            )
        ));

        /*
         * At each file it encounters, nftw() shall call the user-supplied
         * function fn with four arguments:
         *
         * The first argument is the pathname of the object.
         *
         * The second argument is a pointer to the stat buffer containing
         * information on the object.
         *
         * The fourth argument is a pointer to an FTW structure. The value of
         * base is the offset of the object's filename in the pathname passed
         * as the first argument to fn. The value of level indicates depth
         * relative to the root of the walk, where the root level is 0.
         */
        REQ( "nftw64.03", "nftw64() shall call fn for objects in file tree",
             ( traceFunctionCall( context,
                                  checkCallsFlags_NFTWFunction( context, path, fn, flags, cwd, * errno == SUT_EACCES ),
                                  true,
                                  "checkCallsFlags_NFTWFunction in req nftw.03",
                                  "path", toString( path ),
                                  "fn", toString( fn ),
                                  "flags.phys ", valueOfBool_String( flags.phys  ),
                                  "flags.mount", valueOfBool_String( flags.mount ),
                                  "flags.depth", valueOfBool_String( flags.depth ),
                                  "flags.chdir", valueOfBool_String( flags.chdir ),
                                  "cwd", toString( cwd ),
                                  "* errno == SUT_EACCES", valueOfBool_String( * errno == SUT_EACCES ),
                                  NULL
                                ) &&
               traceFunctionCall( context,
                                  checkCallsOrder_NFTWFunction( context, fn, flags ),
                                  true,
                                  "checkCallsOrder_NFTWFunction in req nftw.03",
                                  "fn", toString( fn ),
                                  "flags.phys ", valueOfBool_String( flags.phys  ),
                                  "flags.mount", valueOfBool_String( flags.mount ),
                                  "flags.depth", valueOfBool_String( flags.depth ),
                                  "flags.chdir", valueOfBool_String( flags.chdir ),
                                  NULL
                                )
             )
           );

        /*
         * The argument fd_limit sets the maximum number of file descriptors
         * that shall be used by nftw() while traversing the file tree.
         */
        REQ("nftw64.04", "The fd_limit shall specify the maximum number of file descriptors",
            TODO_REQ()
        );

        /*
         * At most one file descriptor shall be used for each directory level.
         */
        REQ("nftw64.05", "At moust one file descriptor shall be used for each directory level",
            TODO_REQ()
        );

        /*
         * In addition, errno may be set if the function pointed to by fn
         * causes errno to be set.
         */
        REQ("nftw64.09", "errno may be set to any error", true);

        return true;
    }

    FILTER_CLEAN;
}

void onNFTW64(CallContext context, CString *path, FTWFunction *fn, IntT fd_limit,
              NFTWFlags flags, ErrorCode *errno, IntT nftw64_spec)
{
    onFTW(context, path, fn, fd_limit, errno, nftw64_spec);
}

/*****************************************************************************/
/**                            FTWStructure Type                            **/
/*****************************************************************************/

/*
 * This type represents FTW structure.
 *
 * The Open Group Base Specifications Issue 6
 * IEEE Std 1003.1, 2004 Edition
 * Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved
 *
 * See 'Base Definitions / Headers / <ftw.h>'
 */
specification typedef struct FTWStructure FTWStructure = {};

FTWStructure* create_FTWStructure(IntT base, IntT level)
{
    return create(&type_FTWStructure, base, level);
}

/*****************************************************************************/
/**                            FTWFunction Type                             **/
/*****************************************************************************/
specification typedef struct FTWFunctionCall FTWFunctionCall = {};

FTWFunctionCall* create_FTWFunctionCall
(
    CString *path,
    FileStatus *file_stat,
    FTWFunctionFlag flag,
    FTWStructure *ftw_struct,
    CString *cwd,
    IntT result
)
{
    return create(&type_FTWFunctionCall, path, file_stat, flag, ftw_struct, cwd, result);
}

FTWFunctionCall* default_FTWFunctionCall(void)
{
    return create_FTWFunctionCall(NULL, NULL, SUT_FTW_UNKNOWN, NULL, NULL, 0);
}

specification typedef struct FTWFunction FTWFunction = {};

FTWFunction* create_FTWFunction(bool nftw, FTWFunctionType type, IntT param, IntT result)
{
    return create(&type_FTWFunction, nftw, type, param, result,
        create_List(&type_FTWFunctionCall));
}

FTWFunction* default_FTWFunction(void)
{
    return create_FTWFunction(false, ConstFTWFunction, 0, 0);
}

FTWFunction* default_NFTWFunction(void)
{
    return create_FTWFunction(true, ConstFTWFunction, 0, 0);
}

void reset_FTWFunction(FTWFunction *fn)
{
    assertion(fn != NULL, "reset_FTWFunction: fn is NULL");

    clear_List(fn->calls);
}

FTWFunctionCall* getCall_FTWFunction(FTWFunction *fn, int i)
{
    assertion(fn != NULL,
        "getCall_FTWFunction: fn is NULL");
    assertion(i >= 0 && i < getCallsNumber_FTWFunction(fn),
        "getCall_FTWFunction: i is out of range");

    return get_List(fn->calls, i);
}

int getCallsNumber_FTWFunction(FTWFunction *fn)
{
    assertion(fn != NULL, "getCallsNumber_FTWFunction: fn is NULL");

    return size_List(fn->calls);
}

bool returnedNonZero_FTWFunction(FTWFunction *fn)
{
    int i, size;

    assertion(fn != NULL, "returnedNonZero_FTWFunction: fn is NULL");

    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

        if(fn_call->result != 0)
        {
            return true;
        }
    }

    return false;
}

int getNonZeroCallNumber_FTWFunction(FTWFunction *fn)
{
    int i, size;

    assertion(fn != NULL, "getNonZeroCallNumber_FTWFunction: fn is NULL");

    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

        if(fn_call->result != 0)
        {
            return i;
        }
    }

    return -1;
}

Set* getProcessedFileTree_FTWFunction(FTWFunction *fn)
{
    int i, size;
    Set *res;

    assertion(fn != NULL, "getProcessedFileTree_FTWFunction: fn is NULL");

    res = create_Set(&type_CString);
    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

        add_Set(res, fn_call->path);
    }

    return res;
}

Set* getNonProcessedFileTree_FTWFunction(CallContext context, FTWFunction *fn)
{
    int i, size;
    Set *res;

    assertion(fn != NULL, "getNonProcessedFileTree_FTWFunction: fn is NULL");

    res = create_Set(&type_CString);
    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

        if(fn_call->flag == SUT_FTW_DNR || fn_call->flag == SUT_FTW_NS)
        {
            Set *file_subtree = getFileTree_FTW_Path(context, fn_call->path, NULL);

            if(file_subtree != NULL)
            {
                addAll_Set(res, file_subtree);
            }
        }
    }

    return res;
}

static bool isDescendant_Path(CString *path, CString *descendant)
{
    int i, size;

    List *path_list = split_Path(path);
    List *descendant_list = split_Path(descendant);

    if((size = size_List(path_list)) >= size_List(descendant_list))
    {
        return false;
    }

    for(i = 0; i < size; i++)
    {
        if(!equals(get_List(path_list, i), get_List(descendant_list, i)))
        {
            return false;
        }
    }

    return true;
}

static bool doesProcessedDescendantExist_FTWFunction(FTWFunction *fn, CString *path)
{
    int i, size;

    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

        if(isDescendant_Path(path, fn_call->path))
        {
            return true;
        }
    }

    return false;
}

bool checkCallsFlags_FTWFunction(CallContext context, FTWFunction *fn)
{
    int i, size;
    bool unknown;
    Bool3 res = True_Bool3;
    FileSystem *file_system = getFileSystem(context);

    assertion(fn != NULL, "checkCallsFlags_FTWFunction: fn is NULL");
    assertion(!fn->nftw, "checkCallsFlags_FTWFunction: fn is nftw");

    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

        if(unknown = fn_call->file_stat->kind == UnknownFileKind)
        {
            res = Unknown_Bool3;
        }

        /*
         * Possible values of the integer, defined in the <ftw.h> header, are:
         */
        switch(fn_call->flag)
        {
        case SUT_FTW_D:
            {
                if(!unknown)
                {
                    /*
                     * FTW_D
                     *
                     * For a directory.
                     */
                    REQ("ftw.03.01;ftw64.03.01", "The file is directory",
                    (
                        fn_call->file_stat->kind == DirectoryFile
                    ));
                }
            }
            break;
        case SUT_FTW_DNR:
            {
                File *file = getFile_FileSystem(file_system, fn_call->path);
                FilePermission *perm = getProcessAccessOnFile(context, file);

                if(!unknown && perm != NULL)
                {
                    /*
                     * FTW_DNR
                     *
                     * For a directory that cannot be read.
                     */
                    REQ("ftw.03.02;ftw64.03.02", "The file is a directory",
                    (
                        fn_call->file_stat->kind == DirectoryFile
                    ));

                    REQ("ftw.03.02;ftw64.03.02", "The directory can not be read",
                    (
                        !perm->read
                    ));
                }
            }
            break;
        case SUT_FTW_F:
            {
                if(!unknown)
                {
                    /*
                     * FTW_F
                     *
                     * For a file.
                     */
                    REQ("ftw.03.03;ftw64.03.03",
                        "The file is not a directory or a symbolic link",
                    (
                        fn_call->file_stat->kind != DirectoryFile &&
                        fn_call->file_stat->kind != SymbolicLinkFile
                    ));
                }
            }
            break;
        case SUT_FTW_SL:
            {
                if(!unknown)
                {
                    /*
                     * FTW_SL
                     *
                     * For a symbolic link (but see also FTW_NS below).
                     */
                    REQ("ftw.03.04;ftw64.03.04", "The file is a symbolic link",
                    (
                        fn_call->file_stat->kind == SymbolicLinkFile
                    ));
                }
            }
            break;
        case SUT_FTW_NS:
            {
                /*
                 * If the integer is FTW_NS, the stat structure contains
                 * undefined values.
                 */
                REQ("ftw.05;ftw64.05", "The stat structure is undefined", true);

                /*
                 * FTW_NS
                 *
                 * For an object other than a symbolic link on which stat()
                 * could not successfully be executed.
                 */
                REQ("ftw.03.05.01;ftw64.03.05",
                    "stat() failed for object other than a symbolic link", true);

                /*
                 * FTW_NS
                 *
                 * If the object is a symbolic link and stat() failed, it is
                 * unspecified whether ftw() passes FTW_SL or FTW_NS to the
                 * user-supplied function.
                 */
                REQ("ftw.03.05.02;ftw64.03.05.02", "stat() failed for a symbolic link", true);
            }
            break;
        default:
            {
                /*
                 * Possible values of the integer, defined in the <ftw.h>
                 * header, are:
                 */
                REQ("ftw.03;ftw64.03", "The flag shall have known value", false);
            }
        }
    }

    return res != False_Bool3 ? true : false;
}

bool checkCallsFlags_NFTWFunction(CallContext context, CString *path, FTWFunction *fn,
                                  NFTWFlags flags, CString *cwd, bool isAccessDenied)
{
    int i, size;
    bool unknown;
    Bool3 res;
    File *root;
    FileSystem *file_system;

    assertion(fn != NULL, "checkCallsFlags_NFTWFunction: fn is NULL");
    assertion(fn->nftw, "checkCallsFlags_NFTWFunction: fn is ftw");

    res = True_Bool3;
    file_system = getFileSystem(context);
    root = getFile_FileSystem(file_system, path);

    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);
        File *file = getFile_FileSystem(file_system, fn_call->path);

        traceFormattedUserInfo("checkCallsFlags_NFTWFunction: call=$(obj)", fn_call);

        /*
         * At each file it encounters, nftw() shall call the user-supplied
         * function fn with four arguments:
         */

        /* The first argument is the pathname of the object. */
        REQ("nftw.03.01;nftw64.03.01", "The path shall not be NULL",
        (
            fn_call->path != NULL
        ));

        /*
         * The second argument is a pointer to the stat buffer containing
         * information on the object.
         */
        REQ("nftw.03.02;nftw64.03.02", "The stat buffer shall not be NULL",
        (
            fn_call->path != NULL
        ));

        /*
         * The fourth argument is a pointer to an FTW structure. The value of
         * base is the offset of the object's filename in the pathname passed
         * as the first argument to fn. The value of level indicates depth
         * relative to the root of the walk, where the root level is 0.
         */

        /*
         * The fourth argument is a pointer to an FTW structure. The value of
         * base is the offset of the object's filename in the pathname passed
         * as the first argument to fn. The value of level indicates depth
         * relative to the root of the walk, where the root level is 0.
         */
        REQ("nftw.03.04;nftw64.03.04", "The FTW structure shall not be NULL",
        (
            fn_call->ftw_struct != NULL
        ));

        traceFormattedUserInfo("checkCallsFlags_NFTWFunction: base=(%d, %d)",
            fn_call->ftw_struct->base, getBase_Path(fn_call->path));

        REQ("nftw.03.04;nftw64.03.04", "The value of base shall be the offset",
        (
            fn_call->ftw_struct->base == getBase_Path(fn_call->path)
        ));

        traceFormattedUserInfo("checkCallsFlags_NFTWFunction: level=(%d, %d)",
            fn_call->ftw_struct->level, getLevel_Path(path, fn_call->path));

        REQ("nftw.03.04;nftw64.03.04", "The value of level shall be the depth",
        (
            fn_call->ftw_struct->level == getLevel_Path(path, fn_call->path)
        ));

        if(unknown = fn_call->file_stat->kind == UnknownFileKind)
        {
            res = Unknown_Bool3;
        }

        /*
         * The nftw() function has a similar effect to ftw() except that it
         * takes an additional argument flags, which is a bitwise-inclusive OR
         * of zero or more of the following flags:
         *
         * FTW_CHDIR
         */
        if(flags.chdir)
        {
            CString *parent = fn_call->file_stat->kind != DirectoryFile ?
                getParentDir_Path(fn_call->path) : fn_call->path;

            traceFormattedUserInfo("checkCallsFlags_NFTWFunction: cwd=$(obj)", fn_call->cwd);
            traceFormattedUserInfo("checkCallsFlags_NFTWFunction: parent=$(obj)", parent);

            if(!isAccessDenied)
            {
                /*
                 * If set, nftw() shall change the current working directory to
                 * each directory as it reports files in that directory.
                 */
                REQ("nftw.02.01.01;nftw64.02.01.01", "nftw() shall change the cwd",
                (
                    equals(fn_call->cwd, parent)
                ));
            }
        }
        else
        {
            if(cwd == NULL)
            {
                res = Unknown_Bool3;
            }
            else
            {
                if(!isAccessDenied)
                {
                    /*
                     * If clear, nftw() shall not change the current working
                     * directory.
                     */
                    REQ("nftw.02.01.02;nftw64.02.01.02", "nftw() shall not change the cwd",
                    (
                        equals(fn_call->cwd, cwd)
                    ));
                }
            }
        }

        /*
         * The nftw() function has a similar effect to ftw() except that it
         * takes an additional argument flags, which is a bitwise-inclusive OR
         * of zero or more of the following flags:
         *
         * FTW_MOUNT
         */
        if(flags.mount)
        {
            if(fn_call->flag == SUT_FTW_NS)
            {
                res = Unknown_Bool3;
            }
            else
            {
                if(root->dev != NULL)
                {
                    /*
                     * If set, nftw() shall only report files in the same file
                     * system as path.
                     */
                    REQ("nftw.02.03.01;nftw64.02.03.01",
                        "nftw() shall report files in the same file system",
                    (
                        equals(root->dev, create_DevTObj(fn_call->file_stat->dev))
                    ));
                }
            }
        }
        else
        {
            /*
             * If clear, nftw() shall report all files encountered during the
             * walk.
             */
            REQ("nftw.02.03.02;nftw64.02.03.02", "nftw() shall report all files", true);
        }

        /*
         * The nftw() function has a similar effect to ftw() except that it
         * takes an additional argument flags, which is a bitwise-inclusive OR
         * of zero or more of the following flags:
         *
         * FTW_PHYS
         */
        if(flags.phys)
        {
            File *descendant = getFile_FileSystem(file_system, fn_call->path);
            File *directory = getFile_FileSystem(file_system, path);

            if(descendant!=NULL && directory!=NULL)
            {
                /*
                 * If set, nftw() shall perform a physical walk and shall not
                 * follow symbolic links.
                 */
                REQ("nftw.02.04;nftw64.02.04", "nftw() shall perform a physical walk",
                (
                    isDescendantOf_Directory(file_system, descendant, directory) != False_Bool3
                ));
            }
        }
        else
        {
            if(flags.depth)
            {
                /*
                 * If FTW_PHYS is clear and FTW_DEPTH is set, nftw() shall
                 * follow links instead of reporting them, but shall not report
                 * any directory that would be a descendant of itself.
                 */
                REQ("nftw.02.05;nftw64.02.05", "nftw() shall follow links",
                (
                    fn_call->flag != SUT_FTW_SL && fn_call->flag != SUT_FTW_SLN
                ));

                if(file != NULL && isOfKind_File(file, DirectoryFile) == True_Bool3)
                {
                    REQ("nftw.02.05;nftw64.02.05",
                        "nftw() shall not report descendants of itself",
                    (
                        // TODO: Unclear
                        // isDescendantOfItself_Directory_SymLinks(file_system, file) != True_Bool3
                        true
                    ));
                }
            }
            else
            {
                /*
                 * If FTW_PHYS is clear and FTW_DEPTH is clear, nftw() shall
                 * follow links instead of reporting them, but shall not report
                 * the contents of any directory that would be a descendant of
                 * itself.
                 */
                REQ("nftw.02.06;nftw64.02.06", "nftw() shall follow links",
                (
                    fn_call->flag != SUT_FTW_SL && fn_call->flag != SUT_FTW_SLN
                ));

                if(file != NULL && isOfKind_File(file, DirectoryFile) == True_Bool3)
                {
                    REQ("nftw.02.06;nftw64.02.06",
                        "nftw() shall not report descendants of itself",
                    (
                        // TODO: Unclear
                        // isDescendantOfItself_Directory_SymLinks(file_system, file) != True_Bool3
                        true
                    ));
                }
            }
        }

        /*
         * At each file it encounters, nftw() shall call the user-supplied
         * function fn with four arguments:
         *
         * The third argument is an integer giving additional information. Its
         * value is one of the following:
         */
        switch(fn_call->flag)
        {
        case SUT_FTW_D:
            {
                if(!unknown)
                {
                    /*
                     * FTW_D
                     *
                     * The object is a directory.
                     */
                    REQ("nftw.03.03.02;nftw64.03.03.02", "The file is a directory",
                    (
                        fn_call->file_stat->kind == DirectoryFile
                    ));
                }
            }
            break;
        case SUT_FTW_DNR:
            {
                if( file != NULL )
                {
                    FilePermission *perm = getProcessAccessOnFile(context, file);

                    if(!unknown && perm != NULL)
                    {
                        /*
                         * FTW_DNR
                         *
                         * The object is a directory that cannot be read.
                         */
                        REQ("nftw.03.03.06.01;nftw64.03.03.06.01", "The file is a directory",
                        (
                            fn_call->file_stat->kind == DirectoryFile
                        ));

                        REQ("nftw.03.03.03;nftw64.03.03.03", "The directory can not be read",
                        (
                            !perm->read
                        ));
                    }
                }
            }
            break;
        case SUT_FTW_F:
            {
                /*
                 * FTW_F
                 *
                 * The object is a file.
                 */
                if(!unknown)
                {
                    /*
                     * FTW_F
                     *
                     * The object is a file.
                     */
                    REQ("nftw.03.03.01;nftw64.03.03.01",
                        "The file is not a directory or a symbolic link",
                    (
                        fn_call->file_stat->kind != DirectoryFile &&
                        fn_call->file_stat->kind != SymbolicLinkFile
                    ));
                }

            }
            break;
        case SUT_FTW_SL:
            {
                /*
                 * FTW_SL
                 *
                 * The object is a symbolic link. (This condition shall only
                 * occur if the FTW_PHYS flag is included in flags.)
                 */
                REQ("nftw.03.03.04;nftw64.03.03.04", "FTW_PHYS is included in flags",
                (
                    flags.phys
                ));

                if(!unknown)
                {
                    REQ("nftw.03.03.04;nftw64.03.03.04", "The file is a symbolic link",
                    (
                        fn_call->file_stat->kind == SymbolicLinkFile
                    ));
                }
            }
            break;
        case SUT_FTW_NS:
            {
                /*
                 * FTW_NS
                 *
                 * The stat() function failed on the object because of lack of
                 * appropriate permission. The stat buffer passed to fn is
                 * undefined. Failure of stat() for any other reason is
                 * considered an error and nftw() shall return -1.
                 */
                REQ("nftw.03.03.07;nftw64.03.03.07", "stat() failed",
                (
                    shall_isEACCES_xstat(context, file_system, fn_call->path) != False_Bool3
                ));
            }
            break;
        case SUT_FTW_DP:
            {
                /*
                 * FTW_DP
                 *
                 * The object is a directory and subdirectories have been
                 * visited. (This condition shall only occur if the FTW_DEPTH
                 * flag is included in flags.)
                 */
                REQ("nftw.03.03.03;nftw64.03.03.03", "FTW_DEPTH is included in flags",
                (
                    flags.depth
                ));

                if(!unknown)
                {
                    REQ("nftw.03.03.03;nftw64.03.03.03", "The file is a directory",
                    (
                        fn_call->file_stat->kind == DirectoryFile
                    ));
                }
            }
            break;
        case SUT_FTW_SLN:
            {
                Bool3 eloop;
                CString *resolved_path;

                /*
                 * FTW_SLN
                 *
                 * The object is a symbolic link that does not name an existing
                 * file. (This condition shall only occur if the FTW_PHYS flag
                 * is not included in flags.)
                 */
                REQ("nftw.03.03.05;nftw64.03.03.05", "FTW_PHYS is not included in flags",
                (
                    !flags.phys
                ));

                if(!unknown)
                {
                    REQ("nftw.03.03.05;nftw64.03.03.05", "The file is a symbolic link",
                    (
                        fn_call->file_stat->kind == SymbolicLinkFile
                    ));
                }

                resolved_path = resolveAbsolutePath_Ext
                    (context, file_system, fn_call->path, &eloop);

                REQ("nftw.03.03.05;nftw64.03.03.05", "The link shall not contain loops",
                (
                    eloop != True_Bool3
                ));

                REQ("nftw.03.03.05;nftw64.03.03.05", "The link does not name an existing file",
                (
                    doesFileExist_FileSystem(file_system, resolved_path) != True_Bool3
                ));
            }
            break;
        default:
            {
                /*
                 * At each file it encounters, nftw() shall call the
                 * user-supplied function fn with four arguments:
                 *
                 * The third argument is an integer giving additional
                 * information. Its value is one of the following:
                 */
                REQ("nftw.03.03;nftw64.03.03", "The flag shall have known value", false);
            }
        }
    }

    return res != False_Bool3 ? true : false;
}

bool checkCallsOrder_FTWFunction(CallContext context, FTWFunction *fn)
{
    int i, j, size;

    assertion(fn != NULL, "checkCallsOrder_FTWFunction: fn is NULL");
    assertion(!fn->nftw, "checkCallsOrder_FTWFunction: fn is nftw");

    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

        if(fn_call->flag == SUT_FTW_DNR)
        {
            /*
             * If the integer is FTW_DNR, descendants of that directory shall
             * not be processed.
             */
            IMPLEMENT_REQ("ftw.04;ftw64.04");

            if(doesProcessedDescendantExist_FTWFunction(fn, fn_call->path))
            {
                return False_Bool3;
            }
        }

        /*
         * The ftw() function shall visit a directory before visiting any of
         * its descendants.
         */
        IMPLEMENT_REQ("ftw.06;ftw64.06");

        for(j = i + 1; j < size; j++)
        {
            FTWFunctionCall *next_fn_call = getCall_FTWFunction(fn, j);

            if(isDescendant_Path(next_fn_call->path, fn_call->path))
            {
                return False_Bool3;
            }
        }
    }

    return True_Bool3;
}

bool checkCallsOrder_NFTWFunction(CallContext context, FTWFunction *fn, NFTWFlags flags)
{
    int i, j, size;

    assertion(fn != NULL, "checkCallsOrder_NFTWFunction: fn is NULL");
    assertion(fn->nftw, "checkCallsOrder_NFTWFunction: fn is ftw");

    size = getCallsNumber_FTWFunction(fn);
    for(i = 0; i < size; i++)
    {
        FTWFunctionCall *fn_call = getCall_FTWFunction(fn, i);

        if(fn_call->flag == SUT_FTW_DNR)
        {
            /*
             * FTW_DNR
             *
             * The fn function shall not be called for any of its descendants.
             */
            IMPLEMENT_REQ("nftw.03.03.06.02;nftw64.03.03.06.02");

            if(doesProcessedDescendantExist_FTWFunction(fn, fn_call->path))
            {
                return False_Bool3;
            }
        }

        if(flags.depth)
        {
            /*
             * FTW_DEPTH
             *
             * If set, nftw() shall report all files in a directory before
             * reporting the directory itself.
             */
            IMPLEMENT_REQ("nftw.02.02.01;nftw64.02.02.01");

            for(j = i + 1; j < size; j++)
            {
                FTWFunctionCall *next_fn_call = getCall_FTWFunction(fn, j);

                if(isDescendant_Path(fn_call->path, next_fn_call->path))
                {
                    return False_Bool3;
                }
            }
        }
        else
        {
            /*
             * FTW_DEPTH
             *
             * If clear, nftw() shall report any directory before reporting the
             * files in that directory.
             */
            IMPLEMENT_REQ("nftw.02.02.02;nftw64.02.02.02");

            for(j = i + 1; j < size; j++)
            {
                FTWFunctionCall *next_fn_call = getCall_FTWFunction(fn, j);

                if(isDescendant_Path(next_fn_call->path, fn_call->path))
                {
                    return False_Bool3;
                }
            }
        }
    }

    return True_Bool3;
}

/*****************************************************************************/
/**                              NFTWFlags Type                             **/
/*****************************************************************************/

/*
 * This type represents nftw() and nftw64() functions flags.
 *
 * The Open Group Base Specifications Issue 6
 * IEEE Std 1003.1, 2004 Edition
 * Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved
 *
 * See 'Base Definitions / Headers / <ftw.h>'
 */
NFTWFlags default_NFTWFlags(void)
{
    NFTWFlags flags = { false, false, false, false };

    return flags;
}

specification typedef NFTWFlags NFTWFlagsObj = {};

NFTWFlagsObj* create_NFTWFlagsObj(NFTWFlags flags)
{
    return create
    (
        &type_NFTWFlagsObj,
        flags.phys,
        flags.mount,
        flags.depth,
        flags.chdir
    );
}

NFTWFlagsObj* default_NFTWFlagsObj(void)
{
    return create_NFTWFlagsObj(default_NFTWFlags());
}

/*****************************************************************************/
/**                            Helper Functions                             **/
/*****************************************************************************/
Bool3 checkFileDescriptorsLimit(CallContext context, IntT fd_limit)
{
    /* The argument should be in the range [1, {OPEN_MAX}] */
    LongT open_max = getSystemConfigurationValue(context, SUT_SC_OPEN_MAX);

    if(fd_limit < 1)
    {
        return False_Bool3;
    }

    if(open_max == SC_VALUE_NO_LIMIT)
    {
        return True_Bool3;
    }

    if(open_max == SC_VALUE_UNKNOWN)
    {
        return True_Bool3;
    }

    return (LongT)fd_limit <= open_max;
}

static bool processDirectory_getFileTree_NFTW_Path
(
    FileSystem *file_system,
    File *root,
    File *directory,
    NFTWFlags flags,
    Set *result,
    Set *processed
);

static bool processSymLink_getFileTree_NFTW_Path
(
    FileSystem *file_system,
    File *root,
    File *symlink,
    NFTWFlags flags,
    Set *result,
    Set *processed
)
{
    bool uptodate = true;

    FileIdObj *symlink_fileid_obj = create_FileIdObj(symlink->fileid);

    if(contains_Set(processed, symlink_fileid_obj))
    {
        return true;
    }

    add_Set(processed, symlink_fileid_obj);

    if(flags.phys)
    {
        add_Set(result, getPath_File(file_system, symlink));
    }
    else
    {
        if(symlink->descriptor == NULL)
        {
            uptodate = false;
        }
        else
        {
            File *file = getFile_FileSystem(file_system, symlink->descriptor);

            if(file->kind == UnknownFileKind)
            {
                uptodate = false;
            }
            else if(file->kind == DirectoryFile)
            {
                uptodate = processDirectory_getFileTree_NFTW_Path
                    (file_system, root, file, flags, result, processed);
            }
            else if(file->kind == SymbolicLinkFile)
            {
                uptodate = processSymLink_getFileTree_NFTW_Path
                    (file_system, root, file, flags, result, processed);
            }
            else
            {
                if(flags.mount)
                {
                    if(equals(root->dev, file->dev))
                    {
                        add_Set(result, getPath_File(file_system, file));
                    }
                }
            }

            if(!uptodate)
            {
                return false;
            }
        }
    }

    return uptodate;
}

static bool processDirectory_getFileTree_NFTW_Path
(
    FileSystem *file_system,
    File *root,
    File *directory,
    NFTWFlags flags,
    Set *result,
    Set *processed
)
{
    int i, count;

    bool uptodate = true;

    FileIdObj *directory_fileid_obj = create_FileIdObj(directory->fileid);

    if(contains_Set(processed, directory_fileid_obj))
    {
        return true;
    }

    add_Set(processed, directory_fileid_obj);

    if(flags.mount)
    {
        if(!equals(root->dev, directory->dev))
        {
            return true;
        }
    }

    if(!isUptodate_Directory(directory))
    {
        return false;
    }

    traceFormattedUserInfo("processDirectory_getFileTree_NFTW_Path: directory=$(obj)",
        getPath_File(file_system, directory));

    add_Set(result, getPath_File(file_system, directory));

    count = getFileCount_Directory(directory);

    traceFormattedUserInfo("processDirectory_getFileTree_NFTW_Path: count=%d", count);

    for(i = 0; i < count; i++)
    {
        File *file = getFileAt_Directory(file_system, directory, i);

        traceFormattedUserInfo("processDirectory_getFileTree_NFTW_Path: file=$(obj)",
            getPath_File(file_system, file));

        if(file->kind == UnknownFileKind)
        {
            uptodate = false;
        }
        else if(file->kind == DirectoryFile)
        {
            File *parent = getTheOnlyParentDirectory_File(file_system, directory);

            if(equals_FileId(file->fileid, directory->fileid))
            {
                /* Filter '.' */
                continue;
            }

            if(equals_FileId(file->fileid, parent->fileid))
            {
                /* Filter '..' */
                continue;
            }

            uptodate = processDirectory_getFileTree_NFTW_Path
                (file_system, root, file, flags, result, processed);
        }
        else if(file->kind == SymbolicLinkFile)
        {
            uptodate = processSymLink_getFileTree_NFTW_Path
                (file_system, root, file, flags, result, processed);
        }
        else
        {
            add_Set(result, getPath_File(file_system, file));
        }

        if(!uptodate)
        {
            return false;
        }
    }

    return uptodate;
}

Set* getFileTree_NFTW_Path(CallContext context, CString *path, NFTWFlags flags, bool *uptodate)
{
    Set *result = create_Set(&type_CString);
    Set *processed = create_Set(&type_FileIdObj);
    FileSystem *file_system = getFileSystem(context);
    File *file = getFile_FileSystem(file_system, path);

    bool file_tree_is_uptodate = true;

    if(file == NULL)
    {
        traceUserInfo("getFileTree_NFTW_Path: file is NULL");

        result = NULL;
    }
    else if(file->kind == UnknownFileKind)
    {
        traceUserInfo("getFileTree_NFTW_Path: file is unknown");

        file_tree_is_uptodate = false;
    }
    else if(file->kind == DirectoryFile)
    {
        traceUserInfo("getFileTree_NFTW_Path: file is directory");

        file_tree_is_uptodate = processDirectory_getFileTree_NFTW_Path
            (file_system, file, file, flags, result, processed);
    }
    else if(file->kind == SymbolicLinkFile)
    {
        traceUserInfo("getFileTree_NFTW_Path: file is symbolic link");

        file_tree_is_uptodate = processSymLink_getFileTree_NFTW_Path
            (file_system, file, file, flags, result, processed);
    }
    else
    {
        traceUserInfo("getFileTree_NFTW_Path: file has differ kind");

        result = NULL;
    }

    if(uptodate != NULL)
    {
        *uptodate = file_tree_is_uptodate;
    }

    return result;
}

Set* getFileTree_FTW_Path(CallContext context, CString *path, bool *uptodate)
{
    NFTWFlags flags = default_NFTWFlags();

    flags.phys = true;

    return getFileTree_NFTW_Path(context, path, flags, uptodate);
}

int getBase_Path(CString *path)
{
    int i, j;
    CharT *str;

    assertion(path != NULL, "getBase_Path: path is NULL");

    traceFormattedUserInfo("getBase_Path: path=$(obj)", path);

    str = toCharArray_CString(path);
    for(i = j = 0; str[i]; i++)
    {
        if(str[i] == '/')
        {
            while(str[++i] == '/');

            if(str[i])
            {
                j = i;
            }
        }
    }

    return j;
}

int getLevel_Path(CString *root, CString *path)
{
    List *root_list, *path_list;

    assertion(root != NULL, "getLevel_Path: root is NULL");
    assertion(path != NULL, "getLevel_Path: path is NULL");

    root_list = split_Path(root);
    path_list = split_Path(path);

    return size_List(path_list) - size_List(root_list);
}