ivette/src/renderer/Laboratory.tsx

@@ -51,8 +51,8 @@ const UPDATE = new Dome.Event('labview.library');
 
 class Library {
   modified: boolean;
-  virtual: {};
-  collection: {};
+  virtual: any;
+  collection: any;
   items: any[];
 
   constructor() {

ivette/src/renderer/style.css

@@ -65,3 +65,5 @@
 .dome-window-active .labview-icon {
     fill: #7d7d7d ;
 }
+
+/* -------------------------------------------------------------------------- */

ivette/tsconfig.json

@@ -4,6 +4,7 @@
     // "incremental": true,                   /* Enable incremental compilation */
     "target": "esnext",                       /* Specify ECMAScript target version: 'ES3' (default), 'ES5', 'ES2015', 'ES2016', 'ES2017', 'ES2018', 'ES2019', 'ES2020', or 'ESNEXT'. */
     "module": "esnext",                       /* Specify module code generation: 'none', 'commonjs', 'amd', 'system', 'umd', 'es2015', 'es2020', or 'ESNext'. */
+    "skipLibCheck": true,
     // "lib": [],                             /* Specify library files to be included in the compilation. */
     "allowJs": true,                          /* Allow javascript files to be compiled. */
     // "checkJs": true,                       /* Report errors in .js files. */
@@ -89,30 +90,16 @@
   ],
   "typedocOptions": {
     "name": "Ivette Documentation",
-    "mode": "modules",
     "out": "doc/html",
     "includeVersion": true,
     "disableSources": true,
     "excludePrivate": true,
-    "excludeNotExported": true,
     "excludeExternals": true,
     "categorizeByGroup": false,
     "categoryOrder": [ "Hooks", "Components", "*", "Other" ],
-    "stripInternal": true,
-    "listInvalidSymbolLinks":true,
     "hideGenerator":true,
-    "readme": "./README.md",
-    "inputFiles": [
-      "doc/pages",
-      "src/ivette/index.tsx",
-      "src/ivette/prefs.tsx",
-      "src/frama-c/server.ts",
-      "src/frama-c/states.ts",
-      "src/frama-c/utils.ts",
-      "src/frama-c/api/generated",
-      "src/dome/renderer",
-      "src/dome/misc/utils.ts",
-      "src/dome/misc/system.ts",
-    ]
+    "includes": "src/dome/doc/guides",
+    "customCss": "src/dome/doc/gallery.css",
+    "readme": "none"
   }
 }

ivette/webpack.main.js

@@ -63,6 +63,11 @@ module.exports = {
       'dome/system$':  path.resolve( DOME , 'misc/system.ts' ),
       'dome/devtools': domeDevtools()
     }
+  },
+  devServer: {
+    watchOptions: {
+      ignored: '**/.#'
+    }
   }
 } ;
 

ivette/webpack.renderer.js

@@ -60,6 +60,11 @@ module.exports = {
       'dome':         path.resolve( DOME , 'renderer' ),
       'react-dom':    '@hot-loader/react-dom'
     }
+  },
+  devServer: {
+    watchOptions: {
+      ignored: '**/.#*'
+    }
   }
 } ;
 

opam/opam

@@ -137,13 +137,6 @@ depopts: [
   "zmq"
 ]
 
-messages: [
-  "The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)"
-  {alt-ergo:installed}
-  "The Frama-C/Wp native support for Coq is deprecated and only activated with Coq.8.13.x (use TIP or Why-3 instead)."
-  {coq:installed}
-]
-
 post-messages: [
   "Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect"
 ]

ptests/ptests.ml

@@ -76,6 +76,26 @@ let str_string_match regex s n =
   let res = Str.string_match regex s n in
   Mutex.unlock str_mutex; res
 
+let str_string_match1 regexp line pos =
+  Mutex.lock str_mutex;
+  let res = if Str.string_match regexp line pos then
+      try
+        Some (Str.matched_group 1 line)
+      with Not_found -> None
+    else None
+  in
+  Mutex.unlock str_mutex; res
+
+let str_string_match2 regexp line pos =
+  Mutex.lock str_mutex;
+  let res = if Str.string_match regexp line pos then
+      try
+        Some ((Str.matched_group 1 line), (Str.matched_group 2 line))
+      with Not_found -> None
+    else None
+  in
+  Mutex.unlock str_mutex; res
+
 (* If regex1 matches inside s, adds suffix to the first occurrence of regex2.
    If matched, returns (replaced string, true), otherwise returns (s, false).
 *)
