From c7e9d4ae51532329b85c36c419f36dd50de9e521 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Thu, 22 Aug 2024 10:12:14 +0200
Subject: [PATCH] [wp] remove wp-region from ivette-api config

# Conflicts:
#	ivette/yarn.lock
---
 .../frama-c/kernel/api/parameters/index.ts    | 288 ------------------
 1 file changed, 288 deletions(-)

diff --git a/ivette/src/frama-c/kernel/api/parameters/index.ts b/ivette/src/frama-c/kernel/api/parameters/index.ts
index f42b08cf6cd..8fca8d4066e 100644
--- a/ivette/src/frama-c/kernel/api/parameters/index.ts
+++ b/ivette/src/frama-c/kernel/api/parameters/index.ts
@@ -8284,294 +8284,6 @@ const wpModel_internal: State.State<string> = {
 /** State of parameter -wp-model */
 export const wpModel: State.State<string> = wpModel_internal;
 
-/** Signal for state [`regionAnnot`](#regionannot)  */
-export const signalRegionAnnot: Server.Signal = {
-  name: 'kernel.parameters.signalRegionAnnot',
-};
-
-const getRegionAnnot_internal: Server.GetRequest<null,boolean> = {
-  kind: Server.RqKind.GET,
-  name: 'kernel.parameters.getRegionAnnot',
-  input: Json.jNull,
-  output: Json.jBoolean,
-  fallback: false,
-  signals: [],
-};
-/** Getter for state [`regionAnnot`](#regionannot)  */
-export const getRegionAnnot: Server.GetRequest<null,boolean>= getRegionAnnot_internal;
-
-const setRegionAnnot_internal: Server.SetRequest<boolean,null> = {
-  kind: Server.RqKind.SET,
-  name: 'kernel.parameters.setRegionAnnot',
-  input: Json.jBoolean,
-  output: Json.jNull,
-  fallback: null,
-  signals: [],
-};
-/** Setter for state [`regionAnnot`](#regionannot)  */
-export const setRegionAnnot: Server.SetRequest<boolean,null>= setRegionAnnot_internal;
-
-const regionAnnot_internal: State.State<boolean> = {
-  name: 'kernel.parameters.regionAnnot',
-  signal: signalRegionAnnot,
-  getter: getRegionAnnot,
-  setter: setRegionAnnot,
-};
-/** State of parameter -region-annot */
-export const regionAnnot: State.State<boolean> = regionAnnot_internal;
-
-/** Signal for state [`wpRegionFlat`](#wpregionflat)  */
-export const signalWpRegionFlat: Server.Signal = {
-  name: 'kernel.parameters.signalWpRegionFlat',
-};
-
-const getWpRegionFlat_internal: Server.GetRequest<null,boolean> = {
-  kind: Server.RqKind.GET,
-  name: 'kernel.parameters.getWpRegionFlat',
-  input: Json.jNull,
-  output: Json.jBoolean,
-  fallback: false,
-  signals: [],
-};
-/** Getter for state [`wpRegionFlat`](#wpregionflat)  */
-export const getWpRegionFlat: Server.GetRequest<null,boolean>= getWpRegionFlat_internal;
-
-const setWpRegionFlat_internal: Server.SetRequest<boolean,null> = {
-  kind: Server.RqKind.SET,
-  name: 'kernel.parameters.setWpRegionFlat',
-  input: Json.jBoolean,
-  output: Json.jNull,
-  fallback: null,
-  signals: [],
-};
-/** Setter for state [`wpRegionFlat`](#wpregionflat)  */
-export const setWpRegionFlat: Server.SetRequest<boolean,null>= setWpRegionFlat_internal;
-
-const wpRegionFlat_internal: State.State<boolean> = {
-  name: 'kernel.parameters.wpRegionFlat',
-  signal: signalWpRegionFlat,
-  getter: getWpRegionFlat,
-  setter: setWpRegionFlat,
-};
-/** State of parameter -wp-region-flat */
-export const wpRegionFlat: State.State<boolean> = wpRegionFlat_internal;
-
-/** Signal for state [`wpRegionPack`](#wpregionpack)  */
-export const signalWpRegionPack: Server.Signal = {
-  name: 'kernel.parameters.signalWpRegionPack',
-};
-
-const getWpRegionPack_internal: Server.GetRequest<null,boolean> = {
-  kind: Server.RqKind.GET,
-  name: 'kernel.parameters.getWpRegionPack',
-  input: Json.jNull,
-  output: Json.jBoolean,
-  fallback: false,
-  signals: [],
-};
-/** Getter for state [`wpRegionPack`](#wpregionpack)  */
-export const getWpRegionPack: Server.GetRequest<null,boolean>= getWpRegionPack_internal;
-
-const setWpRegionPack_internal: Server.SetRequest<boolean,null> = {
-  kind: Server.RqKind.SET,
-  name: 'kernel.parameters.setWpRegionPack',
-  input: Json.jBoolean,
-  output: Json.jNull,
-  fallback: null,
-  signals: [],
-};
-/** Setter for state [`wpRegionPack`](#wpregionpack)  */
-export const setWpRegionPack: Server.SetRequest<boolean,null>= setWpRegionPack_internal;
-
-const wpRegionPack_internal: State.State<boolean> = {
-  name: 'kernel.parameters.wpRegionPack',
-  signal: signalWpRegionPack,
-  getter: getWpRegionPack,
-  setter: setWpRegionPack,
-};
-/** State of parameter -wp-region-pack */
-export const wpRegionPack: State.State<boolean> = wpRegionPack_internal;
-
-/** Signal for state [`wpRegionRw`](#wpregionrw)  */
-export const signalWpRegionRw: Server.Signal = {
-  name: 'kernel.parameters.signalWpRegionRw',
-};
-
-const getWpRegionRw_internal: Server.GetRequest<null,boolean> = {
-  kind: Server.RqKind.GET,
-  name: 'kernel.parameters.getWpRegionRw',
-  input: Json.jNull,
-  output: Json.jBoolean,
-  fallback: false,
-  signals: [],
-};
-/** Getter for state [`wpRegionRw`](#wpregionrw)  */
-export const getWpRegionRw: Server.GetRequest<null,boolean>= getWpRegionRw_internal;
-
-const setWpRegionRw_internal: Server.SetRequest<boolean,null> = {
-  kind: Server.RqKind.SET,
-  name: 'kernel.parameters.setWpRegionRw',
-  input: Json.jBoolean,
-  output: Json.jNull,
-  fallback: null,
-  signals: [],
-};
-/** Setter for state [`wpRegionRw`](#wpregionrw)  */
-export const setWpRegionRw: Server.SetRequest<boolean,null>= setWpRegionRw_internal;
-
-const wpRegionRw_internal: State.State<boolean> = {
-  name: 'kernel.parameters.wpRegionRw',
-  signal: signalWpRegionRw,
-  getter: getWpRegionRw,
-  setter: setWpRegionRw,
-};
-/** State of parameter -wp-region-rw */
-export const wpRegionRw: State.State<boolean> = wpRegionRw_internal;
-
-/** Signal for state [`wpRegionInline`](#wpregioninline)  */
-export const signalWpRegionInline: Server.Signal = {
-  name: 'kernel.parameters.signalWpRegionInline',
-};
-
-const getWpRegionInline_internal: Server.GetRequest<null,boolean> = {
-  kind: Server.RqKind.GET,
-  name: 'kernel.parameters.getWpRegionInline',
-  input: Json.jNull,
-  output: Json.jBoolean,
-  fallback: false,
-  signals: [],
-};
-/** Getter for state [`wpRegionInline`](#wpregioninline)  */
-export const getWpRegionInline: Server.GetRequest<null,boolean>= getWpRegionInline_internal;
-
-const setWpRegionInline_internal: Server.SetRequest<boolean,null> = {
-  kind: Server.RqKind.SET,
-  name: 'kernel.parameters.setWpRegionInline',
-  input: Json.jBoolean,
-  output: Json.jNull,
-  fallback: null,
-  signals: [],
-};
-/** Setter for state [`wpRegionInline`](#wpregioninline)  */
-export const setWpRegionInline: Server.SetRequest<boolean,null>= setWpRegionInline_internal;
-
-const wpRegionInline_internal: State.State<boolean> = {
-  name: 'kernel.parameters.wpRegionInline',
-  signal: signalWpRegionInline,
-  getter: getWpRegionInline,
-  setter: setWpRegionInline,
-};
-/** State of parameter -wp-region-inline */
-export const wpRegionInline: State.State<boolean> = wpRegionInline_internal;
-
-/** Signal for state [`wpRegionCluster`](#wpregioncluster)  */
-export const signalWpRegionCluster: Server.Signal = {
-  name: 'kernel.parameters.signalWpRegionCluster',
-};
-
-const getWpRegionCluster_internal: Server.GetRequest<null,boolean> = {
-  kind: Server.RqKind.GET,
-  name: 'kernel.parameters.getWpRegionCluster',
-  input: Json.jNull,
-  output: Json.jBoolean,
-  fallback: false,
-  signals: [],
-};
-/** Getter for state [`wpRegionCluster`](#wpregioncluster)  */
-export const getWpRegionCluster: Server.GetRequest<null,boolean>= getWpRegionCluster_internal;
-
-const setWpRegionCluster_internal: Server.SetRequest<boolean,null> = {
-  kind: Server.RqKind.SET,
-  name: 'kernel.parameters.setWpRegionCluster',
-  input: Json.jBoolean,
-  output: Json.jNull,
-  fallback: null,
-  signals: [],
-};
-/** Setter for state [`wpRegionCluster`](#wpregioncluster)  */
-export const setWpRegionCluster: Server.SetRequest<boolean,null>= setWpRegionCluster_internal;
-
-const wpRegionCluster_internal: State.State<boolean> = {
-  name: 'kernel.parameters.wpRegionCluster',
-  signal: signalWpRegionCluster,
-  getter: getWpRegionCluster,
-  setter: setWpRegionCluster,
-};
-/** State of parameter -wp-region-cluster */
-export const wpRegionCluster: State.State<boolean> = wpRegionCluster_internal;
-
-/** Signal for state [`wpRegionFixpoint`](#wpregionfixpoint)  */
-export const signalWpRegionFixpoint: Server.Signal = {
-  name: 'kernel.parameters.signalWpRegionFixpoint',
-};
-
-const getWpRegionFixpoint_internal: Server.GetRequest<null,boolean> = {
-  kind: Server.RqKind.GET,
-  name: 'kernel.parameters.getWpRegionFixpoint',
-  input: Json.jNull,
-  output: Json.jBoolean,
-  fallback: false,
-  signals: [],
-};
-/** Getter for state [`wpRegionFixpoint`](#wpregionfixpoint)  */
-export const getWpRegionFixpoint: Server.GetRequest<null,boolean>= getWpRegionFixpoint_internal;
-
-const setWpRegionFixpoint_internal: Server.SetRequest<boolean,null> = {
-  kind: Server.RqKind.SET,
-  name: 'kernel.parameters.setWpRegionFixpoint',
-  input: Json.jBoolean,
-  output: Json.jNull,
-  fallback: null,
-  signals: [],
-};
-/** Setter for state [`wpRegionFixpoint`](#wpregionfixpoint)  */
-export const setWpRegionFixpoint: Server.SetRequest<boolean,null>= setWpRegionFixpoint_internal;
-
-const wpRegionFixpoint_internal: State.State<boolean> = {
-  name: 'kernel.parameters.wpRegionFixpoint',
-  signal: signalWpRegionFixpoint,
-  getter: getWpRegionFixpoint,
-  setter: setWpRegionFixpoint,
-};
-/** State of parameter -wp-region-fixpoint */
-export const wpRegionFixpoint: State.State<boolean> = wpRegionFixpoint_internal;
-
-/** Signal for state [`wpRegion`](#wpregion)  */
-export const signalWpRegion: Server.Signal = {
-  name: 'kernel.parameters.signalWpRegion',
-};
-
-const getWpRegion_internal: Server.GetRequest<null,boolean> = {
-  kind: Server.RqKind.GET,
-  name: 'kernel.parameters.getWpRegion',
-  input: Json.jNull,
-  output: Json.jBoolean,
-  fallback: false,
-  signals: [],
-};
-/** Getter for state [`wpRegion`](#wpregion)  */
-export const getWpRegion: Server.GetRequest<null,boolean>= getWpRegion_internal;
-
-const setWpRegion_internal: Server.SetRequest<boolean,null> = {
-  kind: Server.RqKind.SET,
-  name: 'kernel.parameters.setWpRegion',
-  input: Json.jBoolean,
-  output: Json.jNull,
-  fallback: null,
-  signals: [],
-};
-/** Setter for state [`wpRegion`](#wpregion)  */
-export const setWpRegion: Server.SetRequest<boolean,null>= setWpRegion_internal;
-
-const wpRegion_internal: State.State<boolean> = {
-  name: 'kernel.parameters.wpRegion',
-  signal: signalWpRegion,
-  getter: getWpRegion,
-  setter: setWpRegion,
-};
-/** State of parameter -wp-region */
-export const wpRegion: State.State<boolean> = wpRegion_internal;
-
 /** Signal for state [`wpWhy3ExtraConfig`](#wpwhy3extraconfig)  */
 export const signalWpWhy3ExtraConfig: Server.Signal = {
   name: 'kernel.parameters.signalWpWhy3ExtraConfig',
-- 
GitLab