diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index db1d06dcb452781e69835717d02407024fad37da..8a8ff94767995424b50f31dcd026971ae48a1dd3 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,6 @@
Version number Date of release Notes
============== =============== =====
+27.1 (Cobalt) 2023, July, 18
27.0 (Cobalt) 2023, June, 15
26.1 (Iron) 2023, February 15
26.0 (Iron) 2022, November 23
diff --git a/Changelog b/Changelog
index e619fceeedb77c384c4a7f965b2de3e7359104ff..c36ddded8499c474455030207e7d2a87ccbde633 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,15 @@
Open Source Release <next-release>
###############################################################################
+###############################################################################
+Open Source Release 27.1 (Cobalt)
+###############################################################################
+
+- Kernel [2023-07-17] New frama-c-script wrapper for make_machdep.py
+-* Ivette [2023-07-06] Fixes crash with multiple instances
+-* GUI [2023-07-05] Fixes freeze when a plugin aborts during splash screen
+-* GUI [2023-07-05] Fixes crash related to tags and undefined types
+
###############################################################################
Open Source Release 27.0 (Cobalt)
###############################################################################
diff --git a/VERSION b/VERSION
index c49dfde59ea4943a4fad4f6f08b7c34f0d01e99d..fac6b38be1992b6403d0b57c5db9d59cb5284938 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-27.0+dev
+27.1+dev
diff --git a/bin/frama-c-script b/bin/frama-c-script
index 669573f5394d1bcd7cae750123a17f013204fbc8..3e2bfc9335f779c6637a22db14df6c23ffad0c30 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -279,6 +279,11 @@ case "$command" in
shift;
${FRAMAC_LIB}/analysis-scripts/creduce.sh "$@";
;;
+ "make-machdep")
+ shift;
+ ${FRAMAC_LIB}/make_machdep/make_machdep.py \
+ --machdep-schema ${FRAMAC_SHARE}/machdeps/machdep-schema.yaml "$@"
+ ;;
*)
echo "error: unrecognized command: $command";
exit 1
diff --git a/ivette/src/dome/main/dome.ts b/ivette/src/dome/main/dome.ts
index 993f45c5bdd104cb3bbe59bad0220b97631643ca..fde22418299c5565e527a09fd89da3ff7a1edec8 100644
--- a/ivette/src/dome/main/dome.ts
+++ b/ivette/src/dome/main/dome.ts
@@ -483,18 +483,15 @@ function createBrowserWindow(
theWindow.off('close', closeHandler);
// Do not close the window yet
event.preventDefault();
-
+ // Save state
handle.frame = theWindow.getBounds();
handle.devtools = webContents.isDevToolsOpened();
- webContents.send('dome.ipc.closing');
+ // Start closing process
+ webContents.send('dome.ipc.closing', wid);
};
theWindow.on('close', closeHandler);
- ipcMain.on('dome.ipc.closing.done', () => {
- theWindow.close();
- });
-
// Keep track of frame positions (in DEVEL)
if (DEVEL) {
const saveFrame = _.debounce(() => {
@@ -509,6 +506,11 @@ function createBrowserWindow(
return theWindow;
}
+ipcMain.on('dome.ipc.closing.done', (_event, wid:number) => {
+ const handle = WindowHandles.get(wid);
+ if (handle !== undefined) handle.window.close();
+});
+
// --------------------------------------------------------------------------
// --- Application Window(s) & Command Line
// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/dome.tsx b/ivette/src/dome/renderer/dome.tsx
index d05bbd025647811411d424b51848735991eb3992..07d8d0e2c23938c88e33202e92121b1f5ab03dcb 100644
--- a/ivette/src/dome/renderer/dome.tsx
+++ b/ivette/src/dome/renderer/dome.tsx
@@ -251,9 +251,9 @@ export const globalSettings = new Event(Settings.global);
// --- Closing
// --------------------------------------------------------------------------
-ipcRenderer.on('dome.ipc.closing', async () => {
+ipcRenderer.on('dome.ipc.closing', async (_event, wid: number) => {
await System.doExit();
- ipcRenderer.send('dome.ipc.closing.done');
+ ipcRenderer.send('dome.ipc.closing.done', wid);
});
/** Register a callback to be executed when the window is closing. */
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index 34beab7c25ad1b93e0890ec9831a9b19430a5d17..4be82fb950a17b6a28b4a09c0c8834462f96c25d 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -44,6 +44,8 @@
, dos2unix
, doxygen
, python3
+, python3Packages
+, yq
, release_mode ? false
}:
@@ -103,6 +105,8 @@ stdenvNoCC.mkDerivation rec {
dos2unix
doxygen
python3
+ python3Packages.pyaml
+ yq
];
outputs = [ "out" "build_dir" ];
diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index 52dff2811552ecc25594c603eff9237dd47feeb5..bef1ffdc48e296581309ef715d9f971583fdf197 100644
--- a/nix/internal-tests.nix
+++ b/nix/internal-tests.nix
@@ -48,6 +48,8 @@
, perl
, pkgs
, python3
+, python3Packages
+, yq
, swiProlog
, time
, wp-cache
@@ -109,6 +111,8 @@ stdenvNoCC.mkDerivation rec {
perl
pkgs.getopt
python3
+ python3Packages.pyaml
+ yq
swiProlog
time
];
diff --git a/opam b/opam
index d25a560388ebc8ae749a5028643d90244bebb789..ca6dd2be800bbd63a8293969fa83286e14ba63db 100644
--- a/opam
+++ b/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "27.0+dev"
+version: "27.1+dev"
description:"""
Frama-C gathers several analysis techniques in a single collaborative
framework, based on analyzers (called "plug-ins") that can build upon the
@@ -71,7 +71,7 @@ authors: [
homepage: "https://frama-c.com/"
license: "LGPL-2.1-only"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
-doc: "http://frama-c.com/download/user-manual-27.0-Cobalt.pdf"
+doc: "http://frama-c.com/download/user-manual-27.1-Cobalt.pdf"
bug-reports: "https://git.frama-c.com/pub/frama-c/issues"
tags: [
"deductive"
@@ -99,7 +99,7 @@ build: [
install: [
[make
- "PREFIX=%{prefix}%" "MANDIR=%{man}%"
+ "RELEASE=yes" "PREFIX=%{prefix}%" "MANDIR=%{man}%"
"DOCDIR=%{doc}%" { with-doc }
"install"
]
diff --git a/releases/27.1.md b/releases/27.1.md
new file mode 100644
index 0000000000000000000000000000000000000000..7c02e8a360357bbe63be5d2dd00dbee11ef1a4c1
--- /dev/null
+++ b/releases/27.1.md
@@ -0,0 +1,6 @@
+# Kernel
+- Fixes a crash and a freeze in the GTK GUI
+- Add a wrapper in `frama-c-script` pour `make_machdep.py`
+
+# Ivette
+- Fixes a crash with multiple instances of Ivette
diff --git a/share/dune b/share/dune
index 77f771002d1b2e413dd411f13512b51fbf62f5b9..f00d3b92a5ed96459a035d8ca93acd082c366e9c 100644
--- a/share/dune
+++ b/share/dune
@@ -339,7 +339,9 @@
(machdeps/machdep_gcc_x86_32.yaml as share/machdeps/machdep_gcc_x86_32.yaml)
(machdeps/machdep_gcc_x86_64.yaml as share/machdeps/machdep_gcc_x86_64.yaml)
(machdeps/machdep_msvc_x86_64.yaml as share/machdeps/machdep_msvc_x86_64.yaml)
- (machdeps/machdep_ppc_32.yaml as share/machdeps/machdep_ppc_32.yaml))
+ (machdeps/machdep_ppc_32.yaml as share/machdeps/machdep_ppc_32.yaml)
+ (machdeps/machdep-schema.yaml as share/machdeps/machdep-schema.yaml)
+ )
)
; machdep generation script
@@ -368,9 +370,21 @@
(machdeps/make_machdep/alignof_str.c as lib/make_machdep/alignof_str.c)
(machdeps/make_machdep/char_is_unsigned.c as lib/make_machdep/char_is_unsigned.c)
(machdeps/make_machdep/const_string_literals.c as lib/make_machdep/const_string_literals.c)
+ (machdeps/make_machdep/errno.c as lib/make_machdep/errno.c)
(machdeps/make_machdep/has__builtin_va_list.c as lib/make_machdep/has__builtin_va_list.c)
+ (machdeps/make_machdep/int_fast16_t.c as lib/make_machdep/int_fast16_t.c)
+ (machdeps/make_machdep/int_fast32_t.c as lib/make_machdep/int_fast32_t.c)
+ (machdeps/make_machdep/int_fast64_t.c as lib/make_machdep/int_fast64_t.c)
+ (machdeps/make_machdep/int_fast8_t.c as lib/make_machdep/int_fast8_t.c)
+ (machdeps/make_machdep/intptr_t.c as lib/make_machdep/intptr_t.c)
+ (machdeps/make_machdep/limits_macros.c as lib/make_machdep/limits_macros.c)
(machdeps/make_machdep/little_endian.c as lib/make_machdep/little_endian.c)
+ (machdeps/make_machdep/make_machdep_common.h as lib/make_machdep/make_machdep_common.h)
+ (machdeps/make_machdep/nsig.c as lib/make_machdep/nsig.c)
+ (machdeps/make_machdep/posix_version.c as lib/make_machdep/posix_version.c)
(machdeps/make_machdep/ptrdiff_t.c as lib/make_machdep/ptrdiff_t.c)
+ (machdeps/make_machdep/sanity_check.c as lib/make_machdep/sanity_check.c)
+ (machdeps/make_machdep/sig_atomic_t.c as lib/make_machdep/sig_atomic_t.c)
(machdeps/make_machdep/sizeof_double.c as lib/make_machdep/sizeof_double.c)
(machdeps/make_machdep/sizeof_float.c as lib/make_machdep/sizeof_float.c)
(machdeps/make_machdep/sizeof_fun.c as lib/make_machdep/sizeof_fun.c)
@@ -382,6 +396,17 @@
(machdeps/make_machdep/sizeof_short.c as lib/make_machdep/sizeof_short.c)
(machdeps/make_machdep/sizeof_void.c as lib/make_machdep/sizeof_void.c)
(machdeps/make_machdep/size_t.c as lib/make_machdep/size_t.c)
+ (machdeps/make_machdep/ssize_t.c as lib/make_machdep/ssize_t.c)
+ (machdeps/make_machdep/stdio_macros.c as lib/make_machdep/stdio_macros.c)
+ (machdeps/make_machdep/stdlib_macros.c as lib/make_machdep/stdlib_macros.c)
+ (machdeps/make_machdep/time_t.c as lib/make_machdep/time_t.c)
+ (machdeps/make_machdep/uint_fast16_t.c as lib/make_machdep/uint_fast16_t.c)
+ (machdeps/make_machdep/uint_fast32_t.c as lib/make_machdep/uint_fast32_t.c)
+ (machdeps/make_machdep/uint_fast64_t.c as lib/make_machdep/uint_fast64_t.c)
+ (machdeps/make_machdep/uint_fast8_t.c as lib/make_machdep/uint_fast8_t.c)
+ (machdeps/make_machdep/uintptr_t.c as lib/make_machdep/uintptr_t.c)
(machdeps/make_machdep/wchar_t.c as lib/make_machdep/wchar_t.c)
- (machdeps/make_machdep/make_machdep_common.h as lib/make_machdep/make_machdep_common.h)
+ (machdeps/make_machdep/weof.c as lib/make_machdep/weof.c)
+ (machdeps/make_machdep/wint_t.c as lib/make_machdep/wint_t.c)
+ (machdeps/make_machdep/wordsize.c as lib/make_machdep/wordsize.c)
))
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index f5ee3f6c8487f9c21f3de15a75d7255d4ff617d8..055d78e85c3d33563175e3c2c5f2e8d3c2508b8a 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
- -target
- avr
- -m16
+- -mmcu=atmega16
custom_defs: |
#undef AVR
#define AVR 1
@@ -33,6 +34,8 @@ custom_defs: |
#define __ATOMIC_SEQ_CST 5
#undef __AVR
#define __AVR 1
+ #undef __AVR_ATmega16__
+ #define __AVR_ATmega16__ 1
#undef __AVR__
#define __AVR__ 1
#undef __BIGGEST_ALIGNMENT__
@@ -645,6 +648,8 @@ custom_defs: |
#define __clang_version__ "15.0.7 "
#undef __clang_wide_literal_encoding__
#define __clang_wide_literal_encoding__ "UTF-16"
+ #undef __flash
+ #define __flash __attribute__((address_space(1)))
#undef __llvm__
#define __llvm__ 1
eof: (-1)
diff --git a/share/machdeps/machdep_avr_8.yaml b/share/machdeps/machdep_avr_8.yaml
index 9a9268a4d5590425281b29da80561ab9d037b8cd..cbaeb67bbd3b9626e1cba28f416efded67c9cd79 100644
--- a/share/machdeps/machdep_avr_8.yaml
+++ b/share/machdeps/machdep_avr_8.yaml
@@ -15,6 +15,7 @@ compiler: clang
cpp_arch_flags:
- -target
- avr
+- -mmcu=atmega8
custom_defs: |
#undef AVR
#define AVR 1
@@ -32,6 +33,8 @@ custom_defs: |
#define __ATOMIC_SEQ_CST 5
#undef __AVR
#define __AVR 1
+ #undef __AVR_ATmega8__
+ #define __AVR_ATmega8__ 1
#undef __AVR__
#define __AVR__ 1
#undef __BIGGEST_ALIGNMENT__
@@ -644,6 +647,8 @@ custom_defs: |
#define __clang_version__ "15.0.7 "
#undef __clang_wide_literal_encoding__
#define __clang_wide_literal_encoding__ "UTF-16"
+ #undef __flash
+ #define __flash __attribute__((address_space(1)))
#undef __llvm__
#define __llvm__ 1
eof: (-1)
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index bd0b6cefa82eeebfdbf575326681d26122018c34..c6045ab856a81cc991fbda527d32ca5648914719 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -49,8 +49,6 @@ from yaml.representer import Representer
my_path = Path(sys.argv[0]).parent
-logging.basicConfig(format="%(levelname)s: %(message)s")
-
parser = argparse.ArgumentParser(prog="make_machdep")
parser.add_argument("-v", "--verbose", action="store_true")
parser.add_argument("-o", type=argparse.FileType("w"), dest="dest_file")
@@ -61,6 +59,12 @@ parser.add_argument(
help="option to pass to the compiler to obtain its version; default is --version",
)
+parser.add_argument(
+ "--machdep-schema",
+ default="machdep-schema.yaml",
+ help="location of the schema file describing a machdep; default is 'machdep-schema.yaml'",
+)
+
parser.add_argument(
"--from-file",
help="reads compiler and arch flags from existing yaml file. Use -i to update it in place",
@@ -98,6 +102,11 @@ parser.add_argument(
args, other_args = parser.parse_known_args()
+if args.verbose:
+ logging.basicConfig(format="%(levelname)s: %(message)s", level=logging.INFO)
+else:
+ logging.basicConfig(format="%(levelname)s: %(message)s")
+
if not args.compiler_flags:
args.compiler_flags = ["-c"]
@@ -106,8 +115,7 @@ if not args.cpp_arch_flags:
def make_schema():
- schema_filename = my_path.parent / "machdep-schema.yaml"
- with open(schema_filename, "r") as schema:
+ with open(args.machdep_schema, "r") as schema:
return yaml.safe_load(schema)
@@ -275,11 +283,9 @@ def find_value(name, typ, output):
machdep[name] = value
else:
logging.warning(
- f"cannot find value of field '{name}', using default value: '{default}'"
+ f"cannot find value of field '{name}', using default value: '{default}'\ncompiler output is:\n{output}"
)
machdep[name] = default
- if args.verbose:
- print(f"compiler output is:{output}")
else:
logging.warning(f"unexpected symbol '{name}', ignoring")
@@ -331,9 +337,9 @@ for f, typ in source_files:
continue
if typ == "macro":
if proc.returncode != 0:
- logging.warning(f"error in preprocessing value '{p}', some values won't be filled")
- if args.verbose:
- print(f"compiler output is:{proc.stderr.decode()}")
+ logging.warning(
+ f"error in preprocessing value '{p}', some values won't be filled\ncompiler output is:\n{proc.stderr.decode()}"
+ )
name = p.stem
if name in machdep:
machdep[name] = ""
@@ -343,9 +349,9 @@ for f, typ in source_files:
if typ == "macrolist":
name = p.stem
if proc.returncode != 0:
- logging.warning(f"error in preprocessing value '{p}', some value might not be filled")
- if args.verbose:
- print(f"compiler output is:{proc.stderr.decode()}")
+ logging.warning(
+ f"error in preprocessing value '{p}', some values might not be filled\ncompiler output is:{proc.stderr.decode()}"
+ )
if name in machdep:
machdep[name] = {}
continue
@@ -416,9 +422,7 @@ if proc.returncode == 0:
lines += f"{line.strip()}\n"
machdep["custom_defs"] = custom_defs(lines)
else:
- logging.warning("could not determine predefined macros")
- if args.verbose:
- print(f"compiler output is:{proc.stderr}")
+ logging.warning(f"could not determine predefined macros. compiler output is:\n{proc.stderr}")
if args.from_file and args.in_place:
machdep["machdep_name"] = Path(args.from_file).stem
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index dc3f0d40495c6ad04ec9a4d9a40aa80e5b1dc3f0..ffe3da9c20d58e47a2f9e218a137a49a616aa47e 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -840,19 +840,25 @@ struct
super#fkind c
method! compname fmt comp =
- Format.fprintf fmt "@{<%s>%a@}"
- (Info.tag (PGlobal(Globals.Types.global Struct comp.cname)))
- super#compname comp
+ try
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Info.tag (PGlobal(Globals.Types.global Struct comp.cname)))
+ super#compname comp
+ with Not_found -> super#compname fmt comp
method! enuminfo fmt enum =
- Format.fprintf fmt "@{<%s>%a@}"
- (Info.tag (PGlobal(Globals.Types.global Enum enum.ename)))
- super#enuminfo enum
+ try
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Info.tag (PGlobal(Globals.Types.global Enum enum.ename)))
+ super#enuminfo enum
+ with Not_found -> super#enuminfo fmt enum
method! typeinfo fmt tinfo =
- Format.fprintf fmt "@{<%s>%a@}"
- (Info.tag (PGlobal(Globals.Types.global Typedef tinfo.tname)))
- super#typeinfo tinfo
+ try
+ Format.fprintf fmt "@{<%s>%a@}"
+ (Info.tag (PGlobal(Globals.Types.global Typedef tinfo.tname)))
+ super#typeinfo tinfo
+ with Not_found -> super#typeinfo fmt tinfo
initializer force_brace <- true
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8d365c6d4a829724b44bdaac91bb6c491d01fb05..d0829960b6f98351aafa8264a28f34ae5934c948 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,10 @@
Plugin E-ACSL <next-release>
###############################################################################
+###############################################################################
+Plugin E-ACSL 27.1 (Cobalt)
+###############################################################################
+
###############################################################################
Plugin E-ACSL 27.0 (Cobalt)
###############################################################################
diff --git a/src/plugins/e-acsl/tests/builtin/dune b/src/plugins/e-acsl/tests/builtin/dune
index 9dbf4e24533a7de7d1e1946bcef58497e1507f23..60c73d79b871aac38f96989e746ac1ce4757a8b0 100644
--- a/src/plugins/e-acsl/tests/builtin/dune
+++ b/src/plugins/e-acsl/tests/builtin/dune
@@ -1,7 +1,7 @@
(subdir
result/utils
- (copy_files ../../utils/*))
+ (copy_files ../../../utils/*))
(subdir
result_dev/utils
- (copy_files ../../utils/*))
+ (copy_files ../../../utils/*))
diff --git a/src/plugins/e-acsl/tests/builtin/utils b/src/plugins/e-acsl/tests/builtin/utils
deleted file mode 120000
index 19985ba50b51e1b7741a400a0b24ee16739553af..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/builtin/utils
+++ /dev/null
@@ -1 +0,0 @@
-../utils/
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/format/dune b/src/plugins/e-acsl/tests/format/dune
index 9dbf4e24533a7de7d1e1946bcef58497e1507f23..60c73d79b871aac38f96989e746ac1ce4757a8b0 100644
--- a/src/plugins/e-acsl/tests/format/dune
+++ b/src/plugins/e-acsl/tests/format/dune
@@ -1,7 +1,7 @@
(subdir
result/utils
- (copy_files ../../utils/*))
+ (copy_files ../../../utils/*))
(subdir
result_dev/utils
- (copy_files ../../utils/*))
+ (copy_files ../../../utils/*))
diff --git a/src/plugins/e-acsl/tests/format/utils b/src/plugins/e-acsl/tests/format/utils
deleted file mode 120000
index 19985ba50b51e1b7741a400a0b24ee16739553af..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/format/utils
+++ /dev/null
@@ -1 +0,0 @@
-../utils/
\ No newline at end of file
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index d9e13758325b50ceeb393c0d654d61e97542e8bb..2442eb86f7141a0e31f1af8e7d7047843abaa5d5 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1891,27 +1891,26 @@ let toplevel play =
let error_manager =
new Gtk_helper.error_manager (splash_w:>GWindow.window_skel)
in
- let init_crashed = ref true in
+ let init_crash = ref None in
error_manager#protect
~cancelable:true ~parent:(splash_w:>GWindow.window_skel)
(fun () ->
- (try
- play ();
- (* This is a good point to start using real asynchronous tasks
- management: plug-ins launched from command line have finished
- their asynchronous tasks thanks to the default Task.on_idle. *)
- 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
- 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
- realization before we create the error dialog widget.*)
- force_s (); raise e);
- init_crashed := false);
+ try
+ play ();
+ (* This is a good point to start using real asynchronous tasks
+ management: plug-ins launched from command line have finished
+ their asynchronous tasks thanks to the default Task.on_idle. *)
+ 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
+ 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
+ realization before we create the error dialog widget.*)
+ force_s (); init_crash := Some e; raise e);
if Ast.is_computed () then
(* if the ast has parsed, but a plugin has crashed, we display the gui *)
error_manager#protect ~cancelable:false
@@ -1921,18 +1920,18 @@ let toplevel play =
Glib.Timeout.remove tid;
reparent_console main_ui#lower_notebook;
splash_w#destroy ();
- (* Display the console if a crash has occurred. Otherwise, display
- the information panel *)
- if !init_crashed then
- (main_ui#lower_notebook#goto_page 2;
- (* BY TODO: this should scroll to the end of the console. It
- does not work at all after the reparent, and only partially
- before (scrollbar is wrong) *)
- let end_console = splash_out#buffer#end_iter in
- ignore (splash_out#scroll_to_iter ~yalign:0. end_console)
- )
- else
- main_ui#lower_notebook#goto_page 0
+ (* Display the console and an error dialog if a crash has occurred.
+ Otherwise, display the information panel. *)
+ match !init_crash with
+ | None -> main_ui#lower_notebook#goto_page 0
+ | Some e ->
+ main_ui#lower_notebook#goto_page 2;
+ (* BY TODO: this should scroll to the end of the console. It
+ does not work at all after the reparent, and only partially
+ before (scrollbar is wrong) *)
+ let end_console = splash_out#buffer#end_iter in
+ ignore (splash_out#scroll_to_iter ~yalign:0. end_console);
+ error_manager#error ~reset:true "%s" (Cmdline.protect e);
)
in
ignore (Glib.Idle.add (fun () -> in_idle (); false));
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index fd6b8762e486ad03c124f332b8acad806992cfb7..7ca273c4caa42910c0f3909f27ce949ff3eaadcf 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -738,6 +738,7 @@ class error_manager ?reset (o_parent:GWindow.window_skel) : host =
~title:"Error"
~position:`CENTER_ALWAYS
~modal:true
+ ~destroy_with_parent:true
()
in
ignore (w#connect#response ~callback:(fun _ -> w#destroy ()));
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index e5014c708ca44c9f13901cc81eb4f44c82067707..ffb6adc03608fee48db598b77fe3a7e3ba00fb84 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -36,6 +36,10 @@ Plugin WP <next-release>
- WP [2023-06-05] ACSL extension 'strategy' for proof strategies
- WP [2023-06-05] ACSL extension 'proof' for proof resolution hints
+###############################################################################
+Plugin WP 27.1 (Cobalt)
+###############################################################################
+
###############################################################################
Plugin WP 27.0 (Cobalt)
###############################################################################
diff --git a/tests/fc_script/oracle/custom_machdep.yaml b/tests/fc_script/oracle/custom_machdep.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..24f472d19e21723c8f7bf328c8ff0a0bea41a373
--- /dev/null
+++ b/tests/fc_script/oracle/custom_machdep.yaml
@@ -0,0 +1,183 @@
+alignof_aligned: 16
+alignof_double: 8
+alignof_float: 4
+alignof_fun: 4
+alignof_int: 4
+alignof_long: 8
+alignof_longdouble: 16
+alignof_longlong: 8
+alignof_ptr: 8
+alignof_short: 2
+alignof_str: 1
+bufsiz: '8192'
+char_is_unsigned: false
+compiler: clang
+cpp_arch_flags:
+ - --target=x86_64
+eof: (-1)
+errno:
+ e2big: '7'
+ eacces: '13'
+ eaddrinuse: '98'
+ eaddrnotavail: '99'
+ eafnosupport: '97'
+ eagain: '11'
+ ealready: '114'
+ ebade: '52'
+ ebadf: '9'
+ ebadfd: '77'
+ ebadmsg: '74'
+ ebadr: '53'
+ ebadrqc: '56'
+ ebadslt: '57'
+ ebusy: '16'
+ ecanceled: '125'
+ echild: '10'
+ echrng: '44'
+ ecomm: '70'
+ econnaborted: '103'
+ econnrefused: '111'
+ econnreset: '104'
+ edeadlk: '35'
+ edeadlock: '35'
+ edestaddrreq: '89'
+ edom: '33'
+ edquot: '122'
+ eexist: '17'
+ efault: '14'
+ efbig: '27'
+ ehostdown: '112'
+ ehostunreach: '113'
+ eidrm: '43'
+ eilseq: '84'
+ einprogress: '115'
+ eintr: '4'
+ einval: '22'
+ eio: '5'
+ eisconn: '106'
+ eisdir: '21'
+ eisnam: '120'
+ ekeyexpired: '127'
+ ekeyrejected: '129'
+ ekeyrevoked: '128'
+ el2hlt: '51'
+ el2nsync: '45'
+ el3hlt: '46'
+ el3rst: '47'
+ elibacc: '79'
+ elibbad: '80'
+ elibexec: '83'
+ elibmax: '82'
+ elibscn: '81'
+ eloop: '40'
+ emediumtype: '124'
+ emfile: '24'
+ emlink: '31'
+ emsgsize: '90'
+ emultihop: '72'
+ enametoolong: '36'
+ enetdown: '100'
+ enetreset: '102'
+ enetunreach: '101'
+ enfile: '23'
+ enobufs: '105'
+ enodata: '61'
+ enodev: '19'
+ enoent: '2'
+ enoexec: '8'
+ enokey: '126'
+ enolck: '37'
+ enolink: '67'
+ enomedium: '123'
+ enomem: '12'
+ enomsg: '42'
+ enonet: '64'
+ enopkg: '65'
+ enoprotoopt: '92'
+ enospc: '28'
+ enosr: '63'
+ enostr: '60'
+ enosys: '38'
+ enotblk: '15'
+ enotconn: '107'
+ enotdir: '20'
+ enotempty: '39'
+ enotrecoverable: '131'
+ enotsock: '88'
+ enotsup: '95'
+ enotty: '25'
+ enotuniq: '76'
+ enxio: '6'
+ eopnotsupp: '95'
+ eoverflow: '75'
+ eownerdead: '130'
+ eperm: '1'
+ epfnosupport: '96'
+ epipe: '32'
+ eproto: '71'
+ eprotonosupport: '93'
+ eprototype: '91'
+ erange: '34'
+ eremchg: '78'
+ eremote: '66'
+ eremoteio: '121'
+ erestart: '85'
+ erofs: '30'
+ eshutdown: '108'
+ esocktnosupport: '94'
+ espipe: '29'
+ esrch: '3'
+ estale: '116'
+ estrpipe: '86'
+ etime: '62'
+ etimedout: '110'
+ etxtbsy: '26'
+ euclean: '117'
+ eunatch: '49'
+ eusers: '87'
+ ewouldblock: '11'
+ exdev: '18'
+ exfull: '54'
+filename_max: '4096'
+fopen_max: '16'
+has__builtin_va_list: true
+host_name_max: '64'
+int_fast16_t: long
+int_fast32_t: long
+int_fast64_t: long
+int_fast8_t: signed char
+intptr_t: long
+l_tmpnam: '20'
+little_endian: true
+machdep_name: anonymous_machdep
+mb_cur_max: ((size_t)16)
+nsig: (64 + 1)
+path_max: '4096'
+posix_version: 200809L
+ptrdiff_t: long
+rand_max: '2147483647'
+sig_atomic_t: int
+size_t: unsigned long
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: 1
+sizeof_int: 4
+sizeof_long: 8
+sizeof_longdouble: 16
+sizeof_longlong: 8
+sizeof_ptr: 8
+sizeof_short: 2
+sizeof_void: 1
+ssize_t: long
+time_t: long
+tmp_max: '238328'
+tty_name_max: '32'
+uint_fast16_t: unsigned long
+uint_fast32_t: unsigned long
+uint_fast64_t: unsigned long
+uint_fast8_t: unsigned char
+uintptr_t: unsigned long
+wchar_t: int
+weof: (0xffffffffu)
+wint_t: int
+wordsize: '64'
diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res
index 58bf804e3c123e33f21c6761b63dcefa26e2e129..71eea9bdef1d36da92d821b392155e03e811c21e 100644
--- a/tests/fc_script/oracle/find_fun1.res
+++ b/tests/fc_script/oracle/find_fun1.res
@@ -1,4 +1,4 @@
-Looking for 'main2' inside 15 file(s)...
+Looking for 'main2' inside 16 file(s)...
Possible declarations for function 'main2' in the following file(s):
for-find-fun.c
Possible definitions for function 'main2' in the following file(s):
diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res
index d868795ee4e11b8858e75185cfd91d68ea8a24e7..5c9b9b69b9d58907335997f8db1b440930ca63ef 100644
--- a/tests/fc_script/oracle/find_fun2.res
+++ b/tests/fc_script/oracle/find_fun2.res
@@ -1,4 +1,4 @@
-Looking for 'main3' inside 15 file(s)...
+Looking for 'main3' inside 16 file(s)...
Possible declarations for function 'main3' in the following file(s):
for-find-fun2.c
Possible definitions for function 'main3' in the following file(s):
diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res
index 00f4bbc10eab9c20620426e670d9d0cf6b715762..67c26fc2681fd115eaca995ff472d4419c48248a 100644
--- a/tests/fc_script/oracle/find_fun3.res
+++ b/tests/fc_script/oracle/find_fun3.res
@@ -1,2 +1,2 @@
-Looking for 'false_positive' inside 15 file(s)...
+Looking for 'false_positive' inside 16 file(s)...
No declaration/definition found for function 'false_positive'
diff --git a/tests/fc_script/oracle/make_machdep.err.log b/tests/fc_script/oracle/make_machdep.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/fc_script/test_machdep.i b/tests/fc_script/test_machdep.i
new file mode 100644
index 0000000000000000000000000000000000000000..923485dde8e59c0631db3e506d95a6c23cf4699b
--- /dev/null
+++ b/tests/fc_script/test_machdep.i
@@ -0,0 +1,12 @@
+/* run.config
+ NOFRAMAC: Just test the generation of a custom machdep with the installed script.
+ COMMENT: No C code gets analyzed there. File is empty on purpose
+ COMMENT: be sure to keep the first EXECNOW: it ensures
+ COMMENT: that dune will copy the file regardless of the environment
+ COMMENT: so that other tests whose oracles depend on the number of file in
+ COMMENT: the directory will be stable.
+ EXECNOW: LOG empty.res touch empty.res
+ ENABLED_IF: (and %{bin-available:clang} %{bin-available:yq})
+ FILTER: sed -e '/^version:/d'
+ EXECNOW: LOG custom_machdep.yaml LOG make_machdep.err.log PTESTS_TESTING=1 %{bin:frama-c-script} make-machdep --compiler clang --cpp-arch-flags='--target=x86_64' | yq -Y 'del(.version)|del(.custom_defs)' > custom_machdep.yaml 2> make_machdep.err.log
+*/
diff --git a/tools/hdrck/frama-c-hdrck.opam b/tools/hdrck/frama-c-hdrck.opam
index acd43dffc4a7122b1a70a7ed71d9f1d2835a920b..f536d2fc26c201858ee02052f6b7c5d88a5673ce 100644
--- a/tools/hdrck/frama-c-hdrck.opam
+++ b/tools/hdrck/frama-c-hdrck.opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c-hdrck"
synopsis: "Frama-C header check tool"
-version: "27.0+dev"
+version: "27.1+dev"
description:"""
Performs all checks related to file headers as required by the Frama-C
continuous integration.
diff --git a/tools/lint/frama-c-lint.opam b/tools/lint/frama-c-lint.opam
index 08041265966df4bcb34b87e4a768a7faad40342b..8b70df8d1ef65a0b9e546f58f3c42090dbe48ba0 100644
--- a/tools/lint/frama-c-lint.opam
+++ b/tools/lint/frama-c-lint.opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c-lint"
synopsis: "Frama-C lint tool"
-version: "27.0+dev"
+version: "27.1+dev"
description:"""
Performs all checks related to source code formatting as required by the Frama-C
continuous integration. Namely: OCP-indent for ML files, clang-format for E-ACSL
diff --git a/tools/ptests/ptests.ml b/tools/ptests/ptests.ml
index 81a1426372abc479d2d2c085b661c4746869e4f4..4d1178925e63237b512ff43158d4324c99ae0070 100644
--- a/tools/ptests/ptests.ml
+++ b/tools/ptests/ptests.ml
@@ -1977,11 +1977,15 @@ let warn_if_not_enabled =
let dune_cond_regexp = Str.regexp "^(\\(.*\\))" in
let doublequote_regexp = Str.regexp "\"" in
let dune_var_regexp = Str.regexp "%{" in
+ let paren_regexp = Str.regexp "[()]" in
let dune_cond_item s = Str.global_replace dune_cond_regexp "\\1" s in
let escaped_cond s =
let s = Str.global_replace dune_var_regexp "\\%{" s in
Str.global_replace doublequote_regexp "\\\"" s
in
+ let safe_cond s =
+ Str.global_replace paren_regexp "\"\\0\"" s
+ in
fun ~env ~suite fmt enabled_if ->
if not (StringSet.is_empty enabled_if) then begin
Format.fprintf fmt
@@ -2000,7 +2004,7 @@ let warn_if_not_enabled =
let pp_enabled fmt cond =
let cond = dune_cond_item cond in
Format.fprintf fmt " (echo \"- %s: \" %s \"\\n\")\n "
- (escaped_cond cond) cond
+ (escaped_cond cond) (safe_cond cond)
in
let conds = StringSet.elements enabled_if in
Format.fprintf fmt
diff --git a/tools/ptests/wtests.ml b/tools/ptests/wtests.ml
index 9d4d84f9e74d96532ac1f6bc62d9aebbd8aaab5d..6c68edae0becccf09ef34ad4a4bcba4f69a66901 100644
--- a/tools/ptests/wtests.ml
+++ b/tools/ptests/wtests.ml
@@ -211,7 +211,8 @@ let wrapper json test =
let error = ret_code <> test.ret_code in
if error || !verbosity > 0 then begin
if test.out <> "" then print_file test.dir (if test.tmpout = "" then test.out else test.tmpout) ;
- if test.err <> "" then print_file test.dir (if test.tmperr = "" then test.err else test.tmperr)
+ if test.err <> "" then print_file test.dir (if test.tmperr = "" then test.err else test.tmperr) ;
+ List.iter (print_file test.dir) test.log
end;
if error then begin
Format.printf "%a: return code (%d) differs from the requested code (%d) for the command:%s@."