frama-c-openapi.yaml

openapi: 3.0.0
info:
  title: FramaCRestfulApiForPkm
  description: API of Frama-C for PKM
  version: 1.0.0
  contact:
    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:
      operationId: frama_c
      parameters:
        - name: dbName
          description: Database name from where to get source code/header files and put 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/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: mode
                  type: object
                  properties:
                    parser:
                      description: enable/disable parser (implicitely enabled when neither EVA nor WP are enabled)
                      type: boolean
                    eva:
                      description: enable/disable EVA
                      type: boolean
                    wp:
                      description: enable/disable WP
                      type: boolean
                options:
                  description: options
                  type: object
                  properties:
                    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
              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:
      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 (optional, depending on server configuration)
      in: header
      required: true
      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'