/**
 * @file tpl_invoque.% !EXTENSION %
 *
 * @section descr File description
 *
 * System call user level invoque API.
 *
 * @warning this file is generated by gen_invoque.sh based on the 
 * tpl_os_service_ids.h header file.
 *
 * @section copyright Copyright
 *
 * Trampoline OS
 *
 * Trampoline is copyright (c) IRCCyN 2005+
 * Copyright ESEO for function and data structures documentation and ARM port
 * Trampoline is protected by the French intellectual property law.
 *
 * This software is distributed under the Lesser GNU Public Licence
 *
 * @section infos File informations
 *
 * $$Date$$
 * $$Rev$$
 * $$Author$$
 * $$URL$$
 */
#include "tpl_os_application_def.h"
#include "tpl_service_ids.h"

#if WITH_SYSTEM_CALL == NO
#error "This file should not be part of your project since WITH_SYSTEM_CALL is not defined"
#endif

%
if exists ASSEMBLERHEADER default (false) then %
#include "tpl_assembler.h"
%
end if
%
#if WITH_MEMMAP == NO
%
template if exists std_as_code_dir
%
#endif /* WITH_MEMMAP == NO */

#define API_START_SEC_CODE
#include "tpl_as_memmap.h"

%
template if exists instruction_specific
template if exists invoque_specific

foreach api_sec in APIUSED do
  foreach api_func in api_sec::SYSCALL do
    template service_call
  end foreach
end foreach
%

#define API_STOP_SEC_CODE
#include "tpl_as_memmap.h"


/* End of file tpl_invoque.% !EXTENSION % */