Merge branch 'fix/blanchard/kernel/remove-ppx-import' into 'master'

[kernel] drop ppx_import dependency

See merge request frama-c/frama-c!4553

dev/docker/Dockerfile

@@ -281,7 +281,6 @@ RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/alt-ergo
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/lablgtk3
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/lablgtk3-sourceview3
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_deriving
-RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_import
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppx_tools
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/ppxlib
 RUN rm -rf /home/opam/.opam/${OCAML_VERSION}/lib/psmt2-frontend

nix/frama-c.nix

@@ -39,7 +39,6 @@
 , ppx_deriving
 , ppx_deriving_yaml
 , ppx_deriving_yojson
-, ppx_import
 , unionFind
 , yojson
 , which
@@ -101,7 +100,6 @@ stdenvNoCC.mkDerivation rec {
     ppx_deriving
     ppx_deriving_yaml
     ppx_deriving_yojson
-    ppx_import
     unionFind
     yojson
     which

nix/internal-tests.nix

@@ -33,7 +33,6 @@
 , ppx_deriving
 , ppx_deriving_yaml
 , ppx_deriving_yojson
-, ppx_import
 , unionFind
 , yojson
 , which
@@ -96,7 +95,6 @@ stdenvNoCC.mkDerivation rec {
     ppx_deriving
     ppx_deriving_yaml
     ppx_deriving_yojson
-    ppx_import
     unionFind
     yojson
     which

opam

@@ -145,7 +145,6 @@ depends: [
   "ppx_deriving"
   "ppx_deriving_yojson"
   "ppx_deriving_yaml" { >= "0.2.0" }
-  "ppx_import"
 
   # GTK3 disabled on macOS (segfaults), and made optional on Windows
   # (due to complex situation with Cygwin + MinGW).

reference-configuration.md

@@ -13,7 +13,6 @@ compiling Frama-C 28.1.
 - ocamlgraph.2.1.0
 - ppx_deriving_yaml.0.2.1
 - ppx_deriving_yojson.3.7.0
-- ppx_import.1.10.0
 - unionFind.20220122
 - why3.1.7.1
 - yojson.2.0.2

src/dune

@@ -37,7 +37,6 @@
           (echo "  - menhirLib:" %{lib-available:menhirLib} "\n")
           (echo "  - dune-site:" %{lib-available:dune-site} "\n")
           (echo "  - dune-site.plugins:" %{lib-available:dune-site.plugins} "\n")
-          (echo "  - ppx_import:" %{lib-available:ppx_import} "\n")
           (echo "  - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n")
           (echo "  - ppx_deriving.ord:" %{lib-available:ppx_deriving.ord} "\n")
           (echo "  - ppx_deriving_yaml:" %{lib-available:ppx_deriving_yaml} "\n")
@@ -53,7 +52,7 @@
   (libraries frama-c.init fpath str unix zarith ocamlgraph dynlink bytes yaml.unix yojson menhirLib dune-site dune-site.plugins)
   (instrumentation (backend landmarks))
   (instrumentation (backend bisect_ppx))
-  (preprocess (staged_pps ppx_import ppx_deriving.eq ppx_deriving.ord ppx_deriving_yaml))
+  (preprocess (pps ppx_deriving.eq ppx_deriving.ord ppx_deriving_yaml))
 )
 
 (generate_sites_module (module config_data) (sites frama-c) (plugins (frama-c plugins) (frama-c plugins_gui)))

src/kernel_services/ast_data/cil_types.ml

@@ -54,6 +54,118 @@
 (* check_file class in frama-c/src/file.ml (before launching the tests)     *)
 (****************************************************************************)
 
+(* ************************************************************************* *)
+(** {2 Simple types} *)
+(* ************************************************************************* *)
+
+(* ************************************************************************* *)
+(** {3 Operators} *)
+(* ************************************************************************* *)
+
+(** Unary operators *)
+type unop =
+  | Neg   (** Unary minus *)
+  | BNot  (** Bitwise complement (~) *)
+  | LNot  (** Logical Not (!) *)
+[@@deriving eq]
+
+(** Binary operations *)
+type binop =
+    PlusA    (** arithmetic + *)
+  | PlusPI   (** pointer + integer *)
+  | MinusA   (** arithmetic - *)
+  | MinusPI  (** pointer - integer *)
+  | MinusPP  (** pointer - pointer *)
+  | Mult     (** * *)
+  | Div      (** /
+                 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+  | Mod      (** %
+                 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+  | Shiftlt  (** shift left *)
+  | Shiftrt  (** shift right *)
+
+  | Lt       (** <  (arithmetic comparison) *)
+  | Gt       (** >  (arithmetic comparison) *)
+  | Le       (** <= (arithmetic comparison) *)
+  | Ge       (** >= (arithmetic comparison) *)
+  | Eq       (** == (arithmetic comparison) *)
+  | Ne       (** != (arithmetic comparison) *)
+  | BAnd     (** bitwise and *)
+  | BXor     (** exclusive-or *)
+  | BOr      (** inclusive-or *)
+
+  | LAnd     (** logical and. Unlike other expressions this one does not always
+                 evaluate both operands. If you want
+                 to use these, you must set
+                 {!Cil.useLogicalOperators}. *)
+  | LOr      (** logical or. Unlike other expressions this one does not always
+                 evaluate both operands.  If you
+                 want to use these, you must set
+                 {!Cil.useLogicalOperators}. *)
+[@@deriving eq]
+
+(* ************************************************************************* *)
+(** {3 Types} *)
+(* ************************************************************************* *)
+
+(** Various kinds of integers *)
+type ikind =
+  | IBool       (** [_Bool] *)
+  | IChar       (** [char] *)
+  | ISChar      (** [signed char] *)
+  | IUChar      (** [unsigned char] *)
+  | IInt        (** [int] *)
+  | IUInt       (** [unsigned int] *)
+  | IShort      (** [short] *)
+  | IUShort     (** [unsigned short] *)
+  | ILong       (** [long] *)
+  | IULong      (** [unsigned long] *)
+  | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
+  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on MSVC) *)
+[@@deriving eq]
+
+(** Various kinds of floating-point numbers*)
+type fkind =
+  | FFloat      (** [float] *)
+  | FDouble     (** [double] *)
+  | FLongDouble (** [long double] *)
+[@@deriving eq]
+
+(* ************************************************************************* *)
+(** {3 Logic} *)
+(* ************************************************************************* *)
+
+type predicate_kind = Assert | Check | Admit
+[@@deriving eq]
+
+(** builtin logic labels defined in ACSL. *)
+type logic_builtin_label =
+  | Here
+  | Old
+  | Pre
+  | Post
+  | LoopEntry
+  | LoopCurrent
+  | Init
+[@@deriving eq]
+
+(** comparison relations*)
+type relation =
+  | Rlt
+  | Rgt
+  | Rle
+  | Rge
+  | Req
+  | Rneq
+  (** Different
+      @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
+  *)
+[@@deriving eq]
+
+(** kind of termination a post-condition applies to. See ACSL manual. *)
+type termination_kind = Normal | Exits | Breaks | Continues | Returns
+[@@deriving eq]
+
 (* ************************************************************************* *)
 (** {2 Root of the AST} *)
 (* ************************************************************************* *)
@@ -243,28 +355,6 @@ and typ =
   | TBuiltin_va_list of attributes
   (** This is the same as the gcc's type with the same name *)
 
-(** Various kinds of integers *)
-and ikind =
-    IBool       (** [_Bool] *)
-  | IChar       (** [char] *)
-  | ISChar      (** [signed char] *)
-  | IUChar      (** [unsigned char] *)
-  | IInt        (** [int] *)
-  | IUInt       (** [unsigned int] *)
-  | IShort      (** [short] *)
-  | IUShort     (** [unsigned short] *)
-  | ILong       (** [long] *)
-  | IULong      (** [unsigned long] *)
-  | ILongLong   (** [long long] (or [_int64] on Microsoft Visual C) *)
-  | IULongLong  (** [unsigned long long] (or [unsigned _int64] on Microsoft
-                    Visual C) *)
-
-(** Various kinds of floating-point numbers*)
-and fkind =
-    FFloat      (** [float] *)
-  | FDouble     (** [double] *)
-  | FLongDouble (** [long double] *)
-
 (* ************************************************************************* *)
 (** {2 Attributes} *)
 (* ************************************************************************* *)
@@ -742,46 +832,6 @@ and constant =
   (** An enumeration constant. Use [Cillower.lowerEnumVisitor] to replace these
       with integer constants. *)
 
-(** Unary operators *)
-and unop =
-    Neg   (** Unary minus *)
-  | BNot  (** Bitwise complement (~) *)
-  | LNot  (** Logical Not (!) *)
-
-(** Binary operations *)
-and binop =
-    PlusA    (** arithmetic + *)
-  | PlusPI   (** pointer + integer *)
-  | MinusA   (** arithmetic - *)
-  | MinusPI  (** pointer - integer *)
-  | MinusPP  (** pointer - pointer *)
-  | Mult     (** * *)
-  | Div      (** /
-                 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-  | Mod      (** %
-                 @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-  | Shiftlt  (** shift left *)
-  | Shiftrt  (** shift right *)
-
-  | Lt       (** <  (arithmetic comparison) *)
-  | Gt       (** >  (arithmetic comparison) *)
-  | Le       (** <= (arithmetic comparison) *)
-  | Ge       (** >= (arithmetic comparison) *)
-  | Eq       (** == (arithmetic comparison) *)
-  | Ne       (** != (arithmetic comparison) *)
-  | BAnd     (** bitwise and *)
-  | BXor     (** exclusive-or *)
-  | BOr      (** inclusive-or *)
-
-  | LAnd     (** logical and. Unlike other expressions this one does not always
-                 evaluate both operands. If you want
-                 to use these, you must set
-                 {!Cil.useLogicalOperators}. *)
-  | LOr      (** logical or. Unlike other expressions this one does not always
-                 evaluate both operands.  If you
-                 want to use these, you must set
-                 {!Cil.useLogicalOperators}. *)
-
 (* ************************************************************************* *)
 (** {2 Left values} *)
 (* ************************************************************************* *)
@@ -1321,16 +1371,6 @@ and logic_label =
   | FormalLabel of string (** label of global annotation. *)
   | BuiltinLabel of logic_builtin_label
 
-(** builtin logic labels defined in ACSL. *)
-and logic_builtin_label =
-  | Here
-  | Old
-  | Pre
-  | Post
-  | LoopEntry
-  | LoopCurrent
-  | Init
-
 (* ************************************************************************* *)
 (** {2 Terms} *)
 (* ************************************************************************* *)
@@ -1523,19 +1563,6 @@ and logic_ctor_info =
 (** variables bound by a quantifier. *)
 and quantifiers = logic_var list
 
-(** comparison relations*)
-and relation =
-  | Rlt
-  | Rgt
-  | Rle
-  | Rge
-  | Req
-  | Rneq
-  (** Different
-      @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
-  *)
-
-
 (** predicates *)
 and predicate_node =
   | Pfalse (** always-false predicate. *)
@@ -1578,11 +1605,6 @@ and identified_predicate = {
   ip_content: toplevel_predicate; (** the predicate itself*)
 }
 
-and predicate_kind =
-  | Assert
-  | Check
-  | Admit
-
 (** main statement of an annotation. *)
 and toplevel_predicate = {
   tp_kind: predicate_kind;
@@ -1713,9 +1735,6 @@ and behavior = {
   (** extensions *)
 }
 
-(** kind of termination a post-condition applies to. See ACSL manual. *)
-and termination_kind = Normal | Exits | Breaks | Continues | Returns
-
 (** Pragmas for the value analysis plugin of Frama-C. *)
 and loop_pragma =
   | Unroll_specs of term list

src/kernel_services/ast_queries/ast_diff.ml

@@ -438,38 +438,6 @@ let is_matching_logic_type_var a a' env =
   | None -> false
   | Some a'' -> Datatype.String.equal a' a''
 
-module Unop = struct
-  type t = [%import: Cil_types.unop] [@@deriving eq]
-end
-
-module Binop = struct
-  type t = [%import: Cil_types.binop] [@@deriving eq]
-end
-
-module Ikind = struct
-  type t = [%import: Cil_types.ikind] [@@deriving eq]
-end
-
-module Fkind = struct
-  type t = [%import: Cil_types.fkind] [@@deriving eq]
-end
-
-module Predicate_kind = struct
-  type t = [%import: Cil_types.predicate_kind] [@@deriving eq]
-end
-
-module Logic_builtin_label = struct
-  type t = [%import: Cil_types.logic_builtin_label] [@@deriving eq]
-end
-
-module Relation = struct
-  type t = [%import: Cil_types.relation] [@@deriving eq]
-end
-
-module Termination_kind = struct
-  type t = [%import: Cil_types.termination_kind] [@@deriving eq]
-end
-
 let is_same_behavior_set l l' =
   Datatype.String.Set.(equal (of_list l) (of_list l'))
 
@@ -494,7 +462,7 @@ let is_same_logic_label l l' _env =
        Cil_datatype.Stmt.equal !s' s''
      | exception Not_found -> false)
   | FormalLabel s, FormalLabel s' -> Datatype.String.equal s s'
-  | BuiltinLabel l, BuiltinLabel l' -> Logic_builtin_label.equal l l'
+  | BuiltinLabel l, BuiltinLabel l' -> equal_logic_builtin_label l l'
   | (StmtLabel _ | FormalLabel _ | BuiltinLabel _), _ -> false
 
 let rec is_same_predicate p p' env =
@@ -511,7 +479,7 @@ and is_same_predicate_node p p' env =
     is_same_list is_same_term args args' env
   | Pseparated t, Pseparated t' -> is_same_list is_same_term t t' env
   | Prel (r,t1,t2), Prel(r',t1',t2') ->
-    Relation.equal r r' && is_same_term t1 t1' env && is_same_term t2 t2' env
+    equal_relation r r' && is_same_term t1 t1' env && is_same_term t2 t2' env
   | Pand(p1,p2), Pand(p1',p2')
   | Por(p1,p2), Por(p1',p2')
   | Pxor(p1,p2), Pxor(p1',p2')
@@ -579,9 +547,9 @@ and is_same_term_node t t' env =
   | TSizeOfE t, TSizeOfE t'
   | TAlignOfE t, TAlignOfE t' -> is_same_term t t' env
   | TSizeOfStr s, TSizeOfStr s' -> String.length s = String.length s'
-  | TUnOp(op,t), TUnOp(op',t') -> Unop.equal op op' && is_same_term t t' env
+  | TUnOp(op,t), TUnOp(op',t') -> equal_unop op op' && is_same_term t t' env
   | TBinOp(op,t1,t2), TBinOp(op',t1',t2') ->
-    Binop.equal op op' && is_same_term t1 t1' env && is_same_term t2 t2' env
+    equal_binop op op' && is_same_term t1 t1' env && is_same_term t2 t2' env
   | TCast(is_logic, typ, term), TCast(is_logic', typ', term') ->
     is_logic = is_logic' && is_same_logic_type typ typ' env && is_same_term term term' env
   | TAddrOf lv, TAddrOf lv'
@@ -685,7 +653,7 @@ and is_same_term_offset lo lo' env =
   | (TNoOffset | TField _ | TModel _ | TIndex _), _ -> false
 
 and is_same_toplevel_predicate p p' env =
-  Predicate_kind.equal p.tp_kind p'.tp_kind &&
+  equal_predicate_kind p.tp_kind p'.tp_kind &&
   is_same_predicate p.tp_statement p'.tp_statement env
 
 and is_same_identified_predicate p p' env =
@@ -695,7 +663,7 @@ and is_same_identified_term t t' env =
   is_same_term t.it_content t'.it_content env
 
 and is_same_post_cond (k,p) (k',p') env =
-  Termination_kind.equal k k' && is_same_identified_predicate p p' env
+  equal_termination_kind k k' && is_same_identified_predicate p p' env
 
 and is_same_deps d d' env =
   match d,d' with
@@ -877,9 +845,9 @@ and is_same_type t t' env =
   match t, t' with
   | TVoid a, TVoid a' -> Cil_datatype.Attributes.equal a a'
   | TInt (ik,a), TInt(ik',a') ->
-    Ikind.equal ik ik' && Cil_datatype.Attributes.equal a a'
+    equal_ikind ik ik' && Cil_datatype.Attributes.equal a a'
   | TFloat (fk,a), TFloat(fk', a') ->
-    Fkind.equal fk fk' && Cil_datatype.Attributes.equal a a'
+    equal_fkind fk fk' && Cil_datatype.Attributes.equal a a'
   | TBuiltin_va_list a, TBuiltin_va_list a' ->
     Cil_datatype.Attributes.equal a a'
   | TPtr(t,a), TPtr(t',a') ->
@@ -922,7 +890,7 @@ and is_same_compinfo ci ci' env =
 and is_same_enuminfo ei ei' env =
   let res, _ =
     (Cil_datatype.Attributes.equal ei.eattr ei'.eattr &&
-     Ikind.equal ei.ekind ei'.ekind, env) &&&
+     equal_ikind ei.ekind ei'.ekind, env) &&&
     is_same_list_env is_same_enumitem ei.eitems ei'.eitems
   in
   res
@@ -994,9 +962,9 @@ and is_same_exp e e' env =
   | AlignOf t, AlignOf t' -> is_same_type t t' env
   | AlignOfE e, AlignOfE e' -> is_same_exp e e' env
   | UnOp(op,e,t), UnOp(op',e',t') ->
-    Unop.equal op op' && is_same_exp e e' env && is_same_type t t' env
+    equal_unop op op' && is_same_exp e e' env && is_same_type t t' env
   | BinOp(op,e1,e2,t), BinOp(op',e1',e2',t') ->
-    Binop.equal op op' && is_same_exp e1 e1' env && is_same_exp e2 e2' env
+    equal_binop op op' && is_same_exp e1 e1' env && is_same_exp e2 e2' env
     && is_same_type t t' env
   | CastE(t,e), CastE(t',e') -> is_same_type t t' env && is_same_exp e e' env
   | AddrOf lv, AddrOf lv' -> is_same_lval lv lv' env

src/plugins/eva/dune

@@ -45,7 +45,7 @@
  (libraries frama-c.kernel frama-c-server.core frama-c-postdominators.core)
  (instrumentation (backend landmarks))
  (instrumentation (backend bisect_ppx))
- (preprocess (staged_pps ppx_deriving.eq ppx_deriving.ord)))
+ (preprocess (pps ppx_deriving.eq ppx_deriving.ord)))
 
 (plugin
  (name eva)