From a3d630ba0c455414bab33b22490412a90ad2c11e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 9 May 2022 17:43:32 +0200
Subject: [PATCH] [tests] remove journal tests
---
.../plugin_entry_points/journal.ml | 499 ------------------
.../plugin_entry_points/journal.mli | 120 -----
src/plugins/callgraph/journalize.ml | 45 --
src/plugins/callgraph/journalize.mli | 44 --
tests/journal/abstract_cpt.ml | 33 --
tests/journal/control.i | 29 -
tests/journal/control2.c | 19 -
tests/journal/intra.i | 119 -----
tests/journal/intra.ml | 4 -
tests/journal/oracle/control.0.res.oracle | 38 --
tests/journal/oracle/control.1.res.oracle | 71 ---
tests/journal/oracle/control.2.res.oracle | 6 -
tests/journal/oracle/control2.res.oracle | 73 ---
tests/journal/oracle/control2_sav.err | 0
tests/journal/oracle/control2_sav.res | 77 ---
tests/journal/oracle/intra.res.oracle | 116 ----
tests/journal/test_config | 2 -
tests/journal/use_cpt.ml | 20 -
18 files changed, 1315 deletions(-)
delete mode 100644 src/kernel_services/plugin_entry_points/journal.ml
delete mode 100644 src/kernel_services/plugin_entry_points/journal.mli
delete mode 100644 src/plugins/callgraph/journalize.ml
delete mode 100644 src/plugins/callgraph/journalize.mli
delete mode 100644 tests/journal/abstract_cpt.ml
delete mode 100644 tests/journal/control.i
delete mode 100644 tests/journal/control2.c
delete mode 100644 tests/journal/intra.i
delete mode 100644 tests/journal/intra.ml
delete mode 100644 tests/journal/oracle/control.0.res.oracle
delete mode 100644 tests/journal/oracle/control.1.res.oracle
delete mode 100644 tests/journal/oracle/control.2.res.oracle
delete mode 100644 tests/journal/oracle/control2.res.oracle
delete mode 100644 tests/journal/oracle/control2_sav.err
delete mode 100644 tests/journal/oracle/control2_sav.res
delete mode 100644 tests/journal/oracle/intra.res.oracle
delete mode 100644 tests/journal/test_config
delete mode 100644 tests/journal/use_cpt.ml
diff --git a/src/kernel_services/plugin_entry_points/journal.ml b/src/kernel_services/plugin_entry_points/journal.ml
deleted file mode 100644
index 4c81ac38b9c..00000000000
--- a/src/kernel_services/plugin_entry_points/journal.ml
+++ /dev/null
@@ -1,499 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(* ****************************************************************************)
-(* ****************************************************************************)
-(* ****************************************************************************)
-
-(* Disclaimer
- ----------
- This module uses very unsafe caml features (module Obj).
- Modify it at your own risk.
- Sometimes the caml type system does not help you here.
- Introducing a bug here may introduce some "segmentation faults" in Frama-C *)
-
-(* ****************************************************************************)
-(* ****************************************************************************)
-(* ****************************************************************************)
-
-open Cmdline.Kernel_log
-
-(** Journalization of functions *)
-
-(* ****************************************************************************)
-(** {2 Journal management} *)
-(* ****************************************************************************)
-
-(* [started] prevents journalization of function call
- inside another one. It is [true] iff a journalized function is being
- applied. *)
-let started = ref false
-
-module Sentences = struct
-
- type t =
- { sentence: Format.formatter -> unit;
- raise_exn: bool }
-
- let sentences : t Queue.t = Queue.create ()
-
- let add print exn =
- Queue.add { sentence = print; raise_exn = exn } sentences
-
- let write fmt =
- let finally_raised = ref false in
- (* printing the sentences *)
- Queue.iter
- (fun s -> s.sentence fmt; finally_raised := s.raise_exn)
- sentences;
- (* if any, re-raised the exception raised by the last sentence *)
- Format.fprintf fmt "@[%s@]"
- (if !finally_raised then "raise (Exception (Printexc.to_string exn))"
- else "()");
- (* closing the box opened when catching exception *)
- Queue.iter
- (fun s -> if s.raise_exn then Format.fprintf fmt "@]@]@]@;end")
- sentences
-
- let journal_copy = ref (Queue.create ())
- let save () = journal_copy := Queue.copy sentences
- let restore () =
- Queue.clear sentences;
- Queue.transfer !journal_copy sentences
-
-end
-
-module Abstract_modules = struct
- let tbl: (string, string) Hashtbl.t = Hashtbl.create 7
- let () = Type.add_abstract_types := Hashtbl.replace tbl
- let write fmt =
- Hashtbl.iter
- (fun k v ->
- Format.fprintf fmt
- "@[<hv 2>let module %s=@;@[<hv 0>Type.Abstract\
- (struct let name = %S end) in@]@]@;"
- k v)
- tbl
- let tbl_copy = ref (Hashtbl.create 7)
- let save () = tbl_copy := Hashtbl.copy tbl
- let restore () =
- Hashtbl.clear tbl;
- Hashtbl.iter (fun k v -> Hashtbl.add tbl k v) !tbl_copy
-end
-
-let save () =
- Sentences.save ();
- Abstract_modules.save ()
-
-let restore () =
- Sentences.restore ();
- Abstract_modules.restore ()
-
-let now () = Unix.localtime (Unix.time ())
-
-let default_filename = "frama_c_journal.ml"
-let filename = ref default_filename
-let get_session_file = ref (fun _ -> assert false)
-let get_name () =
- let f = !filename in
- if f == default_filename
- then !get_session_file f
- else Datatype.Filepath.of_string f
-
-let set_name s = filename := s
-
-let print_header fmt =
- let time = now () in
- Format.pp_open_hvbox fmt 0; (* the outermost box *)
- Format.fprintf fmt
- "@[(* Frama-C journal generated at %02d:%02d the %02d/%02d/%d *)@]@;@;"
- time.Unix.tm_hour
- time.Unix.tm_min
- time.Unix.tm_mday
- (time.Unix.tm_mon+1)
- (time.Unix.tm_year + 1900);
- Format.fprintf fmt "@[exception Unreachable@]@;";
- Format.fprintf fmt "@[exception Exception of string@]@;@;";
- Format.fprintf fmt "@[[@@@@@@ warning \"-26\"]@]@;@;";
- Format.fprintf fmt (* open two boxes for start *)
- "(* Run the user commands *)@;@[<hv 2>let run () =@;@[<hv 0>"
-
-let print_trailer fmt =
- let name = Format.asprintf "%a" Datatype.Filepath.pretty (get_name ()) in
- Format.fprintf fmt "@[(* Main *)@]@\n";
- Format.fprintf fmt "@[<hv 2>let main () =@;";
- Format.fprintf fmt
- "@[<hv 0>@[<hv 2>Journal.keep_file@; (Datatype.Filepath.of_string@; (\"%s\"));@]@;"
- name;
- Format.fprintf fmt "try run ()@;";
- Format.fprintf fmt "@[<v>with@;@[<hv 2>| Unreachable ->@ ";
- Format.fprintf fmt
- "@[<hv 2>Kernel.fatal@;\"Journal reaches an assumed dead code\"@;@]@]@;";
- Format.fprintf fmt "@[<hv 2>| Exception s ->@ ";
- Format.fprintf fmt
- "@[<hv 2>Kernel.log@;\"Journal re-raised the exception %%S\"@;s@]@]@;";
- Format.fprintf fmt "@[<hv 2>| exn ->@ ";
- Format.fprintf fmt
- "@[<hv 2>Kernel.fatal@;\"Journal raised an unexpected exception: %%s\"@;";
- Format.fprintf fmt "(Printexc.to_string exn)@]@]@]@]@]@\n@\n";
- Format.fprintf fmt "@[(* Registering *)@]@\n";
- Format.fprintf fmt
- "@[<hv 2>let main : unit -> unit =@;@[<hv 2>Dynamic.register@;~plugin:%S@;\"main\"@;"
- (String.capitalize_ascii (Filename.basename name));
- Format.fprintf fmt
- "@[<hv 2>(Datatype.func@;Datatype.unit@;Datatype.unit)@]@;";
- Format.fprintf fmt "~journalize:false@;main@]@]@\n@\n";
- Format.fprintf fmt "@[(* Hooking *)@]@\n";
- Format.fprintf fmt "@[<hv 2>let () =@;";
- Format.fprintf fmt
- "@[<hv 2>Cmdline.run_after_loading_stage@;main;@]@;";
- Format.fprintf fmt "@[<hv 2>Cmdline.is_going_to_load@;()@]@]@.";
- (* close the outermost box *)
- Format.pp_close_box fmt ()
-
-let preserved_files : Datatype.Filepath.t list ref = ref []
-let keep_file s = preserved_files := s :: !preserved_files
-
-let get_filename =
- let cpt = ref 0 in
- let rec get_filename first =
- let name_fp = get_name () in
- let name = (name_fp:>string) in
- if (not first && Sys.file_exists name) || List.mem name_fp !preserved_files
- then begin
- incr cpt;
- let suf = "_" ^ string_of_int !cpt in
- (try
- let n =
- Str.search_backward
- (Str.regexp "_[0-9]+")
- name
- (String.length name - 1)
- in
- filename := Str.string_before name n ^ suf
- with Not_found ->
- filename := name ^ suf);
- get_filename false
- end else
- name_fp
- in
- fun () -> get_filename true
-
-let write () =
- let write fmt =
- print_header fmt;
- Abstract_modules.write fmt;
- Sentences.write fmt;
- Format.fprintf fmt "@]@]@;@;";
- print_trailer fmt;
- Format.pp_print_flush fmt ()
- in
- let error msg s = error "cannot %s journal (%s)." msg s in
- let filename = get_filename () in
- feedback "writing journal in file `%a'."
- Datatype.Filepath.pretty filename;
- try
- let cout = open_out (filename:>string) in
- let fmt = Format.formatter_of_out_channel cout in
- Format.pp_set_margin fmt 78 (* line length *);
- (try write fmt with Sys_error s -> error "write into" s);
- try close_out cout with Sys_error s -> error "close" s
- with Sys_error s ->
- error "create" s
-
-let () =
- (* write the journal iff it is enable and
- - either an error occurs;
- - or the user explicitly wanted it. *)
- if Cmdline.journal_enable then begin
- Cmdline.at_error_exit (fun _ -> write ());
- if Cmdline.journal_isset then Cmdline.at_normal_exit write
- end
-
-(* ****************************************************************************)
-(** {2 Journalization} *)
-(* ****************************************************************************)
-
-module Binding: sig
- val add: 'a Type.t -> 'a -> string -> unit
- (** [add ty v var] binds the value [v] to the variable name [var]. Thus,
- [pp ty v] prints [var] and not use the standard pretty printer. Very
- useful to pretty print values with no associated pretty printer. *)
-
- exception Name_already_exists of string
- val add_once: 'a Type.t -> 'a -> string -> unit
- (** Same as function [add] above but raise the exception [Already_exists]
- if the binding previously exists *)
-
- val find: 'a Type.t -> 'a -> string
- val iter: ('a Type.t -> 'a -> string -> unit) -> unit
-end = struct
-
- let bindings : string Type.Obj_tbl.t = Type.Obj_tbl.create ()
-
- let add ty v var =
- Type.Obj_tbl.add bindings ty v var (* eta-expansion required *)
-
- (* add bindings for [Format.std_formatter] and [Format.err_formatter] *)
- let () =
- add Datatype.formatter Format.std_formatter "Format.std_formatter";
- add Datatype.formatter Format.err_formatter "Format.err_formatter"
-
- exception Name_already_exists of string
- let check_name s =
- let error () =
- Format.eprintf "[Type] A value of name %s already exists@." s;
- raise (Name_already_exists s)
- in
- Type.Obj_tbl.iter bindings (fun _ _ s' -> if s = s' then error ())
-
- let add_once ty x s =
- check_name s;
- add ty x s
-
- let find ty v = Type.Obj_tbl.find bindings ty v (* eta-expansion required *)
- let iter f = Type.Obj_tbl.iter bindings f (* eta-expansion required *)
-
- (* predefined bindings *)
- let () =
- add Datatype.formatter Format.std_formatter "Format.std_formatter";
- add Datatype.formatter Format.err_formatter "Format.err_formatter"
-
-end
-
-(* JS 2012/02/07: useful only for BM introspection testing ;-) *)
-module Reverse_binding = struct
- module Tbl = Type.String_tbl(struct type 'a t = 'a end)
- exception Unbound_value = Tbl.Unbound_value
- exception Incompatible_type = Tbl.Incompatible_type
-
- let tbl = Tbl.create 97
- let fill () = Binding.iter (fun ty v name -> Tbl.add tbl name ty v)
- let find name ty = Tbl.find tbl name ty
- let iter f = Tbl.iter f tbl
-
- let pretty fmt () =
- iter
- (fun name ty v ->
- Format.fprintf fmt "%s --> %a@." name (Datatype.pretty ty) v)
-
-end
-
-exception Not_writable of string
-let never_write name f =
- if Cmdline.journal_enable && Cmdline.use_type then
- if Obj.tag (Obj.repr f) = Obj.closure_tag then
- Obj.magic
- (fun y ->
- if !started then Obj.magic f y
- else
- let msg =
- Format.asprintf
- "a call to the function %s has to be written in the journal, \
- but this function was never journalized."
- name
- in
- raise (Not_writable msg))
- else
- invalid_arg ("[Journal.never_write] " ^ name ^ " is not a closure")
- else
- f
-
-let pp (type t) (ty: t Type.t) fmt (x:t) =
- assert Cmdline.use_type;
- try Format.fprintf fmt "%s" (Binding.find ty x);
- with Not_found ->
- let pp_error msg =
- Format.fprintf fmt "@[<hov 2>(failwith @[<hov 2>\"%s:@ running the journal will fail.\"@])@;@]" msg
- in
- let pp = Datatype.internal_pretty_code ty in
- if pp == Datatype.undefined then
- pp_error
- (Format.asprintf
- "no printer registered for value of type %s"
- (Type.name ty))
- else if pp == Datatype.pp_fail then
- pp_error
- (Format.asprintf
- "no code for pretty printer of type %s"
- (Type.name ty))
- else
- pp Type.Call fmt x
-
-let gen_binding =
- let ids = Hashtbl.create 7 in
- let rec gen s =
- try
- let n = succ (Hashtbl.find ids s) in
- Hashtbl.replace ids s n;
- gen (s ^ "_" ^ string_of_int n)
- with Not_found ->
- Hashtbl.add ids s 1;
- s
- in
- gen
-
-let extend_continuation f_acc pp_arg opt_label opt_arg arg fmt =
- f_acc fmt;
- match opt_label, opt_arg with
- | None, None (* no label *) -> Format.fprintf fmt "@;%a" pp_arg arg;
- | None, Some _ -> assert false
- | Some _, Some f when f () == arg ->
- (* [arg] is the default value of the optional label *)
- ()
- | Some l, _ (* other label *) -> Format.fprintf fmt "@;~%s:%a" l pp_arg arg
-
-(* print any comment *)
-let print_comment fmt pp = match pp with
- | None -> ()
- | Some pp -> Format.fprintf fmt "(* %t *)@;" pp
-
-let print_sentence f_acc is_dyn comment ?value ty fmt =
- assert Cmdline.use_type;
- print_comment fmt comment;
- (* open a new box for the sentence *)
- Format.fprintf fmt "@[<hv 2>";
- (* add a let binding whenever the return type is not unit *)
- let is_unit = Type.equal ty Datatype.unit in
- if not is_unit then
- Format.fprintf fmt "let %t=@;"
- (fun fmt ->
- let binding =
- let varname = Datatype.varname ty in
- match varname == Datatype.undefined, value with
- | true, _ | _, None ->
- "__" (* no binding nor value: ignore the result *)
- | false, Some value ->
- (* bind to a fresh variable name *)
- let b = gen_binding (varname value) in
- Binding.add ty value b;
- b
- in
- Format.fprintf fmt "%s" binding;
- (* add the return type for dynamic application *)
- if is_dyn then Format.fprintf fmt "@;: %s " (Type.name ty)
- else Format.fprintf fmt " ");
- (* pretty print the sentence itself in a box *)
- Format.fprintf fmt "@[<hv 2>%t@]" f_acc;
- (* close the sentence *)
- if is_unit then Format.fprintf fmt ";@]@;"
- else Format.fprintf fmt "@;<1 -2>in@]@;"
-
-let add_sentence f_acc is_dyn comment ?value ty =
- Sentences.add (print_sentence f_acc is_dyn comment ?value ty) false
-
-let catch_exn f_acc is_dyn comment ret_ty exn =
- let s_exn = Printexc.to_string exn in
- (* [s_exn] is not necessarily a valid OCaml exception.
- So don't use it in OCaml code. *)
- let comment fmt =
- Format.fprintf fmt "@[<hv 2>exception %s@;raised on: @]%t" s_exn
- (fun fmt -> Option.iter (fun f -> f fmt) comment)
- in
- let print fmt =
- (* open a new box for the sentence *)
- Format.fprintf fmt
- "@[<hv 2>begin try@;@[<hv>%t@[<hv 2>raise Unreachable@]@]@]@;"
- (print_sentence f_acc is_dyn (Some comment) ret_ty);
- (* two opened boxes closed at end *)
- Format.fprintf fmt
- "@[<v>with@;@[<hv 2>| Unreachable as exn -> raise exn@]@;";
- Format.fprintf fmt
- "@[<hv 2>| exn (* %s *) ->@;@[<hv>@[(* continuing: *)@]@;" s_exn
- in
- Sentences.add print true
-
-let rec journalize_function: 't.
- (Format.formatter -> unit) -> 't Type.t -> bool ->
- (Format.formatter -> unit) option -> 't -> 't =
- fun (type t) (type a) (type b) f_acc (ty: t Type.t) is_dyn comment (x:t)
- ->
- assert Cmdline.use_type;
- if Type.Function.is_instance_of ty then begin
- (* [ty] is a function type value:
- there exists [a] and [b] such than [t = a -> b] *)
- let ty: (a -> b) Type.t = Obj.magic (ty: t Type.t) in
- let f: a -> b = Obj.magic (x: t) in
- let (a: a Type.t), (b: b Type.t), opt_label =
- Type.Function.get_instance ty
- in
- let opt_arg = Type.Function.get_optional_argument ty in
- let f (y: a) : b =
- if !started then
- (* prevent journalisation if you're journalizing another function *)
- f y
- else begin
- try
- (* [started] prevents journalization of function call
- inside another one *)
- started := true;
- (* apply the closure [x] to its argument [y] *)
- let xy = f y in
- started := false;
- (* extend the continuation and continue *)
- let f_acc = extend_continuation f_acc (pp a) opt_label opt_arg y in
- journalize_function f_acc b is_dyn comment xy
- with
- | Not_writable name ->
- started := false;
- fatal
- "a call to the function %S cannot be written in the journal"
- name
- | exn as e ->
- let f_acc = extend_continuation f_acc (pp a) opt_label opt_arg y in
- catch_exn f_acc is_dyn comment b exn;
- started := false;
- raise e
- end in
- (* cast back the closure of type [a -> b] into [t] *)
- (Obj.magic (f: a -> b): t)
- end else begin
- if not !started then add_sentence f_acc is_dyn comment ~value:x ty;
- x
- end
-
-let register s ty ?comment ?(is_dyn=false) x =
- if Cmdline.journal_enable then begin
- assert Cmdline.use_type;
- if s = "" then
- abort "[Journal.register] the given name should not be \"\"";
- Binding.add_once ty x s;
- if Type.Function.is_instance_of ty then begin
- let f_acc fmt = pp ty fmt x in
- journalize_function f_acc ty is_dyn comment x
- end else
- x
- end else
- x
-
-let prevent f x =
- let old = !started in
- started := true;
- let res = try f x with exn -> started := old; raise exn in
- started := old;
- res
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/plugin_entry_points/journal.mli b/src/kernel_services/plugin_entry_points/journal.mli
deleted file mode 100644
index f9be3ee7a31..00000000000
--- a/src/kernel_services/plugin_entry_points/journal.mli
+++ /dev/null
@@ -1,120 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Journalization of functions.
- @plugin development guide *)
-
-(* ****************************************************************************)
-(** {2 Journalization} *)
-(* ****************************************************************************)
-
-val register:
- string ->
- 'a Type.t ->
- ?comment:(Format.formatter -> unit) ->
- ?is_dyn:bool ->
- 'a ->
- 'a
-(** [register name ty ~comment ~is_dyn v] journalizes the value [v]
- of type [ty] with the name [name]. [name] must exactly match the caml
- long name of the value (i.e. "List.iter" and not "iter" even though the
- module List is already opened). Journalisation of anonymous value is
- not possible.
-
- If the [comment] argument is set, the given pretty printer will be
- applied in an OCaml comment when the function is journalized.
-
- Set [is_dyn] to [true] to journalize a dynamic function. *)
-
-val never_write: string -> 'a -> 'a
-(** [never_write name f] returns a closure [g] observationally equal to [f]
- except that trying to write a call to [g] in the journal is an error. If
- [f] is not a closure, then [never_write name f] raises
- [Invalid_argument]. *)
-
-val prevent: ('a -> 'b) -> 'a -> 'b
-(** [prevent f x] applies [x] to [f] without printing anything in the
- journal, even if [f] is journalized. *)
-
-module Binding: sig
- val add: 'a Type.t -> 'a -> string -> unit
- (** [add ty v var] binds the value [v] to the variable name [var]. Thus,
- [pp ty v] prints [var] and not use the standard pretty printer. Very
- useful to pretty print values with no associated pretty printer. *)
-
- exception Name_already_exists of string
- val add_once: 'a Type.t -> 'a -> string -> unit
- (** Same as function [add] above but raise the exception [Already_exists]
- if the binding previously exists *)
-end
-
-(* JS 2012/02/07: useful only for BM introspection testing ;-) *)
-module Reverse_binding: sig
-
- (* Raised by [find] *)
- exception Unbound_value of string
- exception Incompatible_type of string
-
- val fill: unit -> unit
- val find: string -> 'a Type.t -> 'a
- val iter: (string -> 'a Type.t -> 'a -> unit) -> unit
- val pretty: Format.formatter -> unit -> unit
-end
-
-(* ****************************************************************************)
-(** {2 Journal management} *)
-(* ****************************************************************************)
-
-val get_name: unit -> Datatype.Filepath.t
-(** @return the filename which the journal will be written into. *)
-
-val set_name: string -> unit
-(** [set_name name] changes the filename into the journal is generated. *)
-
-val write: unit -> unit
-(** [write ()] writes the content of the journal into the file set by
- [set_name] (or in "frama_c_journal.ml" by default);
- without clearing the journal. *)
-
-val save: unit -> unit
-(** Save the current state of the journal for future restoration.
- @since Beryllium-20090901 *)
-
-val restore: unit -> unit
-(** Restore a previously saved journal.
- @since Beryllium-20090901 *)
-
-(* ****************************************************************************)
-(** {2 Internal use only} *)
-(* ****************************************************************************)
-
-val keep_file: Datatype.Filepath.t -> unit
-(** This function is not to be used explicitly. Only offers functions
- retrieving when running a journal file. *)
-
-val get_session_file: (string -> Datatype.Filepath.t) ref
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/callgraph/journalize.ml b/src/plugins/callgraph/journalize.ml
deleted file mode 100644
index 88a8231294d..00000000000
--- a/src/plugins/callgraph/journalize.ml
+++ /dev/null
@@ -1,45 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-module Make
- (C: sig
- val name: string
- val dump: unit -> unit
- val compute: unit -> unit
- type t
- val ty: t Type.t
- val get: unit -> t
- end) =
-struct
- let name = "Callgraph." ^ C.name
- let unit_unit = Datatype.func Datatype.unit Datatype.unit
- let dump = Journal.register (name ^ ".dump") unit_unit C.dump
- let compute = Journal.register (name ^ ".compute") unit_unit C.compute
- let get =
- Journal.register (name ^ ".get") (Datatype.func Datatype.unit C.ty) C.get
-end
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)
diff --git a/src/plugins/callgraph/journalize.mli b/src/plugins/callgraph/journalize.mli
deleted file mode 100644
index c1c89a0ff8f..00000000000
--- a/src/plugins/callgraph/journalize.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Journalize the API of a callgraph *)
-
-module Make
- (C: sig
- val name: string
- val dump: unit -> unit
- val compute: unit -> unit
- type t
- val ty: t Type.t
- val get: unit -> t
- end):
-sig
- val dump: unit -> unit
- val compute: unit -> unit
- val get: unit -> C.t
-end
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)
diff --git a/tests/journal/abstract_cpt.ml b/tests/journal/abstract_cpt.ml
deleted file mode 100644
index 5fa827630f9..00000000000
--- a/tests/journal/abstract_cpt.ml
+++ /dev/null
@@ -1,33 +0,0 @@
-let mk () = ref 0
-let incr c = incr c; !c
-
-include Datatype.Make(struct
- (* order of lines below does matter *)
- include Datatype.Serializable_undefined
- include Datatype.Ref(Datatype.Int)
- let varname _ = "cpt"
- let name = "Abstract_cpt.t"
-end)
-
-let mk =
- Dynamic.register
- ~journalize:true
- ~plugin:"Abstract_cpt"
- "mk"
- (Datatype.func Datatype.unit ty) mk
-
-let incr =
- Dynamic.register
- ~journalize:true
- ~plugin:"Abstract_cpt"
- "incr"
- (Datatype.func ty Datatype.int)
- incr
-
-let pretty =
- Dynamic.register
- ~journalize:true
- ~plugin:"Abstract_cpt"
- "pretty"
- (Datatype.func ty Datatype.unit)
- (fun n -> Format.printf "%d@." !n)
diff --git a/tests/journal/control.i b/tests/journal/control.i
deleted file mode 100644
index ec7902161dd..00000000000
--- a/tests/journal/control.i
+++ /dev/null
@@ -1,29 +0,0 @@
-/* run.config
- COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
- CMD: @frama-c@ @PTEST_OPTIONS@
- COMMENT: do not compare generated journals since they depend on current time
- PLUGIN: @EVA_PLUGINS@
- EXECNOW: BIN control_journal.ml @frama-c@ @PTEST_FILE@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name @PTEST_RESULT@/control_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
- SCRIPT: @PTEST_RESULT@/control_journal.ml
- OPT:
- MODULE:
- SCRIPT: @PTEST_RESULT@/control_journal_bis.ml
- EXECNOW: BIN control_journal_bis.ml cp %{dep:@PTEST_RESULT@/control_journal.ml} @PTEST_RESULT@/control_journal_bis.ml > @DEV_NULL@ 2> @DEV_NULL@
- OPT: -calldeps
- MODULE: abstract_cpt use_cpt
- SCRIPT:
- EXECNOW: BIN abstract_cpt_journal.ml @frama-c@ -journal-enable -journal-name @PTEST_RESULT@/abstract_cpt_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
- SCRIPT: @PTEST_RESULT@/abstract_cpt_journal.ml
- OPT:
-*/
-
-int x,y,c,d;
-
-void f() {
- int i;
- for(i=0; i<4 ; i++) {
- if (c) { if (d) {y++;} else {x++;}}
- else {};
- x=x+1;
- }
-}
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
deleted file mode 100644
index 9570c6dd3af..00000000000
--- a/tests/journal/control2.c
+++ /dev/null
@@ -1,19 +0,0 @@
-/* run.config
- COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
- CMD: @frama-c@ @PTEST_OPTIONS@
- PLUGIN: @EVA_PLUGINS@
- EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name @PTEST_RESULT@/control_journal2.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
- SCRIPT: @PTEST_RESULT@/control_journal2.ml
- EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml @frama-c@ -journal-enable -lib-entry -journal-name @PTEST_RESULT@/control_journal_next2.ml @PTEST_FILE@ > @PTEST_RESULT@/control2_sav.res 2> @PTEST_RESULT@/control2_sav.err
- SCRIPT: @PTEST_RESULT@/control_journal_next2.ml
- OPT:
-*/
-int x,y,c,d;
-void f() {
- int i;
- for(i=0; i<4 ; i++) {
- if (c) { if (d) {y++;} else {x++;}}
- else {};
- x=x+1;
- }
-}
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
deleted file mode 100644
index 5ae163e21ff..00000000000
--- a/tests/journal/intra.i
+++ /dev/null
@@ -1,119 +0,0 @@
-/* run.config
- COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
- CMD: @frama-c@ @PTEST_OPTIONS@
- PLUGIN: @EVA_PLUGINS@ sparecode
- MODULE: @PTEST_NAME@
- EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name @PTEST_RESULT@/intra_journal.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
- SCRIPT: @PTEST_RESULT@/intra_journal.ml
- OPT:
-*/
-
-/* Waiting for results such as:
- * spare code analysis removes statements having variables with
- * prefix "spare_"
- *
- * slicing analysis removes statement having variables with
- * prefix "spare_" and "any_"
- */
-int G;
-
-int tmp (int a) {
- int x = a;
- //@ assert x == a ;
- int w = 1;
- //@ assert w == 1 ; // w is not spare or else
- // the assertion should be removed !
- int spare_z = 1;
- int spare_y = a+spare_z;
- return x;
-}
-
-int param (int a, int spare_b) {
- return a;
-}
-
-int spare_called_fct (int a) {
- return a;
-}
-
-int two_outputs (int a, int b) {
- G += b;
- return a;
-}
-
-int call_two_outputs (void) {
- int x, spare_y;
- int any_b = 1;
- int any_a = 2;
- int a = 1;
- int b = any_b;
- x = two_outputs (a, b);
- G = 1; /* don't use b = any_b; */
- b = 2;
- a = any_a;
- spare_y = two_outputs (a, b);
- /* don't use spare_y so don't use a = any_a */
- return x;
-}
-
-void assign (int *p, int *q) {
- *p = *q ;
-}
-
-int loop (int x, int y, int z) {
- int i = 0;
- //@ assert i < z ;
- //@ loop invariant i < y ;
- /* should keep y in sparecode analysis even if it is not used in the function */
- while (i < x) {
- i ++;
- }
- return i;
-}
-
-void stop(void) __attribute__ ((noreturn)) ;
-
-int main (int noreturn, int halt) {
- int res = 0;
- int spare_tmp = 3;
- int spare_param = 2 + spare_tmp;
- int spare_ref = 3;
- int x = 1;
- int y = 2;
- res += param (2, spare_param);
- res += tmp (4);
- spare_called_fct (5);
- res += call_two_outputs ();
- res += loop (10, 15, 20);
- assign (&x, &spare_ref) ; /* <- Here, best can be done for spare analysis */
- assign (&x, &y) ;
- if (noreturn) {
- if (halt)
- stop () ;
- else
- while (1);
- //@ assert \false ; // What should be done with
- // assertions related to dead code?
- }
-
- return res + G + x;
-}
-
-/*-------------------------------------*/
-struct { struct { int x; int y; } a; int b; } X10;
-int Y10;
-int f10 (int x) {
- //@ slice pragma expr X10;
- //@ slice pragma expr X10.a;
- //@ slice pragma expr X10.a.x;
- //@ slice pragma expr Y10;
- //@ assert X10.a.x >= 0;
- return x;
-}
-int main2 () {
- Y10 = 0;
- X10.b = 0;
- X10.a.y += f10 (3);
- return X10.a.x + X10.a.y;
-}
-/*-------------------------------------*/
diff --git a/tests/journal/intra.ml b/tests/journal/intra.ml
deleted file mode 100644
index 0962a714022..00000000000
--- a/tests/journal/intra.ml
+++ /dev/null
@@ -1,4 +0,0 @@
-let () =
- Db.Main.extend (fun _ ->
- ignore (Sparecode.Register.get ~select_annot:true
- ~select_slice_pragma:true))
diff --git a/tests/journal/oracle/control.0.res.oracle b/tests/journal/oracle/control.0.res.oracle
deleted file mode 100644
index 8191206632c..00000000000
--- a/tests/journal/oracle/control.0.res.oracle
+++ /dev/null
@@ -1,38 +0,0 @@
-[kernel] Parsing control.i (no preprocessing)
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva] control.i:24: starting to merge loop iterations
-[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
-[eva] Recording results for f
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- x FROM x (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function f:
- x; i
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
deleted file mode 100644
index ae023e8b822..00000000000
--- a/tests/journal/oracle/control.1.res.oracle
+++ /dev/null
@@ -1,71 +0,0 @@
-[kernel] Parsing control.i (no preprocessing)
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva] control.i:24: starting to merge loop iterations
-[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
-[eva] Recording results for f
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- x FROM x (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
-[eva] Recording results for f
-[from] Computing for function f
-[from] Done for function f
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] entry point:
- x FROM x (and SELF)
-[from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] Out (internal) for function f:
- x; i
diff --git a/tests/journal/oracle/control.2.res.oracle b/tests/journal/oracle/control.2.res.oracle
deleted file mode 100644
index 2c9d316b3d6..00000000000
--- a/tests/journal/oracle/control.2.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-1
-2
-3
-1
-2
-3
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
deleted file mode 100644
index 97fb53bb8f6..00000000000
--- a/tests/journal/oracle/control2.res.oracle
+++ /dev/null
@@ -1,73 +0,0 @@
-[kernel] Parsing control2.c (with preprocessing)
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva] control2.c:14: starting to merge loop iterations
-[eva:alarm] control2.c:17: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[eva] Analyzing an incomplete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ [--..--]
- y ∈ [--..--]
- c ∈ [--..--]
- d ∈ [--..--]
-[eva:alarm] control2.c:15: Warning:
- signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:15: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva:alarm] control2.c:17: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [--..--]
- y ∈ [--..--]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 12 statements reached (out of 12): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 3 alarms generated by the analysis:
- 3 integer overflows
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- x FROM x; c; d (and SELF)
- y FROM y; c; d (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function f:
- x; y; i
diff --git a/tests/journal/oracle/control2_sav.err b/tests/journal/oracle/control2_sav.err
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res
deleted file mode 100644
index 1734f9bb537..00000000000
--- a/tests/journal/oracle/control2_sav.res
+++ /dev/null
@@ -1,77 +0,0 @@
-[kernel] Parsing control2.c (with preprocessing)
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva] control2.c:14: starting to merge loop iterations
-[eva:alarm] control2.c:17: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
-[eva] Analyzing an incomplete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ [--..--]
- y ∈ [--..--]
- c ∈ [--..--]
- d ∈ [--..--]
-[eva:alarm] control2.c:15: Warning:
- signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:15: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva:alarm] control2.c:17: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [--..--]
- y ∈ [--..--]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 12 statements reached (out of 12): 100% coverage.
- ----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 0 warnings
- by the Frama-C kernel: 0 errors 1 warning
- ----------------------------------------------------------------------------
- 3 alarms generated by the analysis:
- 3 integer overflows
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- x FROM x; c; d (and SELF)
- y FROM y; c; d (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function f:
- x; y; i
-[kernel] writing journal in file `control_journal_next2.ml'.
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
deleted file mode 100644
index 052f7084bea..00000000000
--- a/tests/journal/oracle/intra.res.oracle
+++ /dev/null
@@ -1,116 +0,0 @@
-[kernel] Parsing intra.i (no preprocessing)
-[sparecode] remove unused code...
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- G ∈ {0}
- X10 ∈ {0}
- Y10 ∈ {0}
-[eva] computing for function param <- main.
- Called from intra.i:83.
-[eva] Recording results for param
-[eva] Done for function param
-[eva] computing for function tmp <- main.
- Called from intra.i:84.
-[eva] intra.i:22: assertion got status valid.
-[eva] intra.i:24: assertion got status valid.
-[eva] Recording results for tmp
-[eva] Done for function tmp
-[eva] computing for function spare_called_fct <- main.
- Called from intra.i:85.
-[eva] Recording results for spare_called_fct
-[eva] Done for function spare_called_fct
-[eva] computing for function call_two_outputs <- main.
- Called from intra.i:86.
-[eva] computing for function two_outputs <- call_two_outputs <- main.
- Called from intra.i:50.
-[eva] Recording results for two_outputs
-[eva] Done for function two_outputs
-[eva] computing for function two_outputs <- call_two_outputs <- main.
- Called from intra.i:54.
-[eva] Recording results for two_outputs
-[eva] Done for function two_outputs
-[eva] Recording results for call_two_outputs
-[eva] Done for function call_two_outputs
-[eva] computing for function loop <- main.
- Called from intra.i:87.
-[eva] intra.i:65: assertion got status valid.
-[eva] intra.i:66: loop invariant got status valid.
-[eva] intra.i:68: starting to merge loop iterations
-[eva] Recording results for loop
-[eva] Done for function loop
-[eva] computing for function assign <- main.
- Called from intra.i:88.
-[eva] Recording results for assign
-[eva] Done for function assign
-[eva] computing for function assign <- main.
- Called from intra.i:89.
-[eva] Recording results for assign
-[eva] Done for function assign
-[kernel:annot:missing-spec] intra.i:92: Warning:
- Neither code nor specification for function stop, generating default assigns from the prototype
-[eva] computing for function stop <- main.
- Called from intra.i:92.
-[eva] using specification for function stop
-[eva] Done for function stop
-[eva] Recording results for main
-[eva] done for function main
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 8 functions analyzed (out of 10): 80% coverage.
- In these functions, 58 statements reached (out of 59): 98% coverage.
- ----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 0 warnings
- by the Frama-C kernel: 0 errors 1 warning
- ----------------------------------------------------------------------------
- 0 alarms generated by the analysis.
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 4 valid 0 unknown 0 invalid 4 total
- Preconditions 0 valid 0 unknown 0 invalid 0 total
- 100% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
-[pdg] computing for function main
-[from] Computing for function param
-[from] Done for function param
-[from] Computing for function tmp
-[from] Done for function tmp
-[from] Computing for function spare_called_fct
-[from] Done for function spare_called_fct
-[from] Computing for function call_two_outputs
-[from] Computing for function two_outputs <-call_two_outputs
-[from] Done for function two_outputs
-[from] Done for function call_two_outputs
-[from] Computing for function loop
-[from] Done for function loop
-[from] Computing for function assign
-[from] Done for function assign
-[from] Computing for function stop
-[from] Done for function stop
-[pdg] done for function main
-[pdg] computing for function call_two_outputs
-[pdg] done for function call_two_outputs
-[pdg] computing for function assign
-[pdg] done for function assign
-[pdg] computing for function loop
-[pdg] done for function loop
-[pdg] computing for function tmp
-[pdg] done for function tmp
-[pdg] computing for function param
-[pdg] done for function param
-[pdg] computing for function two_outputs
-[pdg] done for function two_outputs
-[pdg] computing for function f10
-[pdg] Warning: unreachable entry point (sid:79, function f10)
-[pdg] Bottom for function f10
-[pdg] computing for function main2
-[pdg] Warning: unreachable entry point (sid:87, function main2)
-[pdg] Bottom for function main2
-[pdg] computing for function spare_called_fct
-[pdg] done for function spare_called_fct
-[pdg] computing for function stop
-[pdg] done for function stop
-[sparecode] remove unused global declarations...
-[sparecode] result in new project 'default without sparecode'.
diff --git a/tests/journal/test_config b/tests/journal/test_config
deleted file mode 100644
index 5b4e9a8bdd2..00000000000
--- a/tests/journal/test_config
+++ /dev/null
@@ -1,2 +0,0 @@
-PLUGIN:
-STDOPT:
diff --git a/tests/journal/use_cpt.ml b/tests/journal/use_cpt.ml
deleted file mode 100644
index f19b3e11a7f..00000000000
--- a/tests/journal/use_cpt.ml
+++ /dev/null
@@ -1,20 +0,0 @@
-
-let main () =
- let module T = Type.Abstract(struct let name = "Abstract_cpt.t" end) in
- let c =
- Dynamic.get
- ~plugin:"Abstract_cpt" "mk" (Datatype.func Datatype.unit T.ty) ()
- in
- let incr =
- Dynamic.get
- ~plugin:"Abstract_cpt" "incr" (Datatype.func T.ty Datatype.int)
- in
- let pretty =
- Dynamic.get
- ~plugin:"Abstract_cpt" "pretty" (Datatype.func T.ty Datatype.unit)
- in
- let incr_and_pretty c = ignore (incr c); pretty c in
- for _i = 1 to 3 do incr_and_pretty c done
-
-let () = Db.Main.extend main
-
--
GitLab