Skip to content
Snippets Groups Projects
Commit edfab802 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[kernel] drop ppx_import dependency

parent 86904c03
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
dev/docker/Dockerfile
+ 0
− 1
View file @ edfab802
......@@ -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
+ 0
− 2
View file @ edfab802
......@@ -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
+ 0
− 2
View file @ edfab802
......@@ -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
+ 0
− 1
View file @ edfab802
......@@ -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
+ 0
− 1
View file @ edfab802
......@@ -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.6.0
- yojson.2.0.2
......
src/dune
+ 1
− 2
View file @ edfab802
......@@ -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
+ 112
− 93
View file @ edfab802
......@@ -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
+ 8
− 8
View file @ edfab802
......@@ -439,35 +439,35 @@ let is_matching_logic_type_var a a' env =
| Some a'' -> Datatype.String.equal a' a''
module Unop = struct
type t = [%import: Cil_types.unop] [@@deriving eq]
type t = Cil_types.unop [@@deriving eq]
end
module Binop = struct
type t = [%import: Cil_types.binop] [@@deriving eq]
type t = Cil_types.binop [@@deriving eq]
end
module Ikind = struct
type t = [%import: Cil_types.ikind] [@@deriving eq]
type t = Cil_types.ikind [@@deriving eq]
end
module Fkind = struct
type t = [%import: Cil_types.fkind] [@@deriving eq]
type t = Cil_types.fkind [@@deriving eq]
end
module Predicate_kind = struct
type t = [%import: Cil_types.predicate_kind] [@@deriving eq]
type t = Cil_types.predicate_kind [@@deriving eq]
end
module Logic_builtin_label = struct
type t = [%import: Cil_types.logic_builtin_label] [@@deriving eq]
type t = Cil_types.logic_builtin_label [@@deriving eq]
end
module Relation = struct
type t = [%import: Cil_types.relation] [@@deriving eq]
type t = Cil_types.relation [@@deriving eq]
end
module Termination_kind = struct
type t = [%import: Cil_types.termination_kind] [@@deriving eq]
type t = Cil_types.termination_kind [@@deriving eq]
end
let is_same_behavior_set l l' =
......
src/plugins/eva/dune
+ 1
− 1
View file @ edfab802
......@@ -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)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment