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.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/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/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 9242ad5cc59fc33e58438943df8e6bacc28460a7..fd0a578c9bfc470d1027b7c1d141139e6c0511eb 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1080,7 +1080,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
@@ -1122,7 +1122,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