From a5ed0906b838f5273cefebc694e32f46079ca9d4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 11 Oct 2022 10:26:24 +0200
Subject: [PATCH] [aorai] remove unused files following suppression of
ltl/promela lexers and parsers
---
src/plugins/aorai/ltl_output.ml | 81 --------------------------------
src/plugins/aorai/ltl_output.mli | 35 --------------
src/plugins/aorai/ltlast.ml | 59 -----------------------
3 files changed, 175 deletions(-)
delete mode 100644 src/plugins/aorai/ltl_output.ml
delete mode 100644 src/plugins/aorai/ltl_output.mli
delete mode 100644 src/plugins/aorai/ltlast.ml
diff --git a/src/plugins/aorai/ltl_output.ml b/src/plugins/aorai/ltl_output.ml
deleted file mode 100644
index 2b4f569cfd5..00000000000
--- a/src/plugins/aorai/ltl_output.ml
+++ /dev/null
@@ -1,81 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Aorai plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* INSA (Institut National des Sciences Appliquees) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Format
-open Ltlast
-
-let out_fmt=ref (formatter_of_out_channel stdout)
-
-let rec ltl_form_to_string = function
- | LNext (f) ->
- "X("^(ltl_form_to_string f)^")"
- | LUntil (f1,f2) ->
- "("^(ltl_form_to_string f1)^" U "^(ltl_form_to_string f2)^")"
- | LFatally (f) ->
- "<>("^(ltl_form_to_string f)^")"
- | LGlobally (f) ->
- "[]("^(ltl_form_to_string f)^")"
- | LRelease (f1,f2) ->
- "("^(ltl_form_to_string f1)^" V "^(ltl_form_to_string f2)^")"
-
- | LNot (f) ->
- "!("^(ltl_form_to_string f)^")"
- | LAnd (f1,f2) ->
- "("^(ltl_form_to_string f1)^" && "^(ltl_form_to_string f2)^")"
- | LOr (f1,f2) ->
- "("^(ltl_form_to_string f1)^" || "^(ltl_form_to_string f2)^")"
- | LImplies (f1,f2) ->
- "("^(ltl_form_to_string f1)^" -> "^(ltl_form_to_string f2)^")"
- | LIff (f1,f2) ->
- "("^(ltl_form_to_string f1)^" <-> "^(ltl_form_to_string f2)^")"
-
- | LTrue ->
- "1"
- | LFalse ->
- "0"
-
- | LCall (s) ->
- "callof_"^s
- | LReturn (s) ->
- "returnof_"^s
- | LCallOrReturn (s) ->
- "callorreturnof_"^s
-
- | LIdent (s) ->
- s
-
-let output ltl_form file =
- let c = open_out file in
- out_fmt:=formatter_of_out_channel c ;
- fprintf !out_fmt "%s\n\n" (ltl_form_to_string ltl_form);
- fprintf !out_fmt "@?"; (* Flush du flux *)
- close_out c;
- out_fmt:=formatter_of_out_channel stdout
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/aorai/ltl_output.mli b/src/plugins/aorai/ltl_output.mli
deleted file mode 100644
index 76fa0289f80..00000000000
--- a/src/plugins/aorai/ltl_output.mli
+++ /dev/null
@@ -1,35 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Aorai plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* INSA (Institut National des Sciences Appliquees) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* $Id: ltl_output.mli,v 1.2 2008-10-02 13:33:29 uid588 Exp $ *)
-
-val output : Ltlast.formula -> string -> unit
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/aorai/ltlast.ml b/src/plugins/aorai/ltlast.ml
deleted file mode 100644
index 21f24eac7a0..00000000000
--- a/src/plugins/aorai/ltlast.ml
+++ /dev/null
@@ -1,59 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Aorai plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* INRIA (Institut National de Recherche en Informatique et en *)
-(* Automatique) *)
-(* INSA (Institut National des Sciences Appliquees) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* $Id: ltlast.mli,v 1.3 2008-10-13 09:21:24 uid588 Exp $ *)
-
-(** The abstract tree of LTL formula. Such tree is used by ltl parser/lexer before its translation into Buchi automata by the LTL2BA external tool. *)
-
-
-(** LTL formula parsed abstract syntax trees *)
-type formula =
- | LNext of formula (** 'Next' temporal operator *)
- | LUntil of formula * formula (** 'Until' temporal operator *)
- | LFatally of formula (** 'Fatally' temporal operator *)
- | LGlobally of formula (** 'Globally' temporal operator *)
- | LRelease of formula * formula (** 'Release' temporal operator (reminder: f1 R f2 <=> !(!f1 U !f2)) *)
-
- | LNot of formula (** 'not' logic operator *)
- | LAnd of formula * formula (** 'and' logic operator *)
- | LOr of formula * formula (** 'or' logic operator *)
- | LImplies of formula * formula (** '=>' logic operator *)
- | LIff of formula * formula (** '<=>' logic operator *)
-
- | LTrue (** 'true' logic constant *)
- | LFalse (** 'false' logic constant *)
-
- | LCall of string (** Logic predicate. The String has to be the name of an operation from C program *)
- | LReturn of string (** Logic predicate. The String has to be the name of an operation from C program *)
- | LCallOrReturn of string (** Logic predicate. The String has to be the name of an operation from C program *)
-
- | LIdent of string (** Logic expression. The String is the name of a fresh variable defined by the expression and used to be in conformance with the input syntax of LTL2BA tool. *)
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
--
GitLab