@@ -553,7 +573,7 @@ let parse_config_line =
   fun (key, value) ->
     match key with
     | "DEFAULT_SUITES" ->
-      let l = Str.split regexp_blank value in
+      let l = str_split regexp_blank value in
       default_suites := List.map (Filename.concat test_path) l
     | "TOPLEVEL_PATH" ->
       toplevel_path := value
@@ -570,14 +590,11 @@ let () =
       let regexp = Str.regexp "\\([^=]+\\)=\\(.*\\)" in
       while true do
         let line = input_line ch in
-        if Str.string_match regexp line 0 then
-          let key = Str.matched_group 1 line in
-          let value = Str.matched_group 2 line in
-          parse_config_line (key, value)
-        else begin
+        match str_string_match2 regexp line 0 with
+        | Some (key,value) -> parse_config_line (key, value)
+        | None ->
           Format.eprintf "Cannot interpret line '%s' in ptests_config@." line;
           exit 1
-        end
       done
     with
     | End_of_file ->
@@ -708,7 +725,7 @@ let mk_symbolic_link =
         symlink ~unlink:false ~to_dir ~link_dst ~link
       else if String.(link_dst <> (Unix.readlink link)) then (* goes elsewhere *)
         symlink ~unlink:true ~to_dir ~link_dst ~link
-      else symlink_there link (* is already there *)
+      else symlink_there ~link (* is already there *)
     in
     match infos.st_kind with
     | Unix.S_LNK
@@ -758,9 +775,8 @@ struct
         let expand_macro = function
           | Str.Text s -> s
           | Str.Delim s ->
-            if Str.string_match macro_regex s 0 then begin
-              try
-                let macro = Str.matched_group 1 s in
+            match str_string_match1 macro_regex s 0  with
+            | Some macro -> begin
                 (match macro with
                  | "PTEST_FILE" -> has_ptest_file := true
                  | "PTEST_OPT" -> has_ptest_opt := true
@@ -768,25 +784,23 @@ struct
                  | "frama-c-exe" -> has_frama_c_exe := true
                  | _ -> ());
                 if !verbosity >= 5 then lock_printf "%%     - macro is %s\n%!" macro;
-                let replacement = find macro macros in
-                if !verbosity >= 4 then
-                  lock_printf "%%     - replacement for %s is %s\n%!" macro replacement;
-                aux replacement
-              with
-              | Not_found -> s
-            end
-            else s
+                try
+                  let replacement = find macro macros in
+                  if !verbosity >= 4 then
+                    lock_printf "%%     - replacement for %s is %s\n%!" macro replacement;
+                  aux replacement
+                with Not_found -> s
+              end
+            | None -> s
         in
         String.concat "" (List.map expand_macro (Str.full_split macro_regex s))
       in
-      Mutex.lock str_mutex;
-      let r = try aux s
+      let r =
+        try aux s
         with e ->
-          Mutex.unlock str_mutex;
           lock_eprintf "Uncaught exception %s\n%!" (Printexc.to_string e);
           raise e
       in
