# 
# This file is part of PKM (Persistent Knowledge Monitor).
# Copyright (c) 2020 Capgemini Group, Commissariat à l'énergie atomique et aux énergies alternatives,
#                    OW2, Sysgo AG, Technikon, Tree Technology, Universitat Politècnica de València.
# 
# 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. 

openapi: 3.0.0
info:
  title: FramaCRestfulApiForPkm
  description: API of Frama-C for PKM
  version: 1.0.0
  contact:
    name: DECODER project
    url: https://www.decoder-project.eu
    email: decoder@decoder-project.eu
  license:
    name: Apache 2.0
    url: http://www.apache.org/licenses/LICENSE-2.0.html
servers:
  - url: http://pkm-api_frama-c_1:8081
paths:
  /frama_c/{dbName}:
    post:
      tags:
        - FramaC
      operationId: frama_c
      description: Runs Frama-C static program analyzer
      parameters:
        - name: dbName
          description: The project name from where to get source code/header files, the compile commands, and put the parsing results (Source code ASTs, Comments, and Annotations) and/or the analysis results
          in: path
          required: true
          schema:
            type: string
        - name: asynchronous
          description: flag to control asynchronous/synchronous execution of Frama-C job
          in: query
          schema:
            type: boolean
            default: false
        - $ref: '#/components/parameters/InvocationIdParam'
        - $ref: '#/components/parameters/keyParam'
      requestBody:
        required: true
        content:
          application/json:
            schema:
              type : object
              properties:
                source_file_paths:
                  description: Source Code filenames to process
                  type: array
                  items:
                    type: string
                mode:
                  description: The operating modes
                  type: object
                  properties:
                    parser:
                      description: Enable/disable parser (implicitely enabled when neither EVA nor WP are enabled)
                      type: boolean
                    eva:
                      description: Enable/disable EVA (Evolved Value Analysis) plug-in
                      type: boolean
                    wp:
                      description: Enable/disable WP (Weakest Precondition calculus) plug-in
                      type: boolean
                options:
                  description: options
                  type: object
                  properties:
                    args:
                      description: Frama-C command line options
                      type: array
                      items:
                        type: string
                    eva:
                      description: EVA options
                      type: object
                      properties:
                        main:
                          description: main function for EVA
                          type: string
                    wp:
                      description: WP options
                      type: object
                      properties:
                        wp_fct:
                          description: functions for WP
                          type: array
                          items:
                            description: function name
                            type: string
                    includes_system_files:
                      description: Enable/Disable inclusion of system files (i.e. system headers) in the result
                      type: boolean
              required:
                - source_file_paths
      x-codegen-request-body-name: body
      responses:
        201:
          description: Created, returns a job
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Job'
        400:
          description: Bad request
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
        401:
          description: Unauthorized operation, returns an error message
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
        403:
          description: Forbidden operation, returns an error message
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
        404:
          description: Not found, returns an error message
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
        500:
          description: Internal Server Error, returns an error message
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
  /frama_c/jobs/{jobId}:
    get:
      tags:
        - FramaC
      operationId: getJob
      description: Get Frama-C Job. Getting a finished or failed job, unpublish it (it is no longer available)
      parameters:
        - name: jobId
          description: Job identifier
          in: path
          required: true
          schema:
            type: integer
            minimum: 0
        - $ref: '#/components/parameters/keyParam'
      responses:
        200:
          description: Successful operation, returns a job
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Job'
        400:
          description: Bad request
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
        401:
          description: Unauthorized operation, returns an error message
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
        403:
          description: Forbidden operation, returns an error message
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
        404:
          description: Not found, returns an error message
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
        500:
          description: Internal Server Error, returns an error message
          headers:
            Access-Control-Allow-Origin:
              $ref: '#/components/headers/Access-Control-Allow-Origin'
            Access-Control-Allow-Methods:
              $ref: '#/components/headers/Access-Control-Allow-Methods'
            Access-Control-Allow-Headers:
              $ref: '#/components/headers/Access-Control-Allow-Headers'
          content:
            application/json:
              schema:
                type: string
                description: error message
components:
  parameters:
    keyParam:
      name: key
      description: Access key to the PKM
      in: header
      required: true
      schema:
        type: string
    InvocationIdParam:
      name: invocationID
      description: invocation identifier (optional)
      in: query
      schema:
        type: string
  schemas:
    Job:
      type: object
      description: a job
      properties:
        id:
          description: job identifier
          type: integer
          minimum: 0
        service_name:
          description: name of the service running the job
          type: string
        parameters:
          description: parameters of the job
          type: object
          properties:
            dbName:
              description: database name
              type: string
        state:
          description: job state
          enum: [pending, running, failed, finished]
        start_date:
          description: date (GMT) when job started
          type: string
        end_date:
          description: date (GMT) when job ended
          type: string
        logs:
          description: log messages
          type: string
        warnings:
          type: string
          description: warning messages
        err:
          description: error
          type: object
  headers:
# for CORS (Cross-Origin Resource Sharing)
    Access-Control-Allow-Origin:
      schema:
        type: string
        default: '*'
    Access-Control-Allow-Methods:
      schema:
        type: string
        default: 'GET, POST, PUT, DELETE, OPTIONS'
    Access-Control-Allow-Headers:
      schema:
        type: string
        default: 'Origin, Content-Type, Accept, key'