diff --git a/Changelog b/Changelog
index 356c0d9f00df51165f5a03714c12c180256bd2db..89126925807b1f70a5c6a1ac8265ecad0f82796d 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,15 @@
Open Source Release <next-release>
##################################
+-* Kernel [2019/08/20] Fixes a rare but critical bug which occured when
+ Frama-C internally switched the current project in presence of >2
+ projects and destroyed the old current project at about the same
+ time: the Frama-C internal state became inconsistent and lead to
+ unsound computations and crashes. It may be revealed to the
+ end-user when using a long sequence of -then-replace (at least 3
+ of them).
+-* Kernel [2019/08/20] Fixed sequence of -removed-projects and -then
+ options.
o Ptests [2019/08/05] Add new MODULE directive for compiling and loading
an auxiliary OCaml module for a test
- Kernel [2019/08/05] Add -keep-unused-types normalization option
diff --git a/Makefile b/Makefile
index f1bd75c77b82ed090b286126906ca855c90d89b8..43c11ae3d2657d51b590cd0944d0d2d696344025 100644
--- a/Makefile
+++ b/Makefile
@@ -453,7 +453,8 @@ LIB_CMO =\
src/libraries/stdlib/integer \
src/libraries/utils/json \
src/libraries/utils/markdown \
- src/libraries/utils/rich_text
+ src/libraries/utils/rich_text \
+ src/libraries/utils/dotgraph
NON_OPAQUE_DEPS+=\
src/libraries/datatype/unmarshal_z \
diff --git a/Makefile.generating b/Makefile.generating
index 12dd18b3f0afb4cb03bfaf8a9e8a9e682730a238..31a445a75ca111f32afc84a2b6a6748409d9436f 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -133,11 +133,23 @@ ifeq ($(HAS_OCAML408),yes)
Format.String_tag str -> str \
| _ -> raise (Invalid_argument "unsupported tag extension")
FORMAT_STAG_OF_STRING=Format.String_tag s
+ HAS_OCAML407_OR_408=yes
else
DYNLINK_INIT=Dynlink.init
FORMAT_STAG=tag
FORMAT_STRING_OF_STAG=s
FORMAT_STAG_OF_STRING=s
+ ifeq ($(HAS_OCAML407),yes)
+ HAS_OCAML407_OR_408=yes
+ else
+ HAS_OCAML407_OR_408=no
+ endif
+endif
+
+ifeq ($(HAS_OCAML407_OR_408),yes)
+ FLOAT_MAX_FLOAT=Float.max_float
+else
+ FLOAT_MAX_FLOAT=Pervasives.max_float
endif
src/libraries/stdlib/transitioning.ml: \
@@ -153,6 +165,7 @@ src/libraries/stdlib/transitioning.ml: \
-e 's/@ASSOC_OPT@/$(ASSOC_OPT)/g' \
-e 's/@ASSQ_OPT@/$(ASSQ_OPT)/g' \
-e 's/@DYNLINK_INIT@/$(DYNLINK_INIT)/g' \
+ -e 's/@FLOAT_MAX_FLOAT@/$(FLOAT_MAX_FLOAT)/g' \
-e 's/@FORMAT_STAG@/$(FORMAT_STAG)/g' \
-e 's/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g' \
-e 's/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g' \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 2fb69fa83c4e5a138cd2c1289ebecb6d2be67232..ec689685fd2bca4b2d4bbccc5c6a0a52487960c1 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -648,6 +648,8 @@ src/libraries/utils/cilconfig.ml: CIL
src/libraries/utils/cilconfig.mli: CIL
src/libraries/utils/command.ml: CEA_LGPL
src/libraries/utils/command.mli: CEA_LGPL
+src/libraries/utils/dotgraph.ml: CEA_LGPL
+src/libraries/utils/dotgraph.mli: CEA_LGPL
src/libraries/utils/escape.ml: CIL
src/libraries/utils/escape.mli: CIL
src/libraries/utils/filepath.ml: CEA_LGPL
diff --git a/opam/opam b/opam/opam
index 0c0a81eaa9a61b5d9886d6386a24d3c28c80cbde..3b6424cf61d919a5f75ebeb120dd05eb2d6a6d04 100644
--- a/opam/opam
+++ b/opam/opam
@@ -94,7 +94,7 @@ depends: [
( ( "lablgtk" { >= "2.18.2" } & "conf-gnomecanvas" )
| ( "lablgtk3" { >= "3.0.beta4" & os!="macos" } & "lablgtk3-sourceview3" ))
"conf-gtksourceview"
- ( "alt-ergo-free" | "alt-ergo" { <= "2.2.0" } )
+ ( "alt-ergo-free" | "alt-ergo" )
"conf-graphviz" { post }
"yojson"
]
diff --git a/share/libc/__fc_select.h b/share/libc/__fc_select.h
index 82a079e98bd4fab78b03020d910170aaa3b64b1e..226cab728c71b687a44893152ae307cd1af3e012 100644
--- a/share/libc/__fc_select.h
+++ b/share/libc/__fc_select.h
@@ -51,11 +51,7 @@ extern int pselect(int nfds, fd_set * readfds,
requires errorfds: errorfds == \null || \valid(errorfds);
requires timeout: timeout == \null || \valid(timeout);
assigns __fc_fds_state \from __fc_fds_state;
- assigns readfds == \null ? \empty : *readfds,
- writefds == \null ? \empty : *writefds,
- errorfds == \null ? \empty : *errorfds,
- timeout == \null ? \empty : *timeout,
- \result
+ assigns *readfds, *writefds, *errorfds, *timeout, \result
\from indirect:nfds,
indirect:readfds, indirect:*readfds,
indirect:writefds, indirect:*writefds,
diff --git a/share/libc/signal.h b/share/libc/signal.h
index f42d35711ab12190c0f7e2900f36ce4a2b922333..27ae78965980e8df8e4473bf131b5c445da1faa8 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -205,8 +205,8 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
requires valid_oldact_or_null: oldact == \null || \valid(oldact);
requires valid_read_act_or_null: act == \null || \valid_read(act);
requires separation:separated_acts: \separated(act, oldact);
- assigns oldact == \null ? \empty : *oldact \from __fc_p_sigaction;
- assigns act == \null ? \empty : __fc_p_sigaction[signum] \from *act;
+ assigns *oldact \from __fc_p_sigaction;
+ assigns __fc_p_sigaction[signum] \from *act;
assigns \result \from indirect:signum, indirect:act, indirect:*act,
indirect:oldact, indirect:*oldact;
ensures act_changed: act == \null || \subset(__fc_p_sigaction[signum], *act);
@@ -225,8 +225,7 @@ extern int sigaction(int signum, const struct sigaction *restrict act,
requires separation: (set == oldset == \null) ||
\separated(set, oldset);
assigns \result \from indirect:how, indirect:set, indirect:oldset;
- assigns oldset == \null ? \empty : *oldset
- \from indirect:how, indirect:oldset;
+ assigns *oldset \from indirect:how, indirect:oldset;
ensures result_ok_or_error: \result == 0 || \result == -1;
ensures initialization:oldset_initialized:
oldset != \null && \result == 0 ==> \initialized(oldset);
diff --git a/share/libc/stropts.h b/share/libc/stropts.h
index 48351585e7e3537806592d6ac9d2d6cf81d9f2af..3b0ee82968b303fbf98723c0d45d05198c11e4ea 100644
--- a/share/libc/stropts.h
+++ b/share/libc/stropts.h
@@ -172,7 +172,7 @@ extern int __va_ioctl_int(int fd, int request, int arg);
/*@ assigns \result \from indirect:fd, indirect:request,
indirect:((char*)argp)[0..];
- assigns argp != \null ? ((char*)argp)[0..] : \empty \from
+ assigns ((char*)argp)[0..] \from
indirect:fd, indirect:request, ((char*)argp)[0..]; */
extern int __va_ioctl_ptr(int fd, int request, void* argp);
diff --git a/share/libc/sys/time.h b/share/libc/sys/time.h
index 73fed482445f4c6a663ae88e8535b45fc5c704a8..b860763f4d3909a5c198a66af5701417801f78c9 100644
--- a/share/libc/sys/time.h
+++ b/share/libc/sys/time.h
@@ -151,16 +151,16 @@ extern int getitimer(int which, struct itimerval *curr_value);
/*@
requires valid_new_value: \valid_read(new_value);
requires old_value_null_or_valid: old_value == \null || \valid(old_value);
- assigns old_value != \null ? *old_value : \empty \from
- indirect:which, indirect:old_value, indirect:new_value,
- __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
+ assigns *old_value \from indirect:which, indirect:old_value,
+ indirect:new_value, __fc_itimer_real,
+ __fc_itimer_virtual, __fc_itimer_prof;
assigns \result \from indirect:which, indirect:new_value, indirect:*new_value;
ensures result_ok_or_error: \result == 0 || \result == -1;
behavior real:
assumes itimer_real_and_valid:
which == ITIMER_REAL && __VALID_ITIMERVAL(new_value);
assigns \result \from \nothing;
- assigns old_value != \null ? *old_value : \empty \from __fc_itimer_real;
+ assigns *old_value \from __fc_itimer_real;
assigns __fc_itimer_real \from *new_value;
ensures result_ok: \result == 0;
ensures initialization:old_value: \initialized(old_value);
@@ -168,14 +168,14 @@ extern int getitimer(int which, struct itimerval *curr_value);
assumes itimer_virtual_and_valid:
which == ITIMER_VIRTUAL && __VALID_ITIMERVAL(new_value);
assigns \result \from \nothing;
- assigns old_value != \null ? *old_value : \empty \from __fc_itimer_virtual;
+ assigns *old_value \from __fc_itimer_virtual;
ensures result_ok: \result == 0;
ensures initialization:old_value: \initialized(old_value);
behavior prof:
assumes itimer_prof_and_valid:
which == ITIMER_PROF && __VALID_ITIMERVAL(new_value);
assigns \result \from \nothing;
- assigns old_value != \null ? *old_value : \empty \from __fc_itimer_prof;
+ assigns *old_value \from __fc_itimer_prof;
ensures result_ok: \result == 0;
ensures initialization:old_value: \initialized(old_value);
behavior invalid:
diff --git a/share/libc/time.h b/share/libc/time.h
index 60e5031571f9ef5e2d527e9b5e8a81907ae66a36..52c66700cc80c3df73b708b8f6a302a30b2d6877 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -216,9 +216,8 @@ extern int clock_gettime(clockid_t clk_id, struct timespec *tp);
assumes no_einval: valid_clock_id(clock_id);
assigns \result \from indirect:__fc_time, indirect:clock_id, indirect:rqtp,
indirect:*rqtp;
- assigns rmtp == \null ? \empty : *rmtp \from __fc_time, indirect:clock_id,
- indirect:rqtp, indirect:*rqtp,
- indirect:rmtp;
+ assigns *rmtp \from __fc_time, indirect:clock_id, indirect:rqtp,
+ indirect:*rqtp, indirect:rmtp;
ensures result_interrupted: \result == EINTR;
ensures initialization:interrupted_remaining:
rmtp != \null ==> \initialized(&rmtp->tv_sec) && \initialized(&rmtp->tv_nsec);
@@ -263,9 +262,8 @@ extern struct tm *localtime_r(const time_t *restrict timep,
requires valid_nanosecs: 0 <= rqtp->tv_nsec < 1000000000;
requires valid_remaining_or_null: rmtp == \null || \valid(rmtp);
assigns \result \from indirect:__fc_time, indirect:rqtp, indirect:*rqtp;
- assigns rmtp == \null ? \empty : *rmtp \from indirect:__fc_time,
- indirect:rqtp, indirect:*rqtp,
- indirect:rmtp;
+ assigns *rmtp \from indirect:__fc_time, indirect:rqtp, indirect:*rqtp,
+ indirect:rmtp;
ensures result_elapsed_or_interrupted: \result == 0 || \result == -1;
ensures initialization:interrupted_remaining:
rmtp != \null && \result == -1 ==>
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 9aecb292da713a7214e26574f10a62229de8f029..7448601a76488d7a93c75987b7b33f8a9e6d434e 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -138,8 +138,9 @@ let () =
(* Load Frama-c from disk if required *)
let load_binary () =
- let filename = Kernel.LoadState.get () in
- if filename <> "" then begin
+ let filepath = Kernel.LoadState.get () in
+ if filepath <> Filepath.Normalized.unknown then begin
+ let filename = Filepath.Normalized.to_pretty_string filepath in
try
Project.load_all filename
with Project.IOError s ->
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 1b595764bf03ef02f94a6901f87658e97ab5b21d..a8012c9c465ba4586ebad9e4b558678c24d625ee 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5230,7 +5230,7 @@ and makeCompType ghost (isstruct: bool)
if Cil.isFunctionType ftype then
Kernel.error ~current:true
"field `%s' declared as a function" n
- else if Cil.has_flexible_array_member ftype then
+ else if Cil.has_flexible_array_member ftype && isstruct then
Kernel.error ~current:true
"field `%s' declared with a type containing a flexible array member."
n
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index d74de525bfa58a548f5990215ab66750e7423ef6..d20cc20285af3175eabfb4202058616734e426ae 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -442,6 +442,91 @@ struct
module Empty_string(X: Parameter_sig.Input_with_arg) =
String(struct include X let default = empty_string end)
+ (* ************************************************************************ *)
+ (** {3 Filepath} *)
+ (* ************************************************************************ *)
+
+ module Fc_Filepath = Filepath
+
+ module Filepath
+ (X: sig
+ include Parameter_sig.Input_with_arg
+ val existence : Parameter_sig.existence
+ end) =
+ struct
+
+ exception No_file
+ exception File_exists
+
+ include Build
+ (struct
+ include Datatype.Filepath
+ include X
+ let default () = Filepath.Normalized.unknown
+ let functor_name = "Filepath"
+ end)
+
+ let check_existence existence fp =
+ match existence with
+ | Parameter_sig.Indifferent -> ()
+ | Parameter_sig.Must_exist ->
+ if not (Sys.file_exists (Filepath.Normalized.to_pretty_string fp)) then
+ raise No_file
+ | Parameter_sig.Must_not_exist ->
+ if Sys.file_exists (Filepath.Normalized.to_pretty_string fp) then
+ raise File_exists
+
+ let existence = X.existence
+
+ let convert f oldstr newstr =
+ let oldfp = Filepath.Normalized.to_pretty_string oldstr in
+ let newfp = Filepath.Normalized.to_pretty_string newstr in
+ f oldfp newfp
+
+ let set fp = check_existence existence fp ; set fp
+
+ let set_str s = set (Filepath.Normalized.of_string s)
+
+ let add_option name =
+ Cmdline.add_option
+ name
+ ~argname:X.arg_name
+ ~help:X.help
+ ~visible:is_visible
+ ~ext_help:!Parameter_customize.optional_help_ref
+ ~plugin:P.shortname
+ ~group
+ stage
+ (Cmdline.String set_str)
+
+ let parameter_get fp = Filepath.Normalized.to_pretty_string (get fp)
+ let parameter_add_set_hook f = add_set_hook (convert f)
+ let parameter_add_update_hook f = add_update_hook (convert f)
+
+ let parameter =
+ let accessor =
+ Typed_parameter.String
+ ({ Typed_parameter.get = parameter_get;
+ set = set_str;
+ add_set_hook = parameter_add_set_hook;
+ add_update_hook = parameter_add_update_hook },
+ fun () -> [])
+ in
+ let p =
+ Typed_parameter.create ~name ~help:X.help ~accessor ~is_set
+ in
+ add_parameter !Parameter_customize.group_ref stage p;
+ add_option X.option_name;
+ Parameter_customize.reset ();
+ if is_dynamic then
+ let plugin = empty_string in
+ Dynamic.register
+ ~plugin X.option_name Typed_parameter.ty ~journalize:false p
+ else
+ p
+
+ end
+
(* ************************************************************************ *)
(** {3 Collections} *)
(* ************************************************************************ *)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index bb827691793567e0bbe804f712a2fb7293d5a96b..a36076d68471974e040e4d0cebef792d3d185d74 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -321,6 +321,24 @@ module type Specific_dir = sig
end
+type existence = Must_exist | Must_not_exist | Indifferent
+
+(** signature for normalized pathnames. *)
+module type Filepath = sig
+
+ exception No_file
+ (** raised by {!set} if no file exists and [existence] is [Must_exist]. *)
+
+ exception File_exists
+ (** raised by {!set} if some file exists and [existence] is
+ [Must_nos_exist]. *)
+
+ val existence: existence
+
+ include S with type t = Filepath.Normalized.t
+
+end
+
(* ************************************************************************** *)
(** {3 Collections} *)
(* ************************************************************************** *)
@@ -515,6 +533,13 @@ module type Builder = sig
(** @plugin development guide *)
module Empty_string(X: Input_with_arg): String
+ module Fc_Filepath = Filepath
+
+ module Filepath(X: sig
+ include Input_with_arg
+ val existence: existence
+ end): Filepath
+
exception Cannot_build of string
module Make_set
(E:
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 10241320736c4495275430db1a8a6ac2bbecc563..f686cd7684e27896afc96eae7409215a3f6d11be 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -445,6 +445,14 @@ module Parameter = struct
let modname = "String"
end)
+ module Filepath =
+ Common
+ (struct
+ type t = Datatype.Filepath.t
+ let ty = Datatype.Filepath.ty
+ let modname = "Filepath"
+ end)
+
module StringSet = struct
include Common
(struct include Datatype.String.Set let modname = "StringSet" end)
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index c837a15601e045eb08dfe2a936ba8c4960687689..3650174dc2a424590dc3ba3473e6db44c1abc3be 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -118,6 +118,9 @@ module Parameter : sig
(** String parameters. *)
module String : Common with type t = string
+ (** Filepath parameters. *)
+ module Filepath : Common with type t = Datatype.Filepath.t
+
(** Set of string parameters. *)
module StringSet : sig
include Common with type t = Datatype.String.Set.t
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 02f357e8ebbc52cf9fb7883e3551c04d322a9a6b..3bcff739e6a5064f21a7fd18923c3992c43c6ce3 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -716,10 +716,11 @@ let () = Parameter_customize.set_cmdline_stage Cmdline.Loading
reset *)
(*let () = Parameter_customize.do_not_projectify ()*)
module LoadState =
- P.Empty_string
+ P.Filepath
(struct
let option_name = "-load"
let arg_name = "filename"
+ let existence = Parameter_sig.Must_exist
let help = "load a previously-saved session from file <filename>"
end)
@@ -1522,7 +1523,14 @@ let _ =
let () =
Cmdline.run_after_configuring_stage
- (fun () -> Remove_projects.iter (fun project -> Project.remove ~project ()))
+ (fun () ->
+ (* clear "-remove-projects" before itering over (a copy of) its contents
+ in order to prevent warnings about dangling pointer deletion (since it
+ is itself projectified and so contains a pointer to the project being
+ removed). *)
+ let s = Remove_projects.get () in
+ Remove_projects.clear ();
+ Project.Datatype.Set.iter (fun project -> Project.remove ~project ()) s)
(* ************************************************************************* *)
(** {2 Others options} *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 7976e6c86673f65f73788c64e6a77b384b0a0fed..0b43666bb0891fda4c20fae462daa956571e9dec 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -299,7 +299,7 @@ module BigIntsHex: Parameter_sig.Int
module SaveState: Parameter_sig.String
(** Behavior of option "-save" *)
-module LoadState: Parameter_sig.String
+module LoadState: Parameter_sig.Filepath
(** Behavior of option "-load" *)
module LoadModule: Parameter_sig.String_list
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index f24bdbcfb2680fd819c456b99b0c6d7ca87c8dd9..01d5831cbe50b7cc0048d60f594a888d4a58ad32 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -534,7 +534,7 @@ struct
let pp_source fmt = function
| None -> ()
- | Some src -> Format.fprintf fmt "%a:" Filepath.pp_pos src
+ | Some src -> Format.fprintf fmt "%a:" Fc_Filepath.pp_pos src
end
(* Output must be synchronized with functions [prefix_*] in module Log. *)
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 55280721f01c32fbc314ed7bc74e1571363aae86..27ff62f432dcb24838c06800b3c6a07c4da9e4f8 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -361,6 +361,9 @@ let journalized_set_current =
let set_current ?(on=false) ?(selection=State_selection.full) p =
if not (equal p (current ())) then journalized_set_current on selection p
+let set_current_as_last_created () =
+ Extlib.may (fun p -> set_current p) !last_created_by_copy_ref
+
(** Indicates if we should keep [p] as the current project when calling {!on p}. *)
let keep_current: bool ref = ref false
@@ -376,12 +379,12 @@ let on ?selection p f x =
if old_current == p then f x
else
let set p = set_current ~on:true ?selection p in
- let set_to_old () =
+ let rec set_to_old old =
if not !keep_current then
try
(* if someone asks for keeping [p] as current during the execution of
[f], do not restore [old_current] at the end. *)
- set old_current
+ set old
with Invalid_argument _ ->
(* the old current project has been remove: replace it by the previous
one, if any *)
@@ -390,16 +393,16 @@ let on ?selection p f x =
old_current.unique_name
(current ()).unique_name
else
- Q.move_at_top (Q.nth 1 projects) projects
+ set_to_old (Q.nth 1 projects)
in
let go () =
set p;
let r = f x in
- set_to_old ();
+ set_to_old old_current;
r
in
if debug_atleast 1 then go ()
- else begin try go () with e -> set_to_old (); raise e end
+ else begin try go () with e -> set_to_old old_current; raise e end
(* [set_current] must never be called internally. *)
module Hide_set_current = struct let set_current () = assert false end
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index d24b9b72f021aa85a77861a275c364da006b82cf..ec2f4d49c9be6e619e6cd6dc672ffe4a53f31c8e 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -142,6 +142,10 @@ val set_keep_current: bool -> unit
of the current {!on}) iff [b] is [true].
@since Aluminium-20160501 *)
+(**/**)
+val set_current_as_last_created: unit -> unit
+(**/**)
+
val copy: ?selection:State_selection.t -> ?src:t -> t -> unit
(** Copy a project into another one. Default project for [src] is [current
()]. Replace the destination by [src].
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index de6215991de78ead186f5deb8cca34095989fb99..cf09ddd667ed096ced79582ad7905f8ddc82ed19 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -37,6 +37,10 @@ module Dynlink = struct
let init = @DYNLINK_INIT@
end
+module Float = struct
+ let max_float = @FLOAT_MAX_FLOAT@
+end
+
module Format = struct
type stag = Format.@FORMAT_STAG@
let string_of_stag s = @FORMAT_STRING_OF_STAG@
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 521cf30c013bf939d5bbecc4444a682620267319..94ae54311a9ca97d31b0eab45927b7d4454c96c8 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -49,6 +49,11 @@ module Dynlink: sig
val init: unit -> unit
end
+(** 4.07 *)
+module Float: sig
+ val max_float: float
+end
+
(** 4.08 *)
module Format: sig
type stag
diff --git a/src/libraries/utils/dotgraph.ml b/src/libraries/utils/dotgraph.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f9939a2eb3677e29cafc5c34cbdbcbcefc2e07ef
--- /dev/null
+++ b/src/libraries/utils/dotgraph.ml
@@ -0,0 +1,405 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Attributes and Such --- *)
+(* -------------------------------------------------------------------------- *)
+
+type attr = [
+ | `LR
+ | `TB
+ | `Label of string
+ | `Color of string
+ | `Fillcolor of string
+ | `Shape of string
+ | `Style of string
+ | `Circle
+ | `Box
+ | `Oval
+ | `Point
+ | `Dotted
+ | `Filled
+ | `ArrowBoth
+ | `ArrowBack
+ | `ArrowForward
+ | `ArrowHead of string
+ | `ArrowTail of string
+ | `Attr of string * string
+]
+
+let attr = function
+ | `LR -> "rankdir" , "LR"
+ | `TB -> "rankdir" , "TB"
+ | `Label txt -> "label" , txt
+ | `Color c -> "color" , c
+ | `Fillcolor c -> "fillcolor" , c
+ | `Shape sh -> "shape" , sh
+ | `Style sty -> "style" , sty
+ | `Box -> "shape" , "box"
+ | `Oval -> "shape" , "oval"
+ | `Point -> "shape" , "point"
+ | `Circle -> "shape" , "circle"
+ | `Filled -> "style" , "filled"
+ | `Dotted -> "style" , "dotted"
+ | `ArrowBoth -> "dir" , "both"
+ | `ArrowBack -> "dir" , "back"
+ | `ArrowForward -> "dir" , "forward"
+ | `ArrowHead sh -> "arrowhead" , sh
+ | `ArrowTail sh -> "arrowtail" , sh
+ | `Attr(name,value) -> name , value
+
+let pp_attr fmt (a : attr) =
+ let name,value = attr a in Format.fprintf fmt "%s=%S" name value
+
+let pp_attributes fmt = function
+ | [] -> ()
+ | p::ps ->
+ begin
+ Format.fprintf fmt "@ %a" pp_attr p ;
+ List.iter (fun p -> Format.fprintf fmt ",@ %a" pp_attr p) ps ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Dot Output --- *)
+(* -------------------------------------------------------------------------- *)
+
+type dot = {
+ file : string ;
+ queue : (unit -> unit) Queue.t ;
+ mutable indent : string ;
+ mutable id : int ;
+ mutable fmt : Format.formatter ;
+ mutable out : out_channel option ;
+}
+
+let open_dot ?(name="G") ?(attr=[]) ?(file) () =
+ let file = match file with None -> name ^ ".dot" | Some f -> f in
+ let out = open_out file in
+ let fmt = Format.formatter_of_out_channel out in
+ begin
+ Format.fprintf fmt "digraph %S {@\n" name ;
+ List.iter
+ (fun p ->
+ Format.fprintf fmt " %a ;@\n" pp_attr p
+ ) attr ;
+ Format.pp_print_flush fmt () ;
+ { file ; fmt ;
+ queue = Queue.create () ;
+ indent = " " ; out = Some out ; id = 0 }
+ end
+
+let flush dot =
+ match dot.out with
+ | Some out -> Format.pp_print_flush dot.fmt () ; flush out
+ | None -> ()
+
+let basename f =
+ if Filename.check_suffix f ".dot" then Filename.chop_suffix f ".dot" else f
+
+let installed = ref None
+let is_dot_installed () =
+ match !installed with
+ | Some s -> s
+ | None -> let s = (Sys.command "dot -V" = 0) in installed := Some s ; s
+
+let close dot =
+ match dot.out with
+ | None -> ()
+ | Some out ->
+ begin
+ Format.fprintf dot.fmt "}@." ;
+ dot.fmt <- Format.err_formatter ;
+ Pervasives.flush out ; close_out out ;
+ dot.out <- None ;
+ end
+
+let layout ?(force=false) ?(target="pdf") ?(engine="dot") ?output dot =
+ begin
+ if dot.out <> None then raise (Invalid_argument "DotGraph: not closed") ;
+ let input = dot.file in
+ let output =
+ match output with Some f -> f | None ->
+ Printf.sprintf "%s.%s" (basename dot.file) target in
+ let cmd = Printf.sprintf "dot -K%s -T%s %s -o %s"
+ engine target input output in
+ let status = Sys.command cmd in
+ if status=0 then output else
+ if force then
+ let msg = Printf.sprintf "dot failed with status %d" status in
+ raise (Invalid_argument msg)
+ else dot.file
+ end
+
+let printf dot msg = Format.fprintf dot.fmt msg
+let println dot msg =
+ Format.kfprintf (fun fmt -> Format.pp_print_newline fmt ()) dot.fmt msg
+
+let push dot f = Queue.push f dot.queue
+let pop_all dot =
+ while not (Queue.is_empty dot.queue) do
+ (Queue.pop dot.queue) ()
+ done
+
+(* -------------------------------------------------------------------------- *)
+(* --- Nodes and Edges --- *)
+(* -------------------------------------------------------------------------- *)
+
+type node = string
+
+let fresh ?(prefix="_") dot =
+ let k = dot.id in dot.id <- succ k ; Printf.sprintf "%s%03d" prefix k
+
+let pp_node = Format.pp_print_string
+let pp_edge fmt (a,b) = Format.fprintf fmt "%s -> %s" a b
+
+let pp_stmt dot pp stmt attr =
+ Format.fprintf dot.fmt "%s@[<hv 0>@[<hov 2>%a [%a@]@ ]@];@."
+ dot.indent pp stmt pp_attributes attr
+
+let inode dot ?prefix ?id attr =
+ let a = match id with Some a -> a | None -> fresh ?prefix dot in
+ pp_stmt dot pp_node a attr ; a
+
+let node_default dot attr =
+ pp_stmt dot pp_node "node" attr
+
+let edge_default dot attr =
+ pp_stmt dot pp_node "edge" attr
+
+let node dot id attr = ignore (inode dot ~id attr)
+
+let edge dot a b attr =
+ if attr = []
+ then Format.fprintf dot.fmt "%s%a ;@." dot.indent pp_edge (a,b)
+ else pp_stmt dot pp_edge (a,b) attr
+
+let link dot ps attr =
+ let rec walk dot attr p = function
+ | q :: ps -> edge dot p q attr ; walk dot attr q ps
+ | [] -> ()
+ in match ps with
+ | p :: ps -> walk dot attr p ps
+ | [] -> ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Clustering --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rank dot nodes =
+ begin
+ Format.fprintf dot.fmt "%s@[<hov 2>{ rank=same;" dot.indent ;
+ List.iter (Format.fprintf dot.fmt "@ %s;") nodes ;
+ Format.fprintf dot.fmt "@ }@]@\n" ;
+ end
+
+let subgraph dot ?(cluster=true) attr content =
+ begin
+ let k = dot.id in dot.id <- succ k ;
+ let indent = dot.indent in
+ Format.fprintf dot.fmt "%ssubgraph %s%d {@\n" indent
+ (if cluster then "cluster" else "g") k ;
+ List.iter
+ (fun a -> Format.fprintf dot.fmt "%s %a;@\n" indent pp_attr a) attr ;
+ dot.indent <- indent ^ " " ;
+ content () ;
+ dot.indent <- indent ;
+ Format.fprintf dot.fmt "%s}@\n" indent ;
+ end
+
+type record = [
+ | `Empty
+ | `Hbox of record list
+ | `Vbox of record list
+ | `Label of string
+ | `Port of string * link list * string
+] and link = string * attr list * node
+
+let port a b = if b <> "" then Printf.sprintf "%s:%s" a b else a
+
+module Record =
+struct
+ let hbox = function `Empty -> [] | `Hbox hs -> hs | h -> [h]
+ let vbox = function `Empty -> [] | `Vbox vs -> vs | v -> [v]
+ let (<->) a b = `Vbox (vbox a @ vbox b)
+ let (<|>) a b = `Hbox (hbox a @ hbox b)
+ let link ?(anchor="") ?(attr=[]) node : link = anchor,attr,node
+ let label ?(port="") ?(link=[]) txt : record =
+ if port="" && link=[] then `Label txt else `Port(port,link,txt)
+end
+
+type env = {
+ buffer : Buffer.t ;
+ mutable links : (string * (string * attr list * node) list) list ;
+ mutable port : int ;
+}
+
+let rec mk_record env hv = function
+ | `Empty -> ()
+ | `Label txt -> Buffer.add_string env.buffer txt
+ | `Port(port,links,txt) ->
+ if links <> [] then
+ let port =
+ if port = "" then
+ let p = env.port in env.port <- succ p ; Printf.sprintf "_p%d" p
+ else port in
+ env.links <- (port,links) :: env.links ;
+ Printf.bprintf env.buffer "<%s> %s" port txt
+ | `Hbox rs -> mk_box env hv true rs
+ | `Vbox rs -> mk_box env hv false rs
+
+and mk_box env hv hb = function
+ | [] -> ()
+ | r::rs ->
+ begin
+ let buffer = env.buffer in
+ let boxed = hv <> hb in
+ let hv = not hv in
+ if boxed then Buffer.add_char buffer '{' ;
+ mk_record env hv r ;
+ List.iter (fun r ->
+ Buffer.add_char buffer '|' ;
+ mk_record env hv r
+ ) rs ;
+ if boxed then Buffer.add_char buffer '}' ;
+ end
+
+let irecord dot ?prefix ?id ?(rounded=false) ?(attr=[]) (box : record) =
+ let shape = if rounded then "Mrecord" else "record" in
+ let env = { buffer = Buffer.create 80 ; links = [] ; port = 1 } in
+ mk_record env true box ;
+ let label = Buffer.contents env.buffer in
+ let node = inode dot ?prefix ?id (`Shape shape :: `Label label :: attr) in
+ List.iter
+ (fun (name,links) ->
+ List.iter
+ (fun (anchor,attr,target) ->
+ edge dot (port (port node name) anchor) target attr
+ ) links
+ ) env.links ;
+ node
+
+let record dot node ?rounded ?attr box =
+ ignore (irecord dot ~id:node ?rounded ?attr box)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Indexing --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type Map =
+sig
+ type key
+ type 'a t
+ val empty : 'a t
+ val find : key -> 'a t -> 'a
+ val add : key -> 'a -> 'a t -> 'a t
+end
+
+let kp = ref 0
+
+module Node(M : Map) =
+struct
+ type t = M.key
+
+ let kid = ref 0
+ let prefix = ref None
+ let skip _ _ = ()
+ let once = ref skip
+ let index : node M.t ref = ref M.empty
+
+ let get_prefix () =
+ match !prefix with Some p -> p | None ->
+ let k = !kp in
+ incr kp ;
+ let p =
+ if k < 26 then String.make 1 (char_of_int (int_of_char 'A' + k))
+ else Printf.sprintf "A%d_" k in
+ prefix := Some p ; p
+
+ let get a =
+ try M.find a !index
+ with Not_found ->
+ let k = !kid in incr kid ;
+ let prefix = get_prefix () in
+ let node = Printf.sprintf "%s%03d" prefix k in
+ index := M.add a node !index ; !once a node ; node
+
+ let node dot a attr = node dot (get a) attr
+ let inode dot a attr = inode dot ~id:(get a) attr
+
+ let record dot a ?rounded ?attr box =
+ record dot (get a) ?rounded ?attr box
+
+ let irecord dot a ?rounded ?attr box =
+ irecord dot ~id:(get a) ?rounded ?attr box
+
+ let prefix p = prefix := Some p
+
+ let once f = once := f
+ let push dot f = once (fun a n -> push dot (fun () -> f a n))
+ let clear () = index := M.empty ; kid := 0 ; once skip
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Decorator --- *)
+(* -------------------------------------------------------------------------- *)
+
+type buffer = {
+ label : Buffer.t ;
+ mutable attributes : attr list ;
+}
+
+let apply_label buffer = function
+ | `Label txt ->
+ let buf = buffer.label in
+ Buffer.add_string buf txt ; true
+ | _ -> false
+
+let apply buffer a =
+ if not (apply_label buffer a) then
+ let name = fst (attr a) in
+ let filter name a = fst (attr a) <> name in
+ buffer.attributes <- a :: List.filter (filter name) buffer.attributes
+
+let add_attr buffer a = List.iter (apply buffer) a
+
+let buffer attr =
+ let buffer = { label = Buffer.create 20 ; attributes = [] } in
+ add_attr buffer attr ; buffer
+
+let add_char buffer = Buffer.add_char buffer.label
+let add_label buffer = Buffer.add_string buffer.label
+let bprintf buffer msg =
+ let fmt = Format.formatter_of_buffer buffer.label in
+ Format.kfprintf (fun fmt -> Format.pp_print_flush fmt ()) fmt msg
+
+let attributes buffer =
+ let label = Buffer.contents buffer.label in
+ `Label label :: List.rev buffer.attributes
+
+let add_options buffer options =
+ List.iter (fun (b,a) -> if b then add_attr buffer a) options
+
+let decorate attr options =
+ let buffer = buffer attr in
+ add_options buffer options ; attributes buffer
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/libraries/utils/dotgraph.mli b/src/libraries/utils/dotgraph.mli
new file mode 100644
index 0000000000000000000000000000000000000000..778b90740259b2e4109a5ea98cc3e7a04c495f99
--- /dev/null
+++ b/src/libraries/utils/dotgraph.mli
@@ -0,0 +1,280 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Helper for Printing Dot-graphs.
+
+ This module provides smart-constructors for constructing Dot input
+ files. Basically, a [dot] object is a buffer to a [<file.dot>] on
+ disk where smart constructors write Dot statements.
+
+ Once the [<file.dot>] has been created, it is possible to layout it
+ by running the [dot] command with various engines.
+
+ Typically, let say you have a graph with nodes of type
+ [M.elt] with [M : Map.S] and assumes the graph is stored
+ as a map [graph : M.elt list M.t] with [roots : M.elt list]
+ then you can use:
+
+ {[
+ let module G = Dotgraph in
+ let module N = G.Node(M) in
+ begin
+ let dot = G.open_dot ~name:"mygraph" () in
+ (* For each generated node, declare it and link to its children. *)
+ N.push dot
+ (fun a ->
+ let na = N.inode dot a in
+ try
+ List.iter
+ (fun b -> G.link dot na (N.get b))
+ (M.find a graph)
+ with Not_found -> ()) ;
+ (* Starts by emitting roots *)
+ List.iter
+ (fun r -> ignore (N.get r))
+ roots ;
+ (* Proceeds to the traversal *)
+ G.pop_all dot ;
+ (* You may then complete your graph
+ with other decorations after the traversal... *)
+ G.close dot ;
+ (* Now call the layout engine, if installed. *)
+ G.layout dot ~format:"pdf" () ;
+ end
+ ]}
+
+*)
+
+open Pretty_utils
+
+(** {1 Attributes} *)
+
+type attr = [
+ | `LR
+ | `TB
+ | `Label of string
+ | `Color of string
+ | `Fillcolor of string
+ | `Shape of string
+ | `Style of string
+ | `Circle
+ | `Box
+ | `Oval
+ | `Point
+ | `Dotted
+ | `Filled
+ | `ArrowBoth
+ | `ArrowBack
+ | `ArrowForward
+ | `ArrowHead of string
+ | `ArrowTail of string
+ | `Attr of string * string
+]
+
+val pp_attr : Format.formatter -> attr -> unit
+
+(** {1 Dot Ouput} *)
+
+type dot
+(** Buffer to a [dot] file with a graph environment (nodes, edges, etc.) *)
+
+val open_dot : ?name:string -> ?attr:attr list -> ?file:string -> unit -> dot
+val close : dot -> unit
+
+val is_dot_installed : unit -> bool
+(** Memoized *)
+
+val layout :
+ ?force:bool ->
+ ?target:string ->
+ ?engine:string ->
+ ?output:string -> dot -> string
+(** Invoke [dot] command (if installed) with specified target and engine.
+ Defaults are [~force:false], [~target:"pdf"], [~engine:"dot"].
+
+ The [dot] buffer must be {i closed} before being laid out, although you can
+ invoke several layouts.
+
+ Output is stored in [~output] or in a filename derived from the one of [dot].
+ The function returns the generated output file.
+
+ @raise Invalid_argument if [dot] buffer is not closed, or when [dot]
+ command fails and [~force:true] (not by default). *)
+
+val printf : dot -> ('a,Format.formatter,unit,unit) format4 -> 'a
+(** Low-level routine to directly write material in the [dot] file *)
+
+val println : dot -> ('a,Format.formatter,unit,unit) format4 -> 'a
+(** Low-level routine to directly write material with an end-of-line (["\n"])
+ in the [dot] file *)
+
+val flush : dot -> unit
+(** Flushes the [dot] file buffer to disk. *)
+
+(** {1 Nodes and Edges} *)
+
+type node
+
+(** Set default node attributes *)
+val node_default : dot -> attr list -> unit
+
+(** Set default edge attributes *)
+val edge_default : dot -> attr list -> unit
+
+(** Create a fresh node identifier *)
+val fresh : ?prefix:string -> dot -> node
+
+val pp_node : node formatter
+val pp_edge : (node * node) formatter (** [a -> b] *)
+
+(** Set attributes to node *)
+val node : dot -> node -> attr list -> unit
+
+(** Create an edge with attributes *)
+val edge : dot -> node -> node -> attr list -> unit
+
+(** Link the node sequence with attributed edges *)
+val link : dot -> node list -> attr list -> unit
+
+(** Combinaison of [fresh] and [node] *)
+val inode : dot -> ?prefix:string -> ?id:node -> attr list -> node
+
+(** {1 Clustering} *)
+
+val rank : dot -> node list -> unit
+(** Layout nodes at the same rank *)
+
+val subgraph : dot -> ?cluster:bool -> attr list -> (unit -> unit) -> unit
+(** The continuation shall add the graph content in the [dot] file.
+ Clustering is true by default *)
+
+type record = [
+ | `Empty
+ | `Hbox of record list
+ | `Vbox of record list
+ | `Label of string
+ | `Port of string * link list * string
+ (** Port with output edges to other nodes.
+ Use [Record.link] and [Record.label] smart-constructors to create
+ complex ports. *)
+] and link = string * attr list * node
+
+(** Complex node layout. Smart constructors to create records. *)
+module Record :
+sig
+ val (<->) : record -> record -> record
+ val (<|>) : record -> record -> record
+ val link : ?anchor:string -> ?attr:attr list -> node -> link
+ val label : ?port:string -> ?link:link list -> string -> record
+end
+
+(** Create a port to a node, and returns the associated pseudo-node so you
+ can link an edge to it. *)
+val port : node -> string -> node
+
+(** Define the node to be a record *)
+val record : dot -> node ->
+ ?rounded:bool -> ?attr:attr list -> record -> unit
+
+(** Create a new node from a record (combines [fresh] and [record]) *)
+val irecord : dot -> ?prefix:string -> ?id:node ->
+ ?rounded:bool -> ?attr:attr list -> record -> node
+
+(** {1 Node Indexing} *)
+
+module type Map =
+sig
+ type key
+ type 'a t
+ val empty : 'a t
+ val find : key -> 'a t -> 'a
+ val add : key -> 'a -> 'a t -> 'a t
+end
+
+(** Lazily associates a node to any element. *)
+module Node(M : Map) :
+sig
+ type t = M.key
+ val get : t -> node
+ val node : dot -> t -> attr list -> unit
+ val inode : dot -> t -> attr list -> node
+ val record : dot -> t -> ?rounded:bool -> ?attr:attr list -> record -> unit
+ val irecord : dot -> t -> ?rounded:bool -> ?attr:attr list -> record -> node
+ val clear : unit -> unit
+
+ (** Executes the callback {i once} for all created nodes.
+ Any previously registered callback by [once] or [push] is replaced
+ by the new one.
+
+ {b Warning:} the callback is executed as soon as [get] is called
+ for the first time, possibly interfering with your current output
+ on a [dot] buffer. To insert additional Dot material with a callback,
+ use [push] instead.
+ *)
+ val once : (t -> node -> unit) -> unit
+
+ (** Pushes the callback {i once} for all created nodes.
+ You must call [pop_call] at some point to flush them.
+ Any previsously registred callback by [once] or [push] is replaced
+ by the new one. *)
+ val push : dot -> (t -> node -> unit) -> unit
+
+ (** Set node prefix.
+ Otherwize, some default one is created for each functor application. *)
+ val prefix : string -> unit
+end
+
+(** Register a continuation to be executed later. *)
+val push : dot -> (unit -> unit) -> unit
+
+(** Flushes all pending continuations. *)
+val pop_all : dot -> unit
+
+(** {1 Decorator} *)
+
+(** A text buffer to compose labels and attributes.
+ You can add text and attributes to the buffer, and finally
+ flush it by calling [attributes].
+ A single [`Label] attribute is finally emitted with
+ all the added text (if non-empty). *)
+type buffer
+
+(** Create a buffer initialized with the given attributes. *)
+val buffer : attr list -> buffer
+
+(** Add text material to buffer label. *)
+val bprintf : buffer -> ('a,Format.formatter,unit,unit) format4 -> 'a
+
+val add_char : buffer -> char -> unit
+val add_label : buffer -> string -> unit
+
+(** Add attributes to the buffer. *)
+val add_attr : buffer -> attr list -> unit
+
+(** Only add attributes with a [true] boolean flag *)
+val add_options : buffer -> (bool * attr list) list -> unit
+
+(** Flushes the buffer into a list of attributes *)
+val attributes : buffer -> attr list
+
+(** Concat the attributes with flagged ones *)
+val decorate : attr list -> ( bool * attr list ) list -> attr list
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 0e774657a818b0b5f91cafba14f4b21197480427..eb86c85f6945e397d7e3b1af0e3959c71faa5500 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -224,6 +224,7 @@ module Normalized = struct
let pretty fmt p = Format.fprintf fmt "%s" (pretty p)
let pp_abs fmt p = Format.fprintf fmt "%s" p
let unknown = normalize ""
+ let is_unknown fp = equal fp unknown
end
type position =
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 6ea46d821541a1de524e1baad38bbadcf6339b54..74eef31bbdbb8d6f2ff340258beffeef3539cd65 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -120,6 +120,9 @@ module Normalized: sig
(** Unknown filepath, used as 'dummy' for [Datatype.Filepath]. *)
val unknown: t
+
+ (** @since Frama-C+dev *)
+ val is_unknown: t -> bool
end
(** Describes a position in a source file.
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index bb11d8d56877746f7cea5b12005396ff6ddbeaad..287a5d8e0b01a50e36a5dd37f0f4ea3ba4d3209f 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1863,7 +1863,9 @@ let toplevel play =
Task.on_idle :=
(fun f -> ignore (Glib.Timeout.add ~ms:50 ~callback:f));
let project_name = Gui_parameters.Project_name.get () in
- if project_name <> "" then
+ if project_name = "" then
+ Project.set_current_as_last_created ()
+ else
Project.set_current (Project.from_unique_name project_name);
Ast.compute ()
with e -> (* An error occurred: we need to enforce the splash screen
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 5515e44a3b884a7281f00342677c689c8333baa1..d5438b227de994181748fcdadfd7c43f3a49b05b 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -138,6 +138,7 @@ let reduce_to_valid_location out loc =
begin
if is_assigns out && not (Locations.is_bottom_loc loc) then
Value_parameters.warning ~current:true ~once:true
+ ~wkey:Value_parameters.wkey_invalid_assigns
"@[Completely invalid destination@ for %a.@ \
Ignoring.@]" pp_assign_free_alloc out;
None
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index e5c0bb41a9370ff6c99362bf8a1a5ca7992ea761..ce9a20a55a312fa437321e4c9a52affec6a9aa2e 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -1919,20 +1919,27 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
(* See comments in the code for the evaluation of Pinitialized *)
let star_tsets = deref_tsets tsets in
let rlocb = eval_tlval ~alarm_mode env star_tsets in
- let size = Eval_typ.sizeof_lval_typ rlocb.etype in
- let state = env_state env lbl_initialized in
- let fred = match p_content with
- | Pinitialized _ -> V_Or_Uninitialized.reduce_by_initializedness
- | Pdangling _ -> V_Or_Uninitialized.reduce_by_danglingness
- | _ -> assert false
- in
- let fred = Eval_op.reduce_by_initialized_defined (fred positive) in
- let state_reduced =
- let loc = make_loc rlocb.eunder size in
- let loc = Eval_op.make_loc_contiguous loc in
- Eval_op.apply_on_all_locs fred loc state
- in
- overwrite_state env state_reduced lbl_initialized
+ (* No reduction on negations of \initialized or \dangling on multiple
+ locations: at least one of them is non initialized/dangling, but
+ which one? Reduction would only be possible in the rare case where
+ only one of the locations might be non initialized/dangling. *)
+ if not (positive || Location_Bits.cardinal_zero_or_one rlocb.eover)
+ then env
+ else
+ let size = Eval_typ.sizeof_lval_typ rlocb.etype in
+ let state = env_state env lbl_initialized in
+ let fred = match p_content with
+ | Pinitialized _ -> V_Or_Uninitialized.reduce_by_initializedness
+ | Pdangling _ -> V_Or_Uninitialized.reduce_by_danglingness
+ | _ -> assert false
+ in
+ let fred = Eval_op.reduce_by_initialized_defined (fred positive) in
+ let state_reduced =
+ let loc = make_loc rlocb.eunder size in
+ let loc = Eval_op.make_loc_contiguous loc in
+ Eval_op.apply_on_all_locs fred loc state
+ in
+ overwrite_state env state_reduced lbl_initialized
with LogicEvalError _ -> env
end
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 5471f4b343ffdf7d312a50bdf3420e27ebf77731..5eb874d2566e44e9e243f6d50027377060d47373 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -98,6 +98,8 @@ let () = set_warn_status wkey_missing_loop_unroll Log.Winactive
let wkey_missing_loop_unroll_for = register_warn_category "missing-loop-unroll:for"
let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive
let wkey_signed_overflow = register_warn_category "signed-overflow"
+let wkey_invalid_assigns = register_warn_category "invalid-assigns"
+let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
module ForceValues =
WithOutput
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index fe24f33b22e81e956807ffba17fae01f421217a2..a5f62e9cff6d10c4d4ebaef1a4dae9da8b8294f2 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -204,6 +204,9 @@ val wkey_missing_loop_unroll_for : warn_category
(** Warning category for signed overflows *)
val wkey_signed_overflow : warn_category
+(** Warning category for 'completely invalid' assigns clause *)
+val wkey_invalid_assigns : warn_category
+
(** Debug category used to print information about invalid pointer comparisons*)
val dkey_pointer_comparison: category
diff --git a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
index 834a0dde5f6db9f527a604df92cba0f2fa2a7226..195847c4a798c48e04d7613f0a9ff77e106c4001 100644
--- a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
@@ -13,6 +13,9 @@
[eva] Initial state computed
[eva] using specification for function __va_ioctl_void
[eva] using specification for function __va_ioctl_ptr
+[eva:invalid-assigns] tests/known/ioctl.c:17:
+ Completely invalid destination for assigns clause *((char *)argp + (0 ..)).
+ Ignoring.
[eva] using specification for function __va_ioctl_int
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 877191a8d974c87bdc90c050a25ebcf2e32609da..1c7b3d303cc981c5a84a939d39327c9ae7f12276 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -984,7 +984,7 @@ let base_output () =
| dir ->
make_output_dir dir ; dir in
base_output := Some output;
- Filepath.add_symbolic_dir "WPOUT" output ;
+ Fc_Filepath.add_symbolic_dir "WPOUT" output ;
output
| Some output -> output
@@ -1026,7 +1026,7 @@ let has_print_generated () = has_dkey cat_print_generated
let print_generated ?header file =
let header = match header with
- | None -> Filepath.Normalized.to_pretty_string (Datatype.Filepath.of_string file)
+ | None -> Fc_Filepath.Normalized.to_pretty_string (Datatype.Filepath.of_string file)
| Some head -> head in
debug ~dkey:cat_print_generated "%S@\n%t@." header
begin fun fmt ->
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index e27e83c8af3557509f71e9dee55793438f58b39d..35235461d13ed2ecd8659d12fcde6992bb47ce76 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -39,7 +39,7 @@
[eva] computing for function f <- invalid_assigns_imprecise <- main.
Called from tests/builtins/imprecise.c:11.
[eva] using specification for function f
-[eva] tests/builtins/imprecise.c:11: Warning:
+[eva:invalid-assigns] tests/builtins/imprecise.c:11:
Completely invalid destination for assigns clause *p. Ignoring.
[eva] Done for function f
[eva] Recording results for invalid_assigns_imprecise
diff --git a/tests/builtins/oracle/memchr.res.oracle b/tests/builtins/oracle/memchr.res.oracle
index 94cae8ab088a9ed33b7c3ab50eb097a755f62178..d77c490f0c7d086f6a2150c57f9c6585a7e3c1f2 100644
--- a/tests/builtins/oracle/memchr.res.oracle
+++ b/tests/builtins/oracle/memchr.res.oracle
@@ -100,8 +100,8 @@
[eva] tests/builtins/memchr.c:122: Call to builtin memchr
[eva:alarm] tests/builtins/memchr.c:122: Warning:
function memchr: precondition 'valid' got status unknown.
-[eva] tests/builtins/memchr.c:122:
- function memchr: precondition 'initialization' got status valid.
+[eva:alarm] tests/builtins/memchr.c:122: Warning:
+ function memchr: precondition 'initialization' got status unknown.
[eva:alarm] tests/builtins/memchr.c:122: Warning:
function memchr: precondition 'danglingness' got status unknown.
[eva] tests/builtins/memchr.c:128: Call to builtin memchr
@@ -134,8 +134,8 @@
[eva] tests/builtins/memchr.c:145: Call to builtin memchr
[eva] tests/builtins/memchr.c:145:
function memchr: precondition 'valid' got status valid.
-[eva] tests/builtins/memchr.c:145:
- function memchr: precondition 'initialization' got status valid.
+[eva:alarm] tests/builtins/memchr.c:145: Warning:
+ function memchr: precondition 'initialization' got status unknown.
[eva] tests/builtins/memchr.c:145:
function memchr: precondition 'danglingness' got status valid.
[eva] tests/builtins/memchr.c:145: Frama_C_show_each_mymemchr: {1}
@@ -143,8 +143,8 @@
[eva] tests/builtins/memchr.c:152: Call to builtin memchr
[eva] tests/builtins/memchr.c:152:
function memchr: precondition 'valid' got status valid.
-[eva] tests/builtins/memchr.c:152:
- function memchr: precondition 'initialization' got status valid.
+[eva:alarm] tests/builtins/memchr.c:152: Warning:
+ function memchr: precondition 'initialization' got status unknown.
[eva] tests/builtins/memchr.c:152:
function memchr: precondition 'danglingness' got status valid.
[eva] tests/builtins/memchr.c:152: Frama_C_show_each_mymemchr: {3}
@@ -443,8 +443,8 @@
[eva] tests/builtins/memchr.c:348: Call to builtin memchr
[eva] tests/builtins/memchr.c:348:
function memchr: precondition 'valid' got status valid.
-[eva] tests/builtins/memchr.c:348:
- function memchr: precondition 'initialization' got status valid.
+[eva:alarm] tests/builtins/memchr.c:348: Warning:
+ function memchr: precondition 'initialization' got status unknown.
[eva] tests/builtins/memchr.c:348:
function memchr: precondition 'danglingness' got status valid.
[eva] tests/builtins/memchr.c:348: Frama_C_show_each_mymemchr: {1}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 107f92c67f3f62604ce53ca25bf5a5672e0c65be..417ea214e24ff7f7103182badf324309869ad81f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3145,10 +3145,9 @@ struct sigaction *__fc_p_sigaction = __fc_sigaction;
\old(oldact) ≡ \null ∨
*\old(oldact) ∈ *(__fc_p_sigaction + \old(signum));
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns oldact ≡ \null? \empty: *oldact,
- act ≡ \null? \empty: *(__fc_p_sigaction + signum), \result;
- assigns oldact ≡ \null? \empty: *oldact \from __fc_p_sigaction;
- assigns act ≡ \null? \empty: *(__fc_p_sigaction + signum) \from *act;
+ assigns *oldact, *(__fc_p_sigaction + signum), \result;
+ assigns *oldact \from __fc_p_sigaction;
+ assigns *(__fc_p_sigaction + signum) \from *act;
assigns \result
\from (indirect: signum), (indirect: act), (indirect: *act),
(indirect: oldact), (indirect: *oldact);
@@ -3166,11 +3165,10 @@ extern int sigaction(int signum, struct sigaction const * __restrict act,
initialization: oldset_initialized:
\old(oldset) ≢ \null ∧ \result ≡ 0 ⇒
\initialized(\old(oldset));
- assigns \result, oldset ≡ \null? \empty: *oldset;
+ assigns \result, *oldset;
assigns \result
\from (indirect: how), (indirect: set), (indirect: oldset);
- assigns oldset ≡ \null? \empty: *oldset
- \from (indirect: how), (indirect: oldset);
+ assigns *oldset \from (indirect: how), (indirect: oldset);
*/
extern int sigprocmask(int how, sigset_t const * __restrict set,
sigset_t * __restrict oldset);
@@ -5840,11 +5838,11 @@ axiomatic nanosleep_predicates {
ensures
remaining_valid:
\old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000;
- assigns \result, rmtp ≡ \null? \empty: *rmtp;
+ assigns \result, *rmtp;
assigns \result
\from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp),
(indirect: *rqtp);
- assigns rmtp ≡ \null? \empty: *rmtp
+ assigns *rmtp
\from __fc_time, (indirect: clock_id), (indirect: rqtp),
(indirect: *rqtp), (indirect: rmtp);
@@ -5901,10 +5899,10 @@ extern int clock_nanosleep(clockid_t clock_id, int flags,
interrupted_remaining_valid:
\old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒
0 ≤ \old(rmtp)->tv_nsec < 1000000000;
- assigns \result, rmtp ≡ \null? \empty: *rmtp;
+ assigns \result, *rmtp;
assigns \result
\from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp);
- assigns rmtp ≡ \null? \empty: *rmtp
+ assigns *rmtp
\from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp),
(indirect: rmtp);
*/
@@ -6753,8 +6751,8 @@ extern int getitimer(int which, struct itimerval *curr_value);
requires
old_value_null_or_valid: old_value ≡ \null ∨ \valid(old_value);
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns old_value ≢ \null? *old_value: \empty, \result;
- assigns old_value ≢ \null? *old_value: \empty
+ assigns *old_value, \result;
+ assigns *old_value
\from (indirect: which), (indirect: old_value), (indirect: new_value),
__fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof;
assigns \result
@@ -6767,10 +6765,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
0 ≤ new_value->it_interval.tv_usec ≤ 999999;
ensures result_ok: \result ≡ 0;
ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, old_value ≢ \null? *old_value: \empty,
- __fc_itimer_real;
+ assigns \result, *old_value, __fc_itimer_real;
assigns \result \from \nothing;
- assigns old_value ≢ \null? *old_value: \empty \from __fc_itimer_real;
+ assigns *old_value \from __fc_itimer_real;
assigns __fc_itimer_real \from *new_value;
behavior virtual:
@@ -6780,10 +6777,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
0 ≤ new_value->it_interval.tv_usec ≤ 999999;
ensures result_ok: \result ≡ 0;
ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, old_value ≢ \null? *old_value: \empty;
+ assigns \result, *old_value;
assigns \result \from \nothing;
- assigns old_value ≢ \null? *old_value: \empty
- \from __fc_itimer_virtual;
+ assigns *old_value \from __fc_itimer_virtual;
behavior prof:
assumes
@@ -6792,9 +6788,9 @@ extern int getitimer(int which, struct itimerval *curr_value);
0 ≤ new_value->it_interval.tv_usec ≤ 999999;
ensures result_ok: \result ≡ 0;
ensures initialization: old_value: \initialized(\old(old_value));
- assigns \result, old_value ≢ \null? *old_value: \empty;
+ assigns \result, *old_value;
assigns \result \from \nothing;
- assigns old_value ≢ \null? *old_value: \empty \from __fc_itimer_prof;
+ assigns *old_value \from __fc_itimer_prof;
behavior invalid:
assumes
@@ -6818,27 +6814,25 @@ extern int setitimer(int which,
requires writefds: writefds ≡ \null ∨ \valid(writefds);
requires errorfds: errorfds ≡ \null ∨ \valid(errorfds);
requires timeout: timeout ≡ \null ∨ \valid(timeout);
- assigns __fc_fds_state, readfds ≡ \null? \empty: *readfds,
- writefds ≡ \null? \empty: *writefds,
- errorfds ≡ \null? \empty: *errorfds,
- timeout ≡ \null? \empty: *timeout, \result;
+ assigns __fc_fds_state, *readfds, *writefds, *errorfds, *timeout,
+ \result;
assigns __fc_fds_state \from __fc_fds_state;
- assigns readfds ≡ \null? \empty: *readfds
+ assigns *readfds
\from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
(indirect: writefds), (indirect: *writefds),
(indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
(indirect: *timeout), __fc_fds_state;
- assigns writefds ≡ \null? \empty: *writefds
+ assigns *writefds
\from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
(indirect: writefds), (indirect: *writefds),
(indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
(indirect: *timeout), __fc_fds_state;
- assigns errorfds ≡ \null? \empty: *errorfds
+ assigns *errorfds
\from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
(indirect: writefds), (indirect: *writefds),
(indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
(indirect: *timeout), __fc_fds_state;
- assigns timeout ≡ \null? \empty: *timeout
+ assigns *timeout
\from (indirect: nfds), (indirect: readfds), (indirect: *readfds),
(indirect: writefds), (indirect: *writefds),
(indirect: errorfds), (indirect: *errorfds), (indirect: timeout),
@@ -7129,11 +7123,11 @@ extern int __va_ioctl_void(int fd, int request);
*/
extern int __va_ioctl_int(int fd, int request, int arg);
-/*@ assigns \result, argp ≢ \null? *((char *)argp + (0 ..)): \empty;
+/*@ assigns \result, *((char *)argp + (0 ..));
assigns \result
\from (indirect: fd), (indirect: request),
(indirect: *((char *)argp + (0 ..)));
- assigns argp ≢ \null? *((char *)argp + (0 ..)): \empty
+ assigns *((char *)argp + (0 ..))
\from (indirect: fd), (indirect: request), *((char *)argp + (0 ..));
*/
extern int __va_ioctl_ptr(int fd, int request, void *argp);
diff --git a/tests/libc/oracle/libgen_h.res.oracle b/tests/libc/oracle/libgen_h.res.oracle
index ca158666adf08acb2890a53b2ae8fecfddb3e132..a5ac900a0e19e23678ca830eeef10d3ef012d55b 100644
--- a/tests/libc/oracle/libgen_h.res.oracle
+++ b/tests/libc/oracle/libgen_h.res.oracle
@@ -15,7 +15,7 @@
Called from tests/libc/libgen_h.c:11.
[eva] tests/libc/libgen_h.c:11:
function basename: precondition 'null_or_valid_string_path' got status valid.
-[eva] tests/libc/libgen_h.c:11: Warning:
+[eva:invalid-assigns] tests/libc/libgen_h.c:11:
Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
[eva] Done for function basename
[eva:alarm] tests/libc/libgen_h.c:12: Warning: assertion got status unknown.
@@ -30,7 +30,7 @@
Called from tests/libc/libgen_h.c:16.
[eva] tests/libc/libgen_h.c:16:
function dirname: precondition 'null_or_valid_string_path' got status valid.
-[eva] tests/libc/libgen_h.c:16: Warning:
+[eva:invalid-assigns] tests/libc/libgen_h.c:16:
Completely invalid destination for assigns clause *(path + (0 ..)). Ignoring.
[eva] Done for function dirname
[eva:alarm] tests/libc/libgen_h.c:17: Warning: assertion got status unknown.
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 42c80f2642d6fdde9b66d2ab9487b73f4ff7b8a8..9d071e5884c3e373da23a02893036f0d8bbbaee3 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -83,6 +83,8 @@
function sigprocmask: precondition 'valid_oldset_or_null' got status valid.
[eva] tests/libc/signal_h.c:35:
function sigprocmask: precondition 'separation' got status valid.
+[eva:invalid-assigns] tests/libc/signal_h.c:35:
+ Completely invalid destination for assigns clause *oldset. Ignoring.
[eva] Done for function sigprocmask
[eva] computing for function sigprocmask <- main.
Called from tests/libc/signal_h.c:38.
@@ -137,6 +139,8 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] tests/libc/signal_h.c:51:
function sigaction: precondition 'separation,separated_acts' got status valid.
+[eva:invalid-assigns] tests/libc/signal_h.c:51:
+ Completely invalid destination for assigns clause *oldact. Ignoring.
[eva] Done for function sigaction
[eva] Recording results for main
[eva] done for function main
@@ -176,9 +180,7 @@
[15]{.sa_handler; .sa_sigaction} ∈ {0}
[15]{.sa_mask; .sa_flags} ∈ [--..--]
[16]{.sa_handler; .sa_sigaction} ∈ {0}
- [16]{.sa_mask; .sa_flags} ∈ [--..--]
- [17]{.sa_handler; .sa_sigaction} ∈ {0}
- [17]{.sa_mask; .sa_flags} ∈ [--..--]
+ {[16]{.sa_mask; .sa_flags}; [17]} ∈ [--..--]
[18] ∈
{{ garbled mix of &{__fc_sigaction}
(origin: Library function) }}
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 75780c1ba4a10561b67f6deb39440fddbcfbf8cb..55c5afe6dad117fc0beb325fa0f45052db727460 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -134,7 +134,7 @@
function strtok: precondition 'valid_string_delim' got status valid.
[eva] tests/libc/string_h.c:72:
function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid.
-[eva] tests/libc/string_h.c:72: Warning:
+[eva:invalid-assigns] tests/libc/string_h.c:72:
Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
[eva] Done for function strtok
[eva:alarm] tests/libc/string_h.c:73: Warning: assertion got status unknown.
@@ -144,7 +144,7 @@
function strtok: precondition 'valid_string_delim' got status valid.
[eva:alarm] tests/libc/string_h.c:75: Warning:
function strtok, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva] tests/libc/string_h.c:75: Warning:
+[eva:invalid-assigns] tests/libc/string_h.c:75:
Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
[eva] Done for function strtok
[eva:alarm] tests/libc/string_h.c:76: Warning:
@@ -221,7 +221,7 @@
function strtok_r: precondition 'valid_saveptr' got status valid.
[eva] tests/libc/string_h.c:102:
function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status valid.
-[eva] tests/libc/string_h.c:102: Warning:
+[eva:invalid-assigns] tests/libc/string_h.c:102:
Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
[eva] Done for function strtok_r
[eva:alarm] tests/libc/string_h.c:103: Warning: assertion got status unknown.
@@ -233,7 +233,7 @@
function strtok_r: precondition 'valid_saveptr' got status valid.
[eva:alarm] tests/libc/string_h.c:105: Warning:
function strtok_r, behavior new_str: precondition 'valid_string_s_or_delim_not_found' got status unknown.
-[eva] tests/libc/string_h.c:105: Warning:
+[eva:invalid-assigns] tests/libc/string_h.c:105:
Completely invalid destination for assigns clause *(s + (0 ..)). Ignoring.
[eva] Done for function strtok_r
[eva:alarm] tests/libc/string_h.c:106: Warning:
diff --git a/tests/libc/oracle/sys_select.res.oracle b/tests/libc/oracle/sys_select.res.oracle
index 41fa7f4bc4969060e4bf3300451702b172018a50..453a3465161df7694e3616278d3db5120e82a673 100644
--- a/tests/libc/oracle/sys_select.res.oracle
+++ b/tests/libc/oracle/sys_select.res.oracle
@@ -72,6 +72,10 @@
function select: precondition 'errorfds' got status valid.
[eva] tests/libc/sys_select.c:31:
function select: precondition 'timeout' got status valid.
+[eva:invalid-assigns] tests/libc/sys_select.c:31:
+ Completely invalid destination for assigns clause *writefds. Ignoring.
+[eva:invalid-assigns] tests/libc/sys_select.c:31:
+ Completely invalid destination for assigns clause *errorfds. Ignoring.
[eva] Done for function select
[eva] computing for function FD_ISSET <- main.
Called from tests/libc/sys_select.c:32.
diff --git a/tests/libc/oracle/sys_time.res.oracle b/tests/libc/oracle/sys_time.res.oracle
index 3c7c79cab30db005eb3c7f1d6087a189d033aa56..18c18fa9f8cf4ac0e2cd2252f3a3baf3d7dcd62c 100644
--- a/tests/libc/oracle/sys_time.res.oracle
+++ b/tests/libc/oracle/sys_time.res.oracle
@@ -11,6 +11,8 @@
function setitimer: precondition 'valid_new_value' got status valid.
[eva] tests/libc/sys_time.c:6:
function setitimer: precondition 'old_value_null_or_valid' got status valid.
+[eva:invalid-assigns] tests/libc/sys_time.c:6:
+ Completely invalid destination for assigns clause *old_value. Ignoring.
[eva] Done for function setitimer
[eva] tests/libc/sys_time.c:7: assertion got status valid.
[eva] computing for function setitimer <- main.
diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle
index 5fcd6c6d027bc01e634adfc623934e6e724e7607..7e8f729d1beae0a1300355d51b3f1c84f7826b6c 100644
--- a/tests/libc/oracle/time_h.res.oracle
+++ b/tests/libc/oracle/time_h.res.oracle
@@ -37,9 +37,13 @@
function nanosleep: precondition 'valid_nanosecs' got status valid.
[eva] tests/libc/time_h.c:22:
function nanosleep: precondition 'valid_remaining_or_null' got status valid.
+[eva:invalid-assigns] tests/libc/time_h.c:22:
+ Completely invalid destination for assigns clause *rmtp. Ignoring.
[eva] Done for function nanosleep
[eva] computing for function nanosleep <- main.
Called from tests/libc/time_h.c:22.
+[eva:invalid-assigns] tests/libc/time_h.c:22:
+ Completely invalid destination for assigns clause *rmtp. Ignoring.
[eva] Done for function nanosleep
[eva] computing for function clock_nanosleep <- main.
Called from tests/libc/time_h.c:28.
diff --git a/tests/syntax/flexible_array_member.i b/tests/syntax/flexible_array_member.i
index fbbd55dd676762831d5780ec467bd41a29c8c356..9fda08120828a0b2c8bde3058a345a862bb81ed3 100644
--- a/tests/syntax/flexible_array_member.i
+++ b/tests/syntax/flexible_array_member.i
@@ -1,9 +1,16 @@
// valid flexible array member declarations
-struct {
+struct s1 {
int size;
char data[];
-} s1;
+} ss1;
-struct {
+struct s2 {
char len, data[];
-} s2;
+} ss2;
+
+union u {
+ struct s {
+ char len;
+ char data[];
+ } fam;
+} u1;
diff --git a/tests/syntax/flexible_array_member_invalid1.i b/tests/syntax/flexible_array_member_invalid1.i
index bd4b3f7fc0beb135e67fc780b6b9bae433b41ce2..62ebdab3e24b225226ed31ca6ca17e0cdd50b33f 100644
--- a/tests/syntax/flexible_array_member_invalid1.i
+++ b/tests/syntax/flexible_array_member_invalid1.i
@@ -1,4 +1,4 @@
// invalid flexible array member (empty struct otherwise)
-struct {
+struct s1 {
char data[];
-} s1;
+} ss1;
diff --git a/tests/syntax/flexible_array_member_invalid2.i b/tests/syntax/flexible_array_member_invalid2.i
index e5a1463ec5432beb168dfc1b405f6213d1ca08a8..eab5dccd0c3e11ce97ad2511ab92beaeb96bc405 100644
--- a/tests/syntax/flexible_array_member_invalid2.i
+++ b/tests/syntax/flexible_array_member_invalid2.i
@@ -1,6 +1,6 @@
// invalid flexible array member (two incomplete fields)
-struct {
+struct s {
int len;
char data[];
char more_data[];
-} s;
+} ss;
diff --git a/tests/syntax/flexible_array_member_invalid3.i b/tests/syntax/flexible_array_member_invalid3.i
index 30f2a733c7ee7377ae332c86bba63b0622184dd0..4baf088c14f4a8baeba250ad8f2abe33a2b79766 100644
--- a/tests/syntax/flexible_array_member_invalid3.i
+++ b/tests/syntax/flexible_array_member_invalid3.i
@@ -1,5 +1,5 @@
// invalid flexible array member (two incomplete fields in same field group)
-struct {
+struct s {
int len;
char data[], more_data[];
-} s;
+} ss;
diff --git a/tests/syntax/flexible_array_member_invalid4.i b/tests/syntax/flexible_array_member_invalid4.i
index bd7666227597316d55ba00b5b54ce9fa0b792ddd..e84cce94b9891a77d85135a75691d9f9b7ad1b87 100644
--- a/tests/syntax/flexible_array_member_invalid4.i
+++ b/tests/syntax/flexible_array_member_invalid4.i
@@ -1,6 +1,6 @@
// invalid flexible array member (incomplete field is not last)
-struct {
+struct s {
int len;
char data[];
char b;
-} s;
+} ss;
diff --git a/tests/syntax/flexible_array_member_invalid5.i b/tests/syntax/flexible_array_member_invalid5.i
index dd3eac2f1c52361a2dbadf2303ba550baf481886..a0339194afe9def80ec7aeba80647ec0e8084981 100644
--- a/tests/syntax/flexible_array_member_invalid5.i
+++ b/tests/syntax/flexible_array_member_invalid5.i
@@ -4,7 +4,7 @@ typedef struct {
char data[];
} fam;
-struct {
+struct st {
int len;
fam f;
-} st;
+} sst;
diff --git a/tests/syntax/oracle/flexible_array_member.res.oracle b/tests/syntax/oracle/flexible_array_member.res.oracle
index a7317194e390ea0960fa4a3cbb72e062ae312798..90af690c44153978d928abf3544bb5802d620eea 100644
--- a/tests/syntax/oracle/flexible_array_member.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member.res.oracle
@@ -1,13 +1,21 @@
[kernel] Parsing tests/syntax/flexible_array_member.i (no preprocessing)
/* Generated by Frama-C */
-struct __anonstruct_s1_1 {
+struct s1 {
int size ;
char data[] ;
};
-struct __anonstruct_s2_2 {
+struct s2 {
char len ;
char data[] ;
};
-struct __anonstruct_s1_1 s1;
-struct __anonstruct_s2_2 s2;
+struct s {
+ char len ;
+ char data[] ;
+};
+union u {
+ struct s fam ;
+};
+struct s1 ss1;
+struct s2 ss2;
+union u u1;
diff --git a/tests/value/initialized.c b/tests/value/initialized.c
index 2292df35211489154198dc5402681dd5ebd0f99e..3e04b3cc71674441815e291dae3d6f580cf4586b 100644
--- a/tests/value/initialized.c
+++ b/tests/value/initialized.c
@@ -154,6 +154,41 @@ void g7() {
//@ assert !\initialized(&key[0..127]);
}
+/* Tests the reduction by the negation of the \initialized predicate. */
+void reduce_by_negation () {
+ int x, y;
+ int *p = rand ? &x : &y;
+ if (rand) x = 0;
+ if (rand) y = 0;
+ if (rand) {
+ //@ assert !\initialized(&x);
+ //@ check invalid: \initialized(&x);
+ }
+ if (rand) {
+ //@ assert !\initialized(p);
+ //@ check unknown: \initialized(&x) && \initialized(&y);
+ }
+ if (rand) {
+ //@ assert !\initialized({&x, &y});
+ //@ check unknown: \initialized(&x) && \initialized(&y);
+ }
+ if (rand) {
+ y = 0;
+ //@ assert !\initialized(p);
+ //@ check unknown: \initialized(&x);
+ }
+ if (rand) {
+ y = 0;
+ //@ assert !\initialized({&x, &y});
+ //@ check invalid: \initialized(&x);
+ }
+ char t[10];
+ for (int i = 0; i < 10; i++)
+ t[i] = i;
+ //@ assert !\initialized(&t[0..9]);
+ //@ check unknown: \initialized(&t[0..9]);
+}
+
int main () {
g1();
g2();
@@ -162,5 +197,6 @@ int main () {
g5();
g6();
g7();
+ reduce_by_negation();
return 0;
}
diff --git a/tests/value/oracle/initialized.res.oracle b/tests/value/oracle/initialized.res.oracle
index 79cf5c4a3129d812402778bbe4f0ab7ba79dc9d2..f3d1c20aa17d60f4f052fe7a489807dd3537ff5f 100644
--- a/tests/value/oracle/initialized.res.oracle
+++ b/tests/value/oracle/initialized.res.oracle
@@ -13,7 +13,7 @@
v1 ∈ {0}
i6 ∈ [--..--]
[eva] computing for function g1 <- main.
- Called from tests/value/initialized.c:158.
+ Called from tests/value/initialized.c:193.
[eva] tests/value/initialized.c:19: starting to merge loop iterations
[eva:alarm] tests/value/initialized.c:21: Warning: assertion got status unknown.
[eva:alarm] tests/value/initialized.c:22: Warning: assertion got status unknown.
@@ -65,7 +65,7 @@
[eva] Recording results for g1
[eva] Done for function g1
[eva] computing for function g2 <- main.
- Called from tests/value/initialized.c:159.
+ Called from tests/value/initialized.c:194.
[eva:alarm] tests/value/initialized.c:50: Warning:
signed overflow. assert -2147483648 ≤ (int)(&b4) + (int)(&b4);
[eva:alarm] tests/value/initialized.c:50: Warning:
@@ -149,7 +149,7 @@
[eva] Recording results for g2
[eva] Done for function g2
[eva] computing for function g3 <- main.
- Called from tests/value/initialized.c:160.
+ Called from tests/value/initialized.c:195.
[eva:alarm] tests/value/initialized.c:89: Warning: assertion got status unknown.
[eva:alarm] tests/value/initialized.c:93: Warning:
accessing uninitialized left-value. assert \initialized(&r2);
@@ -171,13 +171,13 @@
[eva] Recording results for g3
[eva] Done for function g3
[eva] computing for function g4 <- main.
- Called from tests/value/initialized.c:161.
+ Called from tests/value/initialized.c:196.
[eva:alarm] tests/value/initialized.c:104: Warning:
accessing uninitialized left-value. assert \initialized(&y);
[eva] Recording results for g4
[eva] Done for function g4
[eva] computing for function g5 <- main.
- Called from tests/value/initialized.c:162.
+ Called from tests/value/initialized.c:197.
[eva] computing for function wrong_assigns <- g5 <- main.
Called from tests/value/initialized.c:127.
[eva] using specification for function wrong_assigns
@@ -193,7 +193,7 @@
[eva] Recording results for g5
[eva] Done for function g5
[eva] computing for function g6 <- main.
- Called from tests/value/initialized.c:163.
+ Called from tests/value/initialized.c:198.
[eva:alarm] tests/value/initialized.c:143: Warning:
assertion got status unknown.
[eva:alarm] tests/value/initialized.c:144: Warning:
@@ -207,7 +207,7 @@
[eva] Recording results for g6
[eva] Done for function g6
[eva] computing for function g7 <- main.
- Called from tests/value/initialized.c:164.
+ Called from tests/value/initialized.c:199.
[eva] computing for function Frama_C_make_unknown <- g7 <- main.
Called from tests/value/initialized.c:153.
[eva] using specification for function Frama_C_make_unknown
@@ -217,6 +217,35 @@
[eva] tests/value/initialized.c:154: assertion got status valid.
[eva] Recording results for g7
[eva] Done for function g7
+[eva] computing for function reduce_by_negation <- main.
+ Called from tests/value/initialized.c:200.
+[eva:alarm] tests/value/initialized.c:164: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/value/initialized.c:165: Warning:
+ check 'invalid' got status invalid.
+[eva:alarm] tests/value/initialized.c:168: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/value/initialized.c:169: Warning:
+ check 'unknown' got status unknown.
+[eva:alarm] tests/value/initialized.c:172: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/value/initialized.c:173: Warning:
+ check 'unknown' got status unknown.
+[eva:alarm] tests/value/initialized.c:177: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/value/initialized.c:178: Warning:
+ check 'unknown' got status unknown.
+[eva:alarm] tests/value/initialized.c:182: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/value/initialized.c:183: Warning:
+ check 'invalid' got status unknown.
+[eva] tests/value/initialized.c:186: starting to merge loop iterations
+[eva:alarm] tests/value/initialized.c:188: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/value/initialized.c:189: Warning:
+ check 'unknown' got status unknown.
+[eva] Recording results for reduce_by_negation
+[eva] Done for function reduce_by_negation
[eva] Recording results for main
[eva] done for function main
[eva] tests/value/initialized.c:93:
@@ -293,6 +322,11 @@
Frama_C_entropy_source ∈ [--..--]
key[0..63] ∈ [--..--]
[64..127] ∈ UNINITIALIZED
+[eva:final-states] Values at end of function reduce_by_negation:
+ x ∈ {0} or UNINITIALIZED
+ y ∈ {0} or UNINITIALIZED
+ p ∈ {{ &x ; &y }}
+ t[0..9] ∈ [0..9] or UNINITIALIZED
[eva:final-states] Values at end of function g5:
v ∈ UNINITIALIZED
p ∈ {{ &v1 ; &v2 }}
@@ -319,6 +353,8 @@
[from] Computing for function Frama_C_make_unknown <-g7
[from] Done for function Frama_C_make_unknown
[from] Done for function g7
+[from] Computing for function reduce_by_negation
+[from] Done for function reduce_by_negation
[from] Computing for function g5
[from] Computing for function wrong_assigns <-g5
[from] Done for function wrong_assigns
@@ -348,6 +384,8 @@
i6 FROM rand (and SELF)
[from] Function g7:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function reduce_by_negation:
+ NO EFFECTS
[from] Function wrong_assigns:
v{.a; .b} FROM \nothing
[from] Function g5:
@@ -386,6 +424,10 @@
Frama_C_entropy_source; key[0..63]
[inout] Inputs for function g7:
Frama_C_entropy_source
+[inout] Out (internal) for function reduce_by_negation:
+ x; y; p; tmp; t[0..9]; i
+[inout] Inputs for function reduce_by_negation:
+ rand
[inout] Out (internal) for function g5:
v{.a; .b}; p; tmp
[inout] Inputs for function g5:
diff --git a/tests/value/oracle/leaf_spec.0.res.oracle b/tests/value/oracle/leaf_spec.0.res.oracle
index 761d38bcf9e226c2597073376f838576ca755dd9..4dda7f7cf8b0609d64b17c78ec40d983449de12b 100644
--- a/tests/value/oracle/leaf_spec.0.res.oracle
+++ b/tests/value/oracle/leaf_spec.0.res.oracle
@@ -27,7 +27,7 @@
[kernel:annot:missing-spec] tests/value/leaf_spec.i:22: Warning:
Neither code nor specification for function k, generating default assigns from the prototype
[eva] using specification for function k
-[eva] tests/value/leaf_spec.i:22: Warning:
+[eva:invalid-assigns] tests/value/leaf_spec.i:22:
Completely invalid destination for assigns clause *l. Ignoring.
[eva] Done for function k
[eva] computing for function k0 <- main.
diff --git a/tests/value/oracle/leaf_spec.1.res.oracle b/tests/value/oracle/leaf_spec.1.res.oracle
index 666a0ee653ea406fd618ea0f479ba41d7741adf0..aa1978e94dfdb9044fb6881d77a2a219b2701da0 100644
--- a/tests/value/oracle/leaf_spec.1.res.oracle
+++ b/tests/value/oracle/leaf_spec.1.res.oracle
@@ -9,9 +9,9 @@
[kernel:annot:missing-spec] tests/value/leaf_spec.i:27: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
-[eva] tests/value/leaf_spec.i:27: Warning:
+[eva:invalid-assigns] tests/value/leaf_spec.i:27:
Completely invalid destination for assigns clause *x. Ignoring.
-[eva] tests/value/leaf_spec.i:27: Warning:
+[eva:invalid-assigns] tests/value/leaf_spec.i:27:
Completely invalid destination for assigns clause *y. Ignoring.
[eva] Done for function f
[eva] Recording results for main1