-      Mutex.unlock str_mutex;
       if !verbosity >= 4 then lock_printf "%% Expansion result: %s@." r;
       { has_ptest_file= !has_ptest_file;
         has_ptest_opt= !has_ptest_opt;
@@ -1332,7 +1346,7 @@ end = struct
                name = "run.config" && !special_config = ""  ||
                name = "run.config_" ^ !special_config
              in
-             let configs = Str.split split_config (String.trim names) in
+             let configs = str_split split_config (String.trim names) in
              if List.exists is_current_config configs then
                (* Found options for current config! *)
                scan_directives ~drop:false dir ~file:f scan_buffer default
@@ -1915,23 +1929,24 @@ let check_file_is_empty_or_nonexisting diff ~log_file =
 (* Searches for executable [s] in the directories contained in the PATH
      environment variable. Returns [None] if not found, or
      [Some <fullpath>] otherwise. *)
-let find_in_path s =
-  let s = trim_right s in
+let find_in_path =
   let path_separator = if Sys.os_type = "Win32" then ";" else ":" in
   let re_path_sep = Str.regexp path_separator in
-  let path_dirs = Str.split re_path_sep (Sys.getenv "PATH") in
-  let found = ref "" in
-  try
-    List.iter (fun dir ->
-        let fullname = dir ^ Filename.dir_sep ^ s in
-        if Sys.file_exists fullname then begin
-          found := fullname;
-          raise Exit
-        end
-      ) path_dirs;
-    None
-  with Exit ->
-    Some !found
+  fun s ->
+    let s = trim_right s in
+    let path_dirs = str_split re_path_sep (Sys.getenv "PATH") in
+    let found = ref "" in
+    try
+      List.iter (fun dir ->
+          let fullname = dir ^ Filename.dir_sep ^ s in
+          if Sys.file_exists fullname then begin
+            found := fullname;
+            raise Exit
+          end
+        ) path_dirs;
+      None
+    with Exit ->
+      Some !found
 
 (* filter commands are executed from the same directory than test commands *)
 let get_filter_cmd = match !dune_mode with
@@ -1954,7 +1969,7 @@ let do_filter =
       let log_ext = log_ext kind in
       let log_file = Filename.sanitize (log_prefix ^ log_ext ^ ".log") in
       let foracle = (Filename.basename log_prefix) ^ log_ext ^ ".oracle" in
-      let filter = Str.global_replace regexp_ptest_oracle foracle filter in
+      let filter = str_global_replace regexp_ptest_oracle foracle filter in
       let exec_name, params = command_partition filter in
       let exec_name =
         if Sys.file_exists exec_name || not (Filename.is_relative exec_name)

share/autocomplete_frama-c

@@ -94,7 +94,7 @@ _frama-c ()
   then
       local prefix=; [[ $cur == *,* ]] && prefix="${cur%,*},"
       advance_options="$(frama-c -wp-detect | grep -E -o " \[.*" | grep -E -o "[^][|]*")"
-      advance_options+=" none script tip native:alt-ergo native:coq native:coqide"
+      advance_options+=" none script tip"
       local ambigous="$(bind -v | grep show-all-if-ambiguous)"
       ambigous="${ambigous##* }"
       if [[ "$ambigous" == "on" ]]

share/compliance/glibc_functions.json

@@ -929,6 +929,7 @@
         "mkfifo",
         "mknod",
         "mkstemp",
+        "mkstemps",
         "mktemp",
         "mktime",
         "mlock",

share/libc/__fc_define_locale_t.h

+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2021                                               */
+/*    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).            */
+/*                                                                        */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_LOCALE_T
+#define __FC_DEFINE_LOCALE_T
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+struct __fc_locale_struct
+{
+  const char *names[13];
+};
+
+typedef struct __fc_locale_struct *locale_t;
+__END_DECLS
+__POP_FC_STDLIB
+#endif

share/libc/__fc_gcc_builtins.h

@@ -254,6 +254,13 @@ int __builtin_popcountl (unsigned long x);
  */
 int __builtin_popcountll (unsigned long long x);
 
+// According to the GCC docs
+// (https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html),
+// this creates a 'full memory barrier'; we do not model the concurrency
+// aspects yet.
+/*@ assigns \nothing; */
+void __sync_synchronize(void);
+
 __END_DECLS
 
 __POP_FC_STDLIB

share/libc/__fc_libc.h

@@ -51,6 +51,7 @@
 #include "ifaddrs.h"
 #include "inttypes.h"
 #include "iso646.h"
+#include "langinfo.h"
 #include "libgen.h"
 #include "limits.h"
 #include "locale.h"
@@ -79,6 +80,7 @@
 #include "stdint.h"
 #include "stdio.h"
 #include "stdlib.h"
+#include "stdnoreturn.h"
 #include "string.h"
 #include "strings.h"
 #include "stropts.h"

share/libc/fcntl.h

@@ -63,6 +63,9 @@ __PUSH_FC_STDLIB
 #define O_TRUNC 0x200
 //#define O_TTY_INIT
 
+// Non-POSIX
+#define O_DIRECT 0x4000
+
 #define O_APPEND 0x400
 #define O_DSYNC 0x1000
 #define O_NONBLOCK 0x800

share/libc/langinfo.h

+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2021                                               */
+/*    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).            */
+/*                                                                        */
+/**************************************************************************/
+
+#ifndef __FC_LANGINFO_H
+#define __FC_LANGINFO_H
+#include "features.h"
+__PUSH_FC_STDLIB
+#include "__fc_define_locale_t.h"
+#include "nl_types.h"
+#include "locale.h" // for LC_CTYPE and other constants
+__BEGIN_DECLS
+
+
+#define _NL_ITEM(category, index)	(((category) << 16) | (index))
+
+/* Extract the category and item index from a constructed `nl_item' value.  */
+#define _NL_ITEM_CATEGORY(item)		((int) (item) >> 16)
+#define _NL_ITEM_INDEX(item)		((int) (item) & 0xffff)
+
+enum
+{
+  CODESET = (LC_CTYPE) << 16,
+#define CODESET CODESET
+  ABDAY_1 = (LC_TIME) << 16,
+#define ABDAY_1 ABDAY_1
+  ABDAY_2,
+#define ABDAY_2 ABDAY_2
+  ABDAY_3,
+#define ABDAY_3 ABDAY_3
+  ABDAY_4,
+#define ABDAY_4 ABDAY_4
+  ABDAY_5,
+#define ABDAY_5 ABDAY_5
+  ABDAY_6,
+#define ABDAY_6 ABDAY_6
+  ABDAY_7,
+#define ABDAY_7 ABDAY_7
+  DAY_1,
+#define DAY_1 DAY_1
+  DAY_2,
+#define DAY_2 DAY_2
+  DAY_3,
+#define DAY_3 DAY_3
+  DAY_4,
+#define DAY_4 DAY_4
+  DAY_5,
+#define DAY_5 DAY_5
+  DAY_6,
+#define DAY_6 DAY_6
+  DAY_7,
+#define DAY_7 DAY_7
+  ABMON_1,
+#define ABMON_1 ABMON_1
+  ABMON_2,
+#define ABMON_2 ABMON_2
+  ABMON_3,
+#define ABMON_3 ABMON_3
+  ABMON_4,
+#define ABMON_4 ABMON_4
+  ABMON_5,
+#define ABMON_5 ABMON_5
+  ABMON_6,
+#define ABMON_6 ABMON_6
+  ABMON_7,
+#define ABMON_7 ABMON_7
+  ABMON_8,
+#define ABMON_8 ABMON_8
+  ABMON_9,
+#define ABMON_9 ABMON_9
+  ABMON_10,
+#define ABMON_10 ABMON_10
+  ABMON_11,
+#define ABMON_11 ABMON_11
+  ABMON_12,
+#define ABMON_12 ABMON_12
+  MON_1,
+#define MON_1 MON_1
+  MON_2,
+#define MON_2 MON_2
+  MON_3,
+#define MON_3 MON_3
+  MON_4,
+#define MON_4 MON_4
+  MON_5,
+#define MON_5 MON_5
+  MON_6,
+#define MON_6 MON_6
+  MON_7,
+#define MON_7 MON_7
+  MON_8,
+#define MON_8 MON_8
+  MON_9,
+#define MON_9 MON_9
+  MON_10,
+#define MON_10 MON_10
+  MON_11,
+#define MON_11 MON_11
+  MON_12,
+#define MON_12 MON_12
+  AM_STR,
+#define AM_STR AM_STR
+  PM_STR,
+#define PM_STR PM_STR
+  D_T_FMT,
+#define D_T_FMT D_T_FMT
+  D_FMT,
+#define D_FMT D_FMT
+  T_FMT,
+#define T_FMT T_FMT
+  T_FMT_AMPM,
+#define T_FMT_AMPM T_FMT_AMPM
+  ERA,
+#define ERA ERA
+  ERA_YEAR, // Non-POSIX; GNU
+#define ERA_YEAR ERA_YEAR
+  ERA_D_FMT,
+#define ERA_D_FMT ERA_D_FMT
+  ALT_DIGITS,
+#define ALT_DIGITS ALT_DIGITS
+  ERA_D_T_FMT,
+#define ERA_D_T_FMT ERA_D_T_FMT
+  ERA_T_FMT,
+#define ERA_T_FMT ERA_T_FMT
+  DECIMAL_POINT = (LC_NUMERIC) << 16, // Non-POSIX; GNU
+#define DECIMAL_POINT DECIMAL_POINT
+  RADIXCHAR,
+#define RADIXCHAR RADIXCHAR
+  THOUSEP,
+#define THOUSEP THOUSEP
+  YESEXPR = (LC_MESSAGES) << 16,
+#define YESEXPR YESEXPR
+  NOEXPR,
+#define NOEXPR NOEXPR
+  CRNCYSTR = (LC_MONETARY) << 16,
+#define CRNCYSTR CRNCYSTR
+};
+
+extern char *nl_langinfo(nl_item item);
+extern char *nl_langinfo_l(nl_item item, locale_t locale);
+
+__END_DECLS
+
+__POP_FC_STDLIB
+#endif

share/libc/locale.h

@@ -24,7 +24,7 @@
 #define __FC_LOCALE
 #include "features.h"
 __PUSH_FC_STDLIB
-
+#include "__fc_define_locale_t.h"
 __BEGIN_DECLS
 
 /* Structure giving information about numeric and monetary notation.  */
@@ -149,6 +149,11 @@ extern char *setlocale(int category, const char *locale);
 */
 extern struct lconv *localeconv(void);
 
+extern locale_t duplocale(locale_t);
+extern void freelocale(locale_t);
+extern locale_t newlocale(int, const char *, locale_t);
+extern locale_t uselocale(locale_t);
+
 __END_DECLS
 
 __POP_FC_STDLIB

share/libc/regex.h

@@ -25,10 +25,16 @@
 #include "features.h"
 __PUSH_FC_STDLIB
 #include "__fc_define_size_t.h"
-
+#include "__fc_define_ssize_t.h"
 __BEGIN_DECLS
 
-struct re_pattern_buffer { size_t re_nsub;  };
+struct re_pattern_buffer {
+  struct re_dfa_t *buffer; // Non-POSIX
+  size_t allocated; // Non-POSIX
+  char *fastmap; // Non-POSIX
+  unsigned char *translate; // Non-POSIX
+  size_t re_nsub;
+};
 
 typedef struct re_pattern_buffer regex_t;
 
@@ -64,7 +70,15 @@ typedef enum __fc_reg_errcode_t
   REG_ERPAREN	  
 } reg_errcode_t;
 
-typedef int regoff_t;
+typedef ssize_t regoff_t;
+
+// Non-POSIX
+struct re_registers
+{
+  size_t num_regs;
+  regoff_t *start;
+  regoff_t *end;
+};
 
 typedef struct __fc_regmatch_t
 {

share/libc/stdlib.c

@@ -232,4 +232,9 @@ char *realpath(const char *restrict file_name, char *restrict resolved_name)
   return resolved_name;
 }
 
+char *canonicalize_file_name(const char *path) {
+  return realpath(path, NULL);
+}
+
+
 __POP_FC_STDLIB

share/libc/stdlib.h

@@ -692,6 +692,7 @@ extern int posix_memalign(void **memptr, size_t alignment, size_t size);
   // missing: requires 'last 6 characters of template must be XXXXXX'
   // missing: assigns \result, templat[0..] \from 'filesystem', 'RNG';
   requires valid_template: valid_string(templat);
+  requires template_len: strlen(templat) >= 6;
   assigns templat[0..] \from \nothing;
   assigns \result \from \nothing;
   ensures result_error_or_valid_fd: \result == -1 ||
@@ -699,9 +700,31 @@ extern int posix_memalign(void **memptr, size_t alignment, size_t size);
  */
 extern int mkstemp(char *templat);
 
+/*@
+  // missing: requires 'last (6+suffixlen) characters of template must be X's'
+  // missing: assigns \result, templat[0..] \from 'filesystem', 'RNG';
+  requires valid_template: valid_string(templat);
+  requires template_len: strlen(templat) >= 6 + suffixlen;
+  requires non_negative_suffixlen: suffixlen >= 0;
+  assigns templat[0..] \from \nothing;
+  assigns \result \from \nothing;
+  ensures result_error_or_valid_fd: \result == -1 ||
+                                    0 <= \result < __FC_FOPEN_MAX;
+ */
+extern int mkstemps(char *templat, int suffixlen);
+
+// This function may allocate memory for the result, which is not supported by
+// some plugins such as Eva. In such cases, it is preferable to use the stub
+// provided in stdlib.c.
 extern char *realpath(const char *restrict file_name,
                       char *restrict resolved_name);
 
+// Non-POSIX; GNU extension
+// This function may allocate memory for the result, which is not supported by
+// some plugins such as Eva. In such cases, it is preferable to use the stub
+// provided in stdlib.c.
+extern char *canonicalize_file_name(const char *path);
+
 __END_DECLS
 
 __POP_FC_STDLIB

share/libc/stdnoreturn.h

+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2021                                               */
+/*    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).            */
+/*                                                                        */
+/**************************************************************************/
+
+// This file is not in the C standard; it exists for compatibility purposes
+
+// 'noreturn' is an attribute in C++
+#ifndef __cpluscplus
+// Note that Frama-C still requires the '-c11' command-line option to parse
+// the _Noreturn keyword. Mere inclusion of this header without the option
+// will not work.
+#define noreturn _Noreturn
+#endif