From 2cca8a49837dcd3204759e9c1cd02a88b7955090 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 7 Jan 2022 16:41:37 +0100
Subject: [PATCH] [Eva] add spec and builtin for reallocarray (GNU libc)
---
share/libc/stdlib.h | 35 +
.../e-acsl/tests/builtin/oracle/gen_strcat.c | 2 +-
.../e-acsl/tests/builtin/oracle/gen_strcmp.c | 4 +-
.../e-acsl/tests/builtin/oracle/gen_strcpy.c | 2 +-
.../e-acsl/tests/builtin/oracle/gen_strlen.c | 4 +-
.../tests/builtin/oracle/strcat.res.oracle | 4 +-
.../tests/builtin/oracle/strcmp.res.oracle | 8 +-
.../tests/builtin/oracle/strcpy.res.oracle | 4 +-
.../tests/builtin/oracle/strlen.res.oracle | 8 +-
.../concurrency/oracle/gen_parallel_threads.c | 2 +-
.../concurrency/oracle/gen_threads_debug.c | 2 +-
.../oracle/parallel_threads.res.oracle | 4 +-
.../oracle/threads_debug.res.oracle | 4 +-
.../tests/format/oracle/fprintf.res.oracle | 4 +-
.../e-acsl/tests/format/oracle/gen_fprintf.c | 2 +-
.../e-acsl/tests/format/oracle/gen_printf.c | 4 +-
.../tests/format/oracle/printf.res.oracle | 8 +-
.../e-acsl/tests/memory/oracle/gen_memalign.c | 8 +-
.../tests/memory/oracle/memalign.res.oracle | 14 +-
.../tests/temporal/oracle/gen_t_getenv.c | 2 +-
.../tests/temporal/oracle/t_getenv.res.oracle | 14 +-
.../tests/sarif/oracle/std_string.sarif | 1532 ++++++++++++-----
.../value/domains/cvalue/builtins_malloc.ml | 55 +-
.../terminates_call_options.1.res.oracle | 4 +-
.../terminates_call_options.1.res.oracle | 4 +-
tests/builtins/oracle/realloc.res.oracle | 130 +-
.../builtins/oracle_gauges/realloc.res.oracle | 73 +
tests/builtins/realloc.c | 21 +-
tests/libc/oracle/argz_c.res.oracle | 1 +
tests/libc/oracle/coverage.res.oracle | 2 +-
tests/libc/oracle/fc_libc.1.res.oracle | 38 +
tests/libc/oracle/netdb_c.res.oracle | 1 +
32 files changed, 1454 insertions(+), 546 deletions(-)
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 406321996e6..2f4ef1f4cd8 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -451,6 +451,41 @@ extern void free(void *p);
*/
extern void *realloc(void *ptr, size_t size);
+// reallocarray is non-POSIX (glibc)
+/*@
+ requires freeable: ptr == \null || \freeable(ptr);
+ allocates \result;
+ frees ptr;
+ assigns __fc_heap_status \from indirect:nmemb, indirect:size,
+ __fc_heap_status;
+ assigns \result \from ptr, indirect:nmemb, indirect:size,
+ indirect:__fc_heap_status;
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(nmemb * size);
+ allocates \result;
+ ensures allocation: \fresh(\result, nmemb * size);
+
+ behavior deallocation:
+ assumes nonnull_ptr: ptr != \null;
+ assumes can_allocate: is_allocable(nmemb * size);
+ frees ptr;
+ ensures freed: \allocable(ptr);
+ ensures freeable: \result == \null || \freeable(\result);
+
+ behavior fail:
+ assumes cannot_allocate: !is_allocable(nmemb * size);
+ allocates \nothing;
+ frees \nothing;
+ assigns \result \from indirect:nmemb, indirect:size,
+ indirect:__fc_heap_status;
+ ensures null_result: \result == \null;
+
+ complete behaviors;
+ disjoint behaviors allocation, fail;
+ disjoint behaviors deallocation, fail;
+ */
+extern void *reallocarray(void *ptr, size_t nmemb, size_t size);
/* ISO C: 7.20.4 */
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index 4949156576b..400997fa108 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -816,7 +816,7 @@ void __gen_e_acsl_exit(int status)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "exit";
- __gen_e_acsl_assert_data.line = 473;
+ __gen_e_acsl_assert_data.line = 508;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 835b7da03d0..e1307d5a6ae 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -357,7 +357,7 @@ void __gen_e_acsl_exit(int status)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "exit";
- __gen_e_acsl_assert_data.line = 473;
+ __gen_e_acsl_assert_data.line = 508;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
@@ -379,7 +379,7 @@ void __gen_e_acsl_abort(void)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "abort";
- __gen_e_acsl_assert_data.line = 460;
+ __gen_e_acsl_assert_data.line = 495;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 4328926452d..e2b3df51a3a 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -791,7 +791,7 @@ void __gen_e_acsl_exit(int status)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "exit";
- __gen_e_acsl_assert_data.line = 473;
+ __gen_e_acsl_assert_data.line = 508;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 824fb3503a5..ffcc52912c6 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -331,7 +331,7 @@ void __gen_e_acsl_exit(int status)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "exit";
- __gen_e_acsl_assert_data.line = 473;
+ __gen_e_acsl_assert_data.line = 508;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
@@ -353,7 +353,7 @@ void __gen_e_acsl_abort(void)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "abort";
- __gen_e_acsl_assert_data.line = 460;
+ __gen_e_acsl_assert_data.line = 495;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
index c63be9146f5..79b68330733 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
@@ -17,10 +17,10 @@
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index c9c93a0901d..8cf84baead9 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -50,17 +50,17 @@
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:457: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:492: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:459: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:494: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 930d48cf15e..82dd3516a25 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -45,10 +45,10 @@
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index ace2bc58bc2..2c826d7c60a 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -48,17 +48,17 @@
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:457: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:492: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:459: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:494: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index 65e0a1d6043..f3a95efc32f 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
@@ -776,7 +776,7 @@ void __gen_e_acsl_exit(int status)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "exit";
- __gen_e_acsl_assert_data.line = 473;
+ __gen_e_acsl_assert_data.line = 508;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
__e_acsl_delete_block((void *)(& status));
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
index bad13c318e4..36848cfe9d2 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
@@ -458,7 +458,7 @@ void __gen_e_acsl_exit(int status)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "exit";
- __gen_e_acsl_assert_data.line = 473;
+ __gen_e_acsl_assert_data.line = 508;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
__e_acsl_delete_block((void *)(& status));
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
index 8f495131885..97e90525ac7 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
@@ -38,10 +38,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:1116: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
index 8f495131885..97e90525ac7 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
@@ -38,10 +38,10 @@
[e-acsl] FRAMAC_SHARE/libc/unistd.h:1116: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index 87d5a40951c..8871dc016e5 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -23,10 +23,10 @@
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index f9fa434c611..be3cdf29226 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -270,7 +270,7 @@ void __gen_e_acsl_exit(int status)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "exit";
- __gen_e_acsl_assert_data.line = 473;
+ __gen_e_acsl_assert_data.line = 508;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 3cc0a9f2184..621b839cc08 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -1163,7 +1163,7 @@ void __gen_e_acsl_exit(int status)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "exit";
- __gen_e_acsl_assert_data.line = 473;
+ __gen_e_acsl_assert_data.line = 508;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
@@ -1185,7 +1185,7 @@ void __gen_e_acsl_abort(void)
__gen_e_acsl_assert_data.pred_txt = "\\false";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "abort";
- __gen_e_acsl_assert_data.line = 460;
+ __gen_e_acsl_assert_data.line = 495;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 7cffddb92f5..6a2b2551ba6 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -86,17 +86,17 @@
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:457: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:492: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:459: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:494: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
index 89f3520d16e..bb292590eff 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
@@ -421,7 +421,7 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size)
__gen_e_acsl_assert_data.pred_txt = "\\valid(memptr)";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data.fct = "posix_memalign";
- __gen_e_acsl_assert_data.line = 666;
+ __gen_e_acsl_assert_data.line = 701;
__gen_e_acsl_assert_data.name = "valid_memptr";
__e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -464,7 +464,7 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size)
__gen_e_acsl_assert_data_2.pred_txt = "alignment >= sizeof(void *) &&\n((size_t)alignment & ((size_t)alignment - 1)) == 0";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_2.fct = "posix_memalign";
- __gen_e_acsl_assert_data_2.line = 668;
+ __gen_e_acsl_assert_data_2.line = 703;
__gen_e_acsl_assert_data_2.name = "alignment_is_a_suitable_power_of_two";
__e_acsl_assert(__gen_e_acsl_and,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -484,7 +484,7 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size)
__gen_e_acsl_assert_data_4.pred_txt = "\\result == 0";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_4.fct = "posix_memalign";
- __gen_e_acsl_assert_data_4.line = 680;
+ __gen_e_acsl_assert_data_4.line = 715;
__gen_e_acsl_assert_data_4.name = "allocation/result_zero";
__e_acsl_assert(__retres == 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -508,7 +508,7 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size)
__gen_e_acsl_assert_data_5.pred_txt = "\\result < 0 || \\result > 0";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_5.fct = "posix_memalign";
- __gen_e_acsl_assert_data_5.line = 685;
+ __gen_e_acsl_assert_data_5.line = 720;
__gen_e_acsl_assert_data_5.name = "no_allocation/result_non_zero";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
index d57b82d4e50..9116a25386a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
@@ -2,23 +2,23 @@
[e-acsl] Warning: annotating undefined function `posix_memalign':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:700: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:710: Warning:
E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:682: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:717: Warning:
E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:700: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:700: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:679: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:714: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:680: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:715: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
index 2af473bdba2..6a3a17e2dfa 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
@@ -57,7 +57,7 @@ char *__gen_e_acsl_getenv(char const *name)
__gen_e_acsl_assert_data_2.pred_txt = "\\result == \\null || \\valid(\\result)";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_2.fct = "getenv";
- __gen_e_acsl_assert_data_2.line = 488;
+ __gen_e_acsl_assert_data_2.line = 523;
__gen_e_acsl_assert_data_2.name = "null_or_valid_result";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index ce1bedf2c98..7782e4d7510 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -2,25 +2,25 @@
[e-acsl] Warning: annotating undefined function `getenv':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:486: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:521: Warning:
E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:485: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:520: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning:
function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown.
[eva:alarm] t_getenv.c:13: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 082afbda187..874f9d2005c 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -4400,9 +4400,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 481,
+ "startLine": 516,
"startColumn": 12,
- "endLine": 481,
+ "endLine": 516,
"endColumn": 17,
"byteLength": 5
}
@@ -4423,9 +4423,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 479,
+ "startLine": 514,
"startColumn": 28,
- "endLine": 479,
+ "endLine": 514,
"endColumn": 34,
"byteLength": 6
}
@@ -4446,9 +4446,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 481,
+ "startLine": 516,
"startColumn": 12,
- "endLine": 481,
+ "endLine": 516,
"endColumn": 17,
"byteLength": 5
}
@@ -4469,9 +4469,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 462,
+ "startLine": 497,
"startColumn": 12,
- "endLine": 462,
+ "endLine": 497,
"endColumn": 17,
"byteLength": 5
}
@@ -4492,9 +4492,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 459,
+ "startLine": 494,
"startColumn": 16,
- "endLine": 459,
+ "endLine": 494,
"endColumn": 33,
"byteLength": 17
}
@@ -4515,9 +4515,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 460,
+ "startLine": 495,
"startColumn": 28,
- "endLine": 460,
+ "endLine": 495,
"endColumn": 34,
"byteLength": 6
}
@@ -4538,9 +4538,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 458,
+ "startLine": 493,
"startColumn": 10,
- "endLine": 458,
+ "endLine": 493,
"endColumn": 22,
"byteLength": 12
}
@@ -4563,9 +4563,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 458,
+ "startLine": 493,
"startColumn": 10,
- "endLine": 458,
+ "endLine": 493,
"endColumn": 22,
"byteLength": 12
}
@@ -4586,9 +4586,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 575,
+ "startLine": 610,
"startColumn": 11,
- "endLine": 575,
+ "endLine": 610,
"endColumn": 14,
"byteLength": 3
}
@@ -4609,9 +4609,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 575,
+ "startLine": 610,
"startColumn": 11,
- "endLine": 575,
+ "endLine": 610,
"endColumn": 14,
"byteLength": 3
}
@@ -4632,9 +4632,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 575,
+ "startLine": 610,
"startColumn": 11,
- "endLine": 575,
+ "endLine": 610,
"endColumn": 14,
"byteLength": 3
}
@@ -4655,9 +4655,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 564,
+ "startLine": 599,
"startColumn": 30,
- "endLine": 564,
+ "endLine": 599,
"endColumn": 51,
"byteLength": 21
}
@@ -4678,9 +4678,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 567,
+ "startLine": 602,
"startColumn": 22,
- "endLine": 567,
+ "endLine": 602,
"endColumn": 27,
"byteLength": 5
}
@@ -4701,9 +4701,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 570,
+ "startLine": 605,
"startColumn": 25,
- "endLine": 570,
+ "endLine": 605,
"endColumn": 31,
"byteLength": 6
}
@@ -4724,9 +4724,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 568,
+ "startLine": 603,
"startColumn": 29,
- "endLine": 568,
+ "endLine": 603,
"endColumn": 42,
"byteLength": 13
}
@@ -4747,9 +4747,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 571,
+ "startLine": 606,
"startColumn": 25,
- "endLine": 571,
+ "endLine": 606,
"endColumn": 37,
"byteLength": 12
}
@@ -4770,9 +4770,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 575,
+ "startLine": 610,
"startColumn": 11,
- "endLine": 575,
+ "endLine": 610,
"endColumn": 14,
"byteLength": 3
}
@@ -4795,9 +4795,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 565,
+ "startLine": 600,
"startColumn": 10,
- "endLine": 565,
+ "endLine": 600,
"endColumn": 17,
"byteLength": 7
}
@@ -4818,9 +4818,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 575,
+ "startLine": 610,
"startColumn": 11,
- "endLine": 575,
+ "endLine": 610,
"endColumn": 14,
"byteLength": 3
}
@@ -4841,9 +4841,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 575,
+ "startLine": 610,
"startColumn": 11,
- "endLine": 575,
+ "endLine": 610,
"endColumn": 14,
"byteLength": 3
}
@@ -4866,9 +4866,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 468,
+ "startLine": 503,
"startColumn": 11,
- "endLine": 468,
+ "endLine": 503,
"endColumn": 24,
"byteLength": 13
}
@@ -4889,9 +4889,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 468,
+ "startLine": 503,
"startColumn": 11,
- "endLine": 468,
+ "endLine": 503,
"endColumn": 24,
"byteLength": 13
}
@@ -4914,9 +4914,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 467,
+ "startLine": 502,
"startColumn": 12,
- "endLine": 467,
+ "endLine": 502,
"endColumn": 19,
"byteLength": 7
}
@@ -4937,9 +4937,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 465,
+ "startLine": 500,
"startColumn": 11,
- "endLine": 465,
+ "endLine": 500,
"endColumn": 17,
"byteLength": 6
}
@@ -4960,9 +4960,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 465,
+ "startLine": 500,
"startColumn": 11,
- "endLine": 465,
+ "endLine": 500,
"endColumn": 17,
"byteLength": 6
}
@@ -4985,9 +4985,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 464,
+ "startLine": 499,
"startColumn": 12,
- "endLine": 464,
+ "endLine": 499,
"endColumn": 19,
"byteLength": 7
}
@@ -5384,9 +5384,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 547,
+ "startLine": 582,
"startColumn": 12,
- "endLine": 547,
+ "endLine": 582,
"endColumn": 13,
"byteLength": 1
}
@@ -5407,9 +5407,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 540,
+ "startLine": 575,
"startColumn": 34,
- "endLine": 540,
+ "endLine": 575,
"endColumn": 57,
"byteLength": 23
}
@@ -5430,9 +5430,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 544,
+ "startLine": 579,
"startColumn": 34,
- "endLine": 545,
+ "endLine": 580,
"endColumn": 76,
"byteLength": 96
}
@@ -5453,9 +5453,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 547,
+ "startLine": 582,
"startColumn": 12,
- "endLine": 547,
+ "endLine": 582,
"endColumn": 13,
"byteLength": 1
}
@@ -5478,9 +5478,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 541,
+ "startLine": 576,
"startColumn": 10,
- "endLine": 541,
+ "endLine": 576,
"endColumn": 17,
"byteLength": 7
}
@@ -6063,9 +6063,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 606,
+ "startLine": 641,
"startColumn": 13,
- "endLine": 606,
+ "endLine": 641,
"endColumn": 16,
"byteLength": 3
}
@@ -6086,9 +6086,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 606,
+ "startLine": 641,
"startColumn": 13,
- "endLine": 606,
+ "endLine": 641,
"endColumn": 16,
"byteLength": 3
}
@@ -6111,9 +6111,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 605,
+ "startLine": 640,
"startColumn": 12,
- "endLine": 605,
+ "endLine": 640,
"endColumn": 19,
"byteLength": 7
}
@@ -6420,9 +6420,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 475,
+ "startLine": 510,
"startColumn": 12,
- "endLine": 475,
+ "endLine": 510,
"endColumn": 16,
"byteLength": 4
}
@@ -6443,9 +6443,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 472,
+ "startLine": 507,
"startColumn": 16,
- "endLine": 472,
+ "endLine": 507,
"endColumn": 38,
"byteLength": 22
}
@@ -6466,9 +6466,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 473,
+ "startLine": 508,
"startColumn": 28,
- "endLine": 473,
+ "endLine": 508,
"endColumn": 34,
"byteLength": 6
}
@@ -6489,9 +6489,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 471,
+ "startLine": 506,
"startColumn": 10,
- "endLine": 471,
+ "endLine": 506,
"endColumn": 22,
"byteLength": 12
}
@@ -6514,9 +6514,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 471,
+ "startLine": 506,
"startColumn": 10,
- "endLine": 471,
+ "endLine": 506,
"endColumn": 22,
"byteLength": 12
}
@@ -6909,9 +6909,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 490,
+ "startLine": 525,
"startColumn": 12,
- "endLine": 490,
+ "endLine": 525,
"endColumn": 13,
"byteLength": 1
}
@@ -6932,9 +6932,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 486,
+ "startLine": 521,
"startColumn": 23,
- "endLine": 486,
+ "endLine": 521,
"endColumn": 46,
"byteLength": 23
}
@@ -6955,9 +6955,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 488,
+ "startLine": 523,
"startColumn": 32,
- "endLine": 488,
+ "endLine": 523,
"endColumn": 67,
"byteLength": 35
}
@@ -6978,9 +6978,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 490,
+ "startLine": 525,
"startColumn": 12,
- "endLine": 490,
+ "endLine": 525,
"endColumn": 13,
"byteLength": 1
}
@@ -7003,9 +7003,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 487,
+ "startLine": 522,
"startColumn": 10,
- "endLine": 487,
+ "endLine": 522,
"endColumn": 17,
"byteLength": 7
}
@@ -7169,9 +7169,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 589,
+ "startLine": 624,
"startColumn": 16,
- "endLine": 589,
+ "endLine": 624,
"endColumn": 20,
"byteLength": 4
}
@@ -7192,9 +7192,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 589,
+ "startLine": 624,
"startColumn": 16,
- "endLine": 589,
+ "endLine": 624,
"endColumn": 20,
"byteLength": 4
}
@@ -7215,9 +7215,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 589,
+ "startLine": 624,
"startColumn": 16,
- "endLine": 589,
+ "endLine": 624,
"endColumn": 20,
"byteLength": 4
}
@@ -7238,9 +7238,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 578,
+ "startLine": 613,
"startColumn": 30,
- "endLine": 578,
+ "endLine": 613,
"endColumn": 61,
"byteLength": 31
}
@@ -7261,9 +7261,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 581,
+ "startLine": 616,
"startColumn": 22,
- "endLine": 581,
+ "endLine": 616,
"endColumn": 27,
"byteLength": 5
}
@@ -7284,9 +7284,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 584,
+ "startLine": 619,
"startColumn": 25,
- "endLine": 584,
+ "endLine": 619,
"endColumn": 31,
"byteLength": 6
}
@@ -7307,9 +7307,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 582,
+ "startLine": 617,
"startColumn": 29,
- "endLine": 582,
+ "endLine": 617,
"endColumn": 42,
"byteLength": 13
}
@@ -7330,9 +7330,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 585,
+ "startLine": 620,
"startColumn": 25,
- "endLine": 585,
+ "endLine": 620,
"endColumn": 37,
"byteLength": 12
}
@@ -7353,9 +7353,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 589,
+ "startLine": 624,
"startColumn": 16,
- "endLine": 589,
+ "endLine": 624,
"endColumn": 20,
"byteLength": 4
}
@@ -7378,9 +7378,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 579,
+ "startLine": 614,
"startColumn": 10,
- "endLine": 579,
+ "endLine": 614,
"endColumn": 17,
"byteLength": 7
}
@@ -7401,9 +7401,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 589,
+ "startLine": 624,
"startColumn": 16,
- "endLine": 589,
+ "endLine": 624,
"endColumn": 20,
"byteLength": 4
}
@@ -7424,9 +7424,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 589,
+ "startLine": 624,
"startColumn": 16,
- "endLine": 589,
+ "endLine": 624,
"endColumn": 20,
"byteLength": 4
}
@@ -7568,9 +7568,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 608,
+ "startLine": 643,
"startColumn": 14,
- "endLine": 608,
+ "endLine": 643,
"endColumn": 18,
"byteLength": 4
}
@@ -7591,9 +7591,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 608,
+ "startLine": 643,
"startColumn": 14,
- "endLine": 608,
+ "endLine": 643,
"endColumn": 18,
"byteLength": 4
}
@@ -7616,9 +7616,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 607,
+ "startLine": 642,
"startColumn": 12,
- "endLine": 607,
+ "endLine": 642,
"endColumn": 19,
"byteLength": 7
}
@@ -7639,9 +7639,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 603,
+ "startLine": 638,
"startColumn": 21,
- "endLine": 603,
+ "endLine": 638,
"endColumn": 26,
"byteLength": 5
}
@@ -7662,9 +7662,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 603,
+ "startLine": 638,
"startColumn": 21,
- "endLine": 603,
+ "endLine": 638,
"endColumn": 26,
"byteLength": 5
}
@@ -7685,9 +7685,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 603,
+ "startLine": 638,
"startColumn": 21,
- "endLine": 603,
+ "endLine": 638,
"endColumn": 26,
"byteLength": 5
}
@@ -7708,9 +7708,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 592,
+ "startLine": 627,
"startColumn": 30,
- "endLine": 592,
+ "endLine": 627,
"endColumn": 63,
"byteLength": 33
}
@@ -7731,9 +7731,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 595,
+ "startLine": 630,
"startColumn": 22,
- "endLine": 595,
+ "endLine": 630,
"endColumn": 27,
"byteLength": 5
}
@@ -7754,9 +7754,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 598,
+ "startLine": 633,
"startColumn": 25,
- "endLine": 598,
+ "endLine": 633,
"endColumn": 31,
"byteLength": 6
}
@@ -7777,9 +7777,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 596,
+ "startLine": 631,
"startColumn": 29,
- "endLine": 596,
+ "endLine": 631,
"endColumn": 42,
"byteLength": 13
}
@@ -7800,9 +7800,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 599,
+ "startLine": 634,
"startColumn": 25,
- "endLine": 599,
+ "endLine": 634,
"endColumn": 37,
"byteLength": 12
}
@@ -7823,9 +7823,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 603,
+ "startLine": 638,
"startColumn": 21,
- "endLine": 603,
+ "endLine": 638,
"endColumn": 26,
"byteLength": 5
}
@@ -7848,9 +7848,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 593,
+ "startLine": 628,
"startColumn": 10,
- "endLine": 593,
+ "endLine": 628,
"endColumn": 17,
"byteLength": 7
}
@@ -7871,9 +7871,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 603,
+ "startLine": 638,
"startColumn": 21,
- "endLine": 603,
+ "endLine": 638,
"endColumn": 26,
"byteLength": 5
}
@@ -7894,9 +7894,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 603,
+ "startLine": 638,
"startColumn": 21,
- "endLine": 603,
+ "endLine": 638,
"endColumn": 26,
"byteLength": 5
}
@@ -7917,9 +7917,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 610,
+ "startLine": 645,
"startColumn": 15,
- "endLine": 610,
+ "endLine": 645,
"endColumn": 20,
"byteLength": 5
}
@@ -7940,9 +7940,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 610,
+ "startLine": 645,
"startColumn": 15,
- "endLine": 610,
+ "endLine": 645,
"endColumn": 20,
"byteLength": 5
}
@@ -7965,9 +7965,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 609,
+ "startLine": 644,
"startColumn": 12,
- "endLine": 609,
+ "endLine": 644,
"endColumn": 19,
"byteLength": 7
}
@@ -8580,9 +8580,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 618,
+ "startLine": 653,
"startColumn": 11,
- "endLine": 618,
+ "endLine": 653,
"endColumn": 16,
"byteLength": 5
}
@@ -8603,9 +8603,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 616,
+ "startLine": 651,
"startColumn": 12,
- "endLine": 616,
+ "endLine": 651,
"endColumn": 19,
"byteLength": 7
}
@@ -8628,9 +8628,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 616,
+ "startLine": 651,
"startColumn": 12,
- "endLine": 616,
+ "endLine": 651,
"endColumn": 19,
"byteLength": 7
}
@@ -8653,9 +8653,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 616,
+ "startLine": 651,
"startColumn": 21,
- "endLine": 616,
+ "endLine": 651,
"endColumn": 37,
"byteLength": 16
}
@@ -8676,9 +8676,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 650,
+ "startLine": 685,
"startColumn": 14,
- "endLine": 650,
+ "endLine": 685,
"endColumn": 22,
"byteLength": 8
}
@@ -8699,9 +8699,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 646,
+ "startLine": 681,
"startColumn": 23,
- "endLine": 646,
+ "endLine": 681,
"endColumn": 42,
"byteLength": 19
}
@@ -8722,9 +8722,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 647,
+ "startLine": 682,
"startColumn": 10,
- "endLine": 647,
+ "endLine": 682,
"endColumn": 17,
"byteLength": 7
}
@@ -8747,9 +8747,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 647,
+ "startLine": 682,
"startColumn": 10,
- "endLine": 647,
+ "endLine": 682,
"endColumn": 17,
"byteLength": 7
}
@@ -8773,9 +8773,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 648,
+ "startLine": 683,
"startColumn": 10,
- "endLine": 648,
+ "endLine": 683,
"endColumn": 24,
"byteLength": 14
}
@@ -8796,9 +8796,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 630,
+ "startLine": 665,
"startColumn": 11,
- "endLine": 630,
+ "endLine": 665,
"endColumn": 17,
"byteLength": 6
}
@@ -8819,9 +8819,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 623,
+ "startLine": 658,
"startColumn": 23,
- "endLine": 623,
+ "endLine": 658,
"endColumn": 41,
"byteLength": 18
}
@@ -8842,9 +8842,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 628,
+ "startLine": 663,
"startColumn": 26,
- "endLine": 628,
+ "endLine": 663,
"endColumn": 38,
"byteLength": 12
}
@@ -8865,9 +8865,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 624,
+ "startLine": 659,
"startColumn": 10,
- "endLine": 624,
+ "endLine": 659,
"endColumn": 17,
"byteLength": 7
}
@@ -8890,9 +8890,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 624,
+ "startLine": 659,
"startColumn": 10,
- "endLine": 624,
+ "endLine": 659,
"endColumn": 17,
"byteLength": 7
}
@@ -8916,9 +8916,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 626,
+ "startLine": 661,
"startColumn": 10,
- "endLine": 626,
+ "endLine": 661,
"endColumn": 29,
"byteLength": 19
}
@@ -8942,9 +8942,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 626,
+ "startLine": 661,
"startColumn": 31,
- "endLine": 626,
+ "endLine": 661,
"endColumn": 48,
"byteLength": 17
}
@@ -11276,9 +11276,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 701,
+ "startLine": 736,
"startColumn": 11,
- "endLine": 701,
+ "endLine": 736,
"endColumn": 18,
"byteLength": 7
}
@@ -11299,9 +11299,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 694,
+ "startLine": 729,
"startColumn": 27,
- "endLine": 694,
+ "endLine": 729,
"endColumn": 48,
"byteLength": 21
}
@@ -11322,9 +11322,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 695,
+ "startLine": 730,
"startColumn": 25,
- "endLine": 695,
+ "endLine": 730,
"endColumn": 45,
"byteLength": 20
}
@@ -11345,9 +11345,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 698,
+ "startLine": 733,
"startColumn": 36,
- "endLine": 699,
+ "endLine": 734,
"endColumn": 53,
"byteLength": 70
}
@@ -11368,9 +11368,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 696,
+ "startLine": 731,
"startColumn": 10,
- "endLine": 696,
+ "endLine": 731,
"endColumn": 22,
"byteLength": 12
}
@@ -11394,9 +11394,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 696,
+ "startLine": 731,
"startColumn": 10,
- "endLine": 696,
+ "endLine": 731,
"endColumn": 22,
"byteLength": 12
}
@@ -11419,9 +11419,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 697,
+ "startLine": 732,
"startColumn": 10,
- "endLine": 697,
+ "endLine": 732,
"endColumn": 17,
"byteLength": 7
}
@@ -11442,9 +11442,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 714,
+ "startLine": 749,
"startColumn": 11,
- "endLine": 714,
+ "endLine": 749,
"endColumn": 19,
"byteLength": 8
}
@@ -11465,9 +11465,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 706,
+ "startLine": 741,
"startColumn": 27,
- "endLine": 706,
+ "endLine": 741,
"endColumn": 48,
"byteLength": 21
}
@@ -11488,9 +11488,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 707,
+ "startLine": 742,
"startColumn": 25,
- "endLine": 707,
+ "endLine": 742,
"endColumn": 57,
"byteLength": 32
}
@@ -11511,9 +11511,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 708,
+ "startLine": 743,
"startColumn": 35,
- "endLine": 708,
+ "endLine": 743,
"endColumn": 49,
"byteLength": 14
}
@@ -11534,9 +11534,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 711,
+ "startLine": 746,
"startColumn": 36,
- "endLine": 712,
+ "endLine": 747,
"endColumn": 53,
"byteLength": 70
}
@@ -11557,9 +11557,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 709,
+ "startLine": 744,
"startColumn": 10,
- "endLine": 709,
+ "endLine": 744,
"endColumn": 22,
"byteLength": 12
}
@@ -11583,9 +11583,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 709,
+ "startLine": 744,
"startColumn": 10,
- "endLine": 709,
+ "endLine": 744,
"endColumn": 22,
"byteLength": 12
}
@@ -11608,9 +11608,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 710,
+ "startLine": 745,
"startColumn": 10,
- "endLine": 710,
+ "endLine": 745,
"endColumn": 17,
"byteLength": 7
}
@@ -11919,9 +11919,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 689,
+ "startLine": 724,
"startColumn": 11,
- "endLine": 689,
+ "endLine": 724,
"endColumn": 25,
"byteLength": 14
}
@@ -11944,9 +11944,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 689,
+ "startLine": 724,
"startColumn": 11,
- "endLine": 689,
+ "endLine": 724,
"endColumn": 25,
"byteLength": 14
}
@@ -11969,9 +11969,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 689,
+ "startLine": 724,
"startColumn": 11,
- "endLine": 689,
+ "endLine": 724,
"endColumn": 25,
"byteLength": 14
}
@@ -11992,9 +11992,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 666,
+ "startLine": 701,
"startColumn": 25,
- "endLine": 666,
+ "endLine": 701,
"endColumn": 39,
"byteLength": 14
}
@@ -12015,9 +12015,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 668,
+ "startLine": 703,
"startColumn": 4,
- "endLine": 669,
+ "endLine": 704,
"endColumn": 54,
"byteLength": 84
}
@@ -12038,9 +12038,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 675,
+ "startLine": 710,
"startColumn": 26,
- "endLine": 675,
+ "endLine": 710,
"endColumn": 44,
"byteLength": 18
}
@@ -12061,9 +12061,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 682,
+ "startLine": 717,
"startColumn": 29,
- "endLine": 682,
+ "endLine": 717,
"endColumn": 48,
"byteLength": 19
}
@@ -12084,9 +12084,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 679,
+ "startLine": 714,
"startColumn": 24,
- "endLine": 679,
+ "endLine": 714,
"endColumn": 44,
"byteLength": 20
}
@@ -12107,9 +12107,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 680,
+ "startLine": 715,
"startColumn": 25,
- "endLine": 680,
+ "endLine": 715,
"endColumn": 37,
"byteLength": 12
}
@@ -12130,9 +12130,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 685,
+ "startLine": 720,
"startColumn": 29,
- "endLine": 685,
+ "endLine": 720,
"endColumn": 55,
"byteLength": 26
}
@@ -12153,9 +12153,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 676,
+ "startLine": 711,
"startColumn": 12,
- "endLine": 676,
+ "endLine": 711,
"endColumn": 28,
"byteLength": 16
}
@@ -12176,9 +12176,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 671,
+ "startLine": 706,
"startColumn": 10,
- "endLine": 671,
+ "endLine": 706,
"endColumn": 26,
"byteLength": 16
}
@@ -12199,9 +12199,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 689,
+ "startLine": 724,
"startColumn": 11,
- "endLine": 689,
+ "endLine": 724,
"endColumn": 25,
"byteLength": 14
}
@@ -12225,9 +12225,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 676,
+ "startLine": 711,
"startColumn": 12,
- "endLine": 676,
+ "endLine": 711,
"endColumn": 28,
"byteLength": 16
}
@@ -12251,9 +12251,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 677,
+ "startLine": 712,
"startColumn": 12,
- "endLine": 677,
+ "endLine": 712,
"endColumn": 19,
"byteLength": 7
}
@@ -12277,9 +12277,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 671,
+ "startLine": 706,
"startColumn": 10,
- "endLine": 671,
+ "endLine": 706,
"endColumn": 26,
"byteLength": 16
}
@@ -12303,9 +12303,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 672,
+ "startLine": 707,
"startColumn": 10,
- "endLine": 672,
+ "endLine": 707,
"endColumn": 17,
"byteLength": 7
}
@@ -12329,9 +12329,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 683,
+ "startLine": 718,
"startColumn": 12,
- "endLine": 683,
+ "endLine": 718,
"endColumn": 19,
"byteLength": 7
}
@@ -12354,9 +12354,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 670,
+ "startLine": 705,
"startColumn": 12,
- "endLine": 670,
+ "endLine": 705,
"endColumn": 19,
"byteLength": 7
}
@@ -12379,9 +12379,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 689,
+ "startLine": 724,
"startColumn": 11,
- "endLine": 689,
+ "endLine": 724,
"endColumn": 25,
"byteLength": 14
}
@@ -12404,9 +12404,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 689,
+ "startLine": 724,
"startColumn": 11,
- "endLine": 689,
+ "endLine": 724,
"endColumn": 25,
"byteLength": 14
}
@@ -12429,9 +12429,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 689,
+ "startLine": 724,
"startColumn": 11,
- "endLine": 689,
+ "endLine": 724,
"endColumn": 25,
"byteLength": 14
}
@@ -12452,9 +12452,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 497,
+ "startLine": 532,
"startColumn": 11,
- "endLine": 497,
+ "endLine": 532,
"endColumn": 17,
"byteLength": 6
}
@@ -12475,9 +12475,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 493,
+ "startLine": 528,
"startColumn": 25,
- "endLine": 493,
+ "endLine": 528,
"endColumn": 50,
"byteLength": 25
}
@@ -12498,9 +12498,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 494,
+ "startLine": 529,
"startColumn": 10,
- "endLine": 494,
+ "endLine": 529,
"endColumn": 23,
"byteLength": 13
}
@@ -12523,9 +12523,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 494,
+ "startLine": 529,
"startColumn": 10,
- "endLine": 494,
+ "endLine": 529,
"endColumn": 23,
"byteLength": 13
}
@@ -12548,9 +12548,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 495,
+ "startLine": 530,
"startColumn": 10,
- "endLine": 495,
+ "endLine": 530,
"endColumn": 17,
"byteLength": 7
}
@@ -12571,9 +12571,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 558,
+ "startLine": 593,
"startColumn": 12,
- "endLine": 558,
+ "endLine": 593,
"endColumn": 17,
"byteLength": 5
}
@@ -12594,9 +12594,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 553,
+ "startLine": 588,
"startColumn": 34,
- "endLine": 553,
+ "endLine": 588,
"endColumn": 57,
"byteLength": 23
}
@@ -12617,9 +12617,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 554,
+ "startLine": 589,
"startColumn": 10,
- "endLine": 554,
+ "endLine": 589,
"endColumn": 29,
"byteLength": 19
}
@@ -12643,9 +12643,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 554,
+ "startLine": 589,
"startColumn": 10,
- "endLine": 554,
+ "endLine": 589,
"endColumn": 29,
"byteLength": 19
}
@@ -12666,9 +12666,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 521,
+ "startLine": 556,
"startColumn": 12,
- "endLine": 521,
+ "endLine": 556,
"endColumn": 22,
"byteLength": 10
}
@@ -12689,9 +12689,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 519,
+ "startLine": 554,
"startColumn": 28,
- "endLine": 519,
+ "endLine": 554,
"endColumn": 34,
"byteLength": 6
}
@@ -12712,9 +12712,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 521,
+ "startLine": 556,
"startColumn": 12,
- "endLine": 521,
+ "endLine": 556,
"endColumn": 22,
"byteLength": 10
}
@@ -12892,7 +12892,647 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function random." },
+ "message": { "text": "assigns clause in function random." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 281,
+ "startColumn": 16,
+ "endLine": 281,
+ "endColumn": 22,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function random."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 278,
+ "startColumn": 10,
+ "endLine": 278,
+ "endColumn": 17,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior allocation in function realloc." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior deallocation in function realloc." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function realloc." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior fail in function realloc." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "freeable." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 422,
+ "startColumn": 22,
+ "endLine": 422,
+ "endColumn": 52,
+ "byteLength": 30
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "can_allocate." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 429,
+ "startColumn": 27,
+ "endLine": 429,
+ "endColumn": 45,
+ "byteLength": 18
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "nonnull_ptr." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 435,
+ "startColumn": 26,
+ "endLine": 435,
+ "endColumn": 38,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "can_allocate." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 436,
+ "startColumn": 27,
+ "endLine": 436,
+ "endColumn": 45,
+ "byteLength": 18
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "cannot_allocate." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 442,
+ "startColumn": 30,
+ "endLine": 442,
+ "endColumn": 49,
+ "byteLength": 19
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "allocation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 432,
+ "startColumn": 25,
+ "endLine": 432,
+ "endColumn": 45,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "freed." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 438,
+ "startColumn": 20,
+ "endLine": 438,
+ "endColumn": 35,
+ "byteLength": 15
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "freeable." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 439,
+ "startColumn": 23,
+ "endLine": 439,
+ "endColumn": 61,
+ "byteLength": 38
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "null_result." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 446,
+ "startColumn": 26,
+ "endLine": 446,
+ "endColumn": 42,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function realloc." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function realloc." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 425,
+ "startColumn": 11,
+ "endLine": 425,
+ "endColumn": 27,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function realloc." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function realloc."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 431,
+ "startColumn": 13,
+ "endLine": 431,
+ "endColumn": 20,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term __fc_heap_status in function realloc."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 425,
+ "startColumn": 11,
+ "endLine": 425,
+ "endColumn": 27,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function realloc."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 426,
+ "startColumn": 11,
+ "endLine": 426,
+ "endColumn": 18,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function realloc."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 445,
+ "startColumn": 13,
+ "endLine": 445,
+ "endColumn": 20,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "allocates/frees clause in function realloc."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 430,
+ "startColumn": 15,
+ "endLine": 430,
+ "endColumn": 22,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "allocates/frees clause in function realloc."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 437,
+ "startColumn": 11,
+ "endLine": 437,
+ "endColumn": 14,
+ "byteLength": 3
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "allocates/frees clause in function realloc."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 424,
+ "startColumn": 9,
+ "endLine": 424,
+ "endColumn": 12,
+ "byteLength": 3
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "allocates/frees clause in function realloc."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "complete clause in function realloc." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "disjoint clause in function realloc." },
"locations": [
{
"physicalLocation": {
@@ -12901,11 +13541,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 281,
- "startColumn": 16,
- "endLine": 281,
- "endColumn": 22,
- "byteLength": 6
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -12915,9 +13555,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": {
- "text": "from clause of term \\result in function random."
- },
+ "message": { "text": "disjoint clause in function realloc." },
"locations": [
{
"physicalLocation": {
@@ -12926,11 +13564,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 278,
- "startColumn": 10,
- "endLine": 278,
- "endColumn": 17,
- "byteLength": 7
+ "startLine": 452,
+ "startColumn": 12,
+ "endLine": 452,
+ "endColumn": 13,
+ "byteLength": 1
}
}
}
@@ -12940,7 +13578,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior allocation in function realloc." },
+ "message": {
+ "text": "behavior allocation in function reallocarray."
+ },
"locations": [
{
"physicalLocation": {
@@ -12949,9 +13589,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -12963,7 +13603,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior deallocation in function realloc." },
+ "message": {
+ "text": "behavior deallocation in function reallocarray."
+ },
"locations": [
{
"physicalLocation": {
@@ -12972,9 +13614,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -12986,7 +13628,9 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior default! in function realloc." },
+ "message": {
+ "text": "behavior default! in function reallocarray."
+ },
"locations": [
{
"physicalLocation": {
@@ -12995,9 +13639,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -13009,7 +13653,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "behavior fail in function realloc." },
+ "message": { "text": "behavior fail in function reallocarray." },
"locations": [
{
"physicalLocation": {
@@ -13018,9 +13662,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -13041,9 +13685,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 422,
+ "startLine": 456,
"startColumn": 22,
- "endLine": 422,
+ "endLine": 456,
"endColumn": 52,
"byteLength": 30
}
@@ -13064,11 +13708,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 429,
+ "startLine": 465,
"startColumn": 27,
- "endLine": 429,
- "endColumn": 45,
- "byteLength": 18
+ "endLine": 465,
+ "endColumn": 53,
+ "byteLength": 26
}
}
}
@@ -13087,9 +13731,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 435,
+ "startLine": 470,
"startColumn": 26,
- "endLine": 435,
+ "endLine": 470,
"endColumn": 38,
"byteLength": 12
}
@@ -13110,11 +13754,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 436,
+ "startLine": 471,
"startColumn": 27,
- "endLine": 436,
- "endColumn": 45,
- "byteLength": 18
+ "endLine": 471,
+ "endColumn": 53,
+ "byteLength": 26
}
}
}
@@ -13133,11 +13777,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 442,
+ "startLine": 477,
"startColumn": 30,
- "endLine": 442,
- "endColumn": 49,
- "byteLength": 19
+ "endLine": 477,
+ "endColumn": 57,
+ "byteLength": 27
}
}
}
@@ -13156,11 +13800,11 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 432,
+ "startLine": 467,
"startColumn": 25,
- "endLine": 432,
- "endColumn": 45,
- "byteLength": 20
+ "endLine": 467,
+ "endColumn": 54,
+ "byteLength": 29
}
}
}
@@ -13179,9 +13823,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 438,
+ "startLine": 473,
"startColumn": 20,
- "endLine": 438,
+ "endLine": 473,
"endColumn": 35,
"byteLength": 15
}
@@ -13202,9 +13846,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 439,
+ "startLine": 474,
"startColumn": 23,
- "endLine": 439,
+ "endLine": 474,
"endColumn": 61,
"byteLength": 38
}
@@ -13225,9 +13869,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 446,
+ "startLine": 482,
"startColumn": 26,
- "endLine": 446,
+ "endLine": 482,
"endColumn": 42,
"byteLength": 16
}
@@ -13239,30 +13883,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function realloc." },
- "locations": [
- {
- "physicalLocation": {
- "artifactLocation": {
- "uri": "libc/stdlib.h",
- "uriBaseId": "FRAMAC_SHARE"
- },
- "region": {
- "startLine": 452,
- "startColumn": 12,
- "endLine": 452,
- "endColumn": 13,
- "byteLength": 1
- }
- }
- }
- ]
- },
- {
- "ruleId": "user-spec",
- "kind": "pass",
- "level": "none",
- "message": { "text": "assigns clause in function realloc." },
+ "message": { "text": "assigns clause in function reallocarray." },
"locations": [
{
"physicalLocation": {
@@ -13271,9 +13892,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 425,
+ "startLine": 459,
"startColumn": 11,
- "endLine": 425,
+ "endLine": 459,
"endColumn": 27,
"byteLength": 16
}
@@ -13285,7 +13906,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "assigns clause in function realloc." },
+ "message": { "text": "assigns clause in function reallocarray." },
"locations": [
{
"physicalLocation": {
@@ -13294,9 +13915,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -13304,38 +13925,13 @@
}
]
},
- {
- "ruleId": "user-spec",
- "kind": "pass",
- "level": "none",
- "message": {
- "text": "from clause of term \\result in function realloc."
- },
- "locations": [
- {
- "physicalLocation": {
- "artifactLocation": {
- "uri": "libc/stdlib.h",
- "uriBaseId": "FRAMAC_SHARE"
- },
- "region": {
- "startLine": 431,
- "startColumn": 13,
- "endLine": 431,
- "endColumn": 20,
- "byteLength": 7
- }
- }
- }
- ]
- },
{
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
"message": {
"text":
- "from clause of term __fc_heap_status in function realloc."
+ "from clause of term __fc_heap_status in function reallocarray."
},
"locations": [
{
@@ -13345,9 +13941,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 425,
+ "startLine": 459,
"startColumn": 11,
- "endLine": 425,
+ "endLine": 459,
"endColumn": 27,
"byteLength": 16
}
@@ -13360,7 +13956,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function realloc."
+ "text": "from clause of term \\result in function reallocarray."
},
"locations": [
{
@@ -13370,9 +13966,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 426,
+ "startLine": 461,
"startColumn": 11,
- "endLine": 426,
+ "endLine": 461,
"endColumn": 18,
"byteLength": 7
}
@@ -13385,7 +13981,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "from clause of term \\result in function realloc."
+ "text": "from clause of term \\result in function reallocarray."
},
"locations": [
{
@@ -13395,9 +13991,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 445,
+ "startLine": 480,
"startColumn": 13,
- "endLine": 445,
+ "endLine": 480,
"endColumn": 20,
"byteLength": 7
}
@@ -13410,7 +14006,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "allocates/frees clause in function realloc."
+ "text": "allocates/frees clause in function reallocarray."
},
"locations": [
{
@@ -13420,9 +14016,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 430,
+ "startLine": 466,
"startColumn": 15,
- "endLine": 430,
+ "endLine": 466,
"endColumn": 22,
"byteLength": 7
}
@@ -13435,7 +14031,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "allocates/frees clause in function realloc."
+ "text": "allocates/frees clause in function reallocarray."
},
"locations": [
{
@@ -13445,9 +14041,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 437,
+ "startLine": 472,
"startColumn": 11,
- "endLine": 437,
+ "endLine": 472,
"endColumn": 14,
"byteLength": 3
}
@@ -13460,7 +14056,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "allocates/frees clause in function realloc."
+ "text": "allocates/frees clause in function reallocarray."
},
"locations": [
{
@@ -13470,9 +14066,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 424,
+ "startLine": 458,
"startColumn": 9,
- "endLine": 424,
+ "endLine": 458,
"endColumn": 12,
"byteLength": 3
}
@@ -13485,7 +14081,7 @@
"kind": "pass",
"level": "none",
"message": {
- "text": "allocates/frees clause in function realloc."
+ "text": "allocates/frees clause in function reallocarray."
},
"locations": [
{
@@ -13495,9 +14091,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -13509,7 +14105,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "complete clause in function realloc." },
+ "message": { "text": "complete clause in function reallocarray." },
"locations": [
{
"physicalLocation": {
@@ -13518,9 +14114,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -13532,7 +14128,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "disjoint clause in function realloc." },
+ "message": { "text": "disjoint clause in function reallocarray." },
"locations": [
{
"physicalLocation": {
@@ -13541,9 +14137,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -13555,7 +14151,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "disjoint clause in function realloc." },
+ "message": { "text": "disjoint clause in function reallocarray." },
"locations": [
{
"physicalLocation": {
@@ -13564,9 +14160,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 452,
+ "startLine": 488,
"startColumn": 12,
- "endLine": 452,
+ "endLine": 488,
"endColumn": 13,
"byteLength": 1
}
@@ -13779,9 +14375,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 507,
+ "startLine": 542,
"startColumn": 11,
- "endLine": 507,
+ "endLine": 542,
"endColumn": 17,
"byteLength": 6
}
@@ -13802,9 +14398,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 500,
+ "startLine": 535,
"startColumn": 23,
- "endLine": 500,
+ "endLine": 535,
"endColumn": 46,
"byteLength": 23
}
@@ -13825,9 +14421,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 501,
+ "startLine": 536,
"startColumn": 24,
- "endLine": 501,
+ "endLine": 536,
"endColumn": 48,
"byteLength": 24
}
@@ -13848,9 +14444,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 505,
+ "startLine": 540,
"startColumn": 30,
- "endLine": 505,
+ "endLine": 540,
"endColumn": 59,
"byteLength": 29
}
@@ -13871,9 +14467,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 502,
+ "startLine": 537,
"startColumn": 10,
- "endLine": 502,
+ "endLine": 537,
"endColumn": 17,
"byteLength": 7
}
@@ -13896,9 +14492,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 502,
+ "startLine": 537,
"startColumn": 10,
- "endLine": 502,
+ "endLine": 537,
"endColumn": 17,
"byteLength": 7
}
@@ -13921,9 +14517,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 502,
+ "startLine": 537,
"startColumn": 19,
- "endLine": 502,
+ "endLine": 537,
"endColumn": 32,
"byteLength": 13
}
@@ -25342,9 +25938,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 528,
+ "startLine": 563,
"startColumn": 11,
- "endLine": 528,
+ "endLine": 563,
"endColumn": 17,
"byteLength": 6
}
@@ -25365,9 +25961,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 525,
+ "startLine": 560,
"startColumn": 5,
- "endLine": 525,
+ "endLine": 560,
"endColumn": 51,
"byteLength": 46
}
@@ -25388,9 +25984,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 528,
+ "startLine": 563,
"startColumn": 11,
- "endLine": 528,
+ "endLine": 563,
"endColumn": 17,
"byteLength": 6
}
@@ -25413,9 +26009,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 526,
+ "startLine": 561,
"startColumn": 10,
- "endLine": 526,
+ "endLine": 561,
"endColumn": 17,
"byteLength": 7
}
@@ -25436,9 +26032,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 515,
+ "startLine": 550,
"startColumn": 11,
- "endLine": 515,
+ "endLine": 550,
"endColumn": 19,
"byteLength": 8
}
@@ -25459,9 +26055,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 510,
+ "startLine": 545,
"startColumn": 23,
- "endLine": 510,
+ "endLine": 545,
"endColumn": 46,
"byteLength": 23
}
@@ -25482,9 +26078,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 513,
+ "startLine": 548,
"startColumn": 30,
- "endLine": 513,
+ "endLine": 548,
"endColumn": 59,
"byteLength": 29
}
@@ -25505,9 +26101,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 511,
+ "startLine": 546,
"startColumn": 10,
- "endLine": 511,
+ "endLine": 546,
"endColumn": 17,
"byteLength": 7
}
@@ -25530,9 +26126,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 511,
+ "startLine": 546,
"startColumn": 10,
- "endLine": 511,
+ "endLine": 546,
"endColumn": 17,
"byteLength": 7
}
@@ -25556,9 +26152,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 511,
+ "startLine": 546,
"startColumn": 19,
- "endLine": 511,
+ "endLine": 546,
"endColumn": 32,
"byteLength": 13
}
@@ -25579,9 +26175,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 659,
+ "startLine": 694,
"startColumn": 14,
- "endLine": 659,
+ "endLine": 694,
"endColumn": 22,
"byteLength": 8
}
@@ -25602,9 +26198,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 655,
+ "startLine": 690,
"startColumn": 23,
- "endLine": 655,
+ "endLine": 690,
"endColumn": 42,
"byteLength": 19
}
@@ -25625,9 +26221,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 656,
+ "startLine": 691,
"startColumn": 10,
- "endLine": 656,
+ "endLine": 691,
"endColumn": 17,
"byteLength": 7
}
@@ -25650,9 +26246,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 656,
+ "startLine": 691,
"startColumn": 10,
- "endLine": 656,
+ "endLine": 691,
"endColumn": 17,
"byteLength": 7
}
@@ -25676,9 +26272,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 657,
+ "startLine": 692,
"startColumn": 10,
- "endLine": 657,
+ "endLine": 692,
"endColumn": 21,
"byteLength": 11
}
@@ -25699,9 +26295,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 641,
+ "startLine": 676,
"startColumn": 11,
- "endLine": 641,
+ "endLine": 676,
"endColumn": 17,
"byteLength": 6
}
@@ -25722,9 +26318,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 638,
+ "startLine": 673,
"startColumn": 10,
- "endLine": 638,
+ "endLine": 673,
"endColumn": 17,
"byteLength": 7
}
@@ -25747,9 +26343,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 638,
+ "startLine": 673,
"startColumn": 10,
- "endLine": 638,
+ "endLine": 673,
"endColumn": 17,
"byteLength": 7
}
@@ -25772,9 +26368,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 639,
+ "startLine": 674,
"startColumn": 10,
- "endLine": 639,
+ "endLine": 674,
"endColumn": 17,
"byteLength": 7
}
@@ -25798,9 +26394,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 639,
+ "startLine": 674,
"startColumn": 19,
- "endLine": 639,
+ "endLine": 674,
"endColumn": 36,
"byteLength": 17
}
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 33d1cae23d6..e63d26c35de 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -817,12 +817,7 @@ let choose_bases_reallocation () =
| By_stack -> realloc_alloc_copy Weak
| Imprecise -> realloc_imprecise_weakest
-let realloc_builtin state args =
- let ptr, size =
- match args with
- | [ (_, ptr); (_, size) ] -> ptr, size
- | _ -> raise (Builtins.Invalid_nb_of_args 2)
- in
+let realloc_builtin_aux state ptr size =
let bases, card_ok, null = resolve_bases_to_free ptr in
if card_ok > 0 then
let realloc = choose_bases_reallocation () in
@@ -839,12 +834,60 @@ let realloc_builtin state args =
let c_clobbered = Base.SetLattice.bottom in
Builtins.Full { c_values = []; c_clobbered; c_from = None; }
+let realloc_builtin state args =
+ let ptr, size =
+ match args with
+ | [ (_, ptr); (_, size) ] -> ptr, size
+ | _ -> raise (Builtins.Invalid_nb_of_args 2)
+ in
+ realloc_builtin_aux state ptr size
+
let () =
let name = "Frama_C_realloc" in
let replace = "realloc" in
let typ () = Cil.(voidPtrType, [voidPtrType; theMachine.typeOfSizeOf]) in
Builtins.register_builtin ~replace name NoCacheCallers realloc_builtin ~typ
+let reallocarray_builtin state args =
+ let ptr, nmemb, sizev =
+ match args with
+ | [ (_, ptr); (_, nmemb); (_, sizev) ] -> ptr, nmemb, sizev
+ | _ -> raise (Builtins.Invalid_nb_of_args 3)
+ in
+ let size = Cvalue.V.mul nmemb sizev in
+ let size_ok = alloc_size_ok size in
+ if size_ok <> Alarmset.True then
+ Eva_utils.warning_once_current
+ "reallocarray out of bounds: assert(nmemb * size <= SIZE_MAX)";
+ if size_ok = Alarmset.False (* size always overflows *)
+ then
+ let c_values = [Some Cvalue.V.singleton_zero, state] in
+ let c_clobbered = Base.SetLattice.bottom in
+ Builtins.Full { c_values; c_clobbered; c_from = None; }
+ else
+ let valid_size =
+ Cvalue.V.narrow (Cvalue.V.inject_ival (zero_to_max_bytes ())) size
+ in
+ let res = realloc_builtin_aux state ptr valid_size in
+ if size_ok = Alarmset.Unknown then
+ (* include failure case among possible results *)
+ match res with
+ | Builtins.Full cr ->
+ let c_values = (Some Cvalue.V.singleton_zero, state) :: cr.c_values in
+ Builtins.Full { cr with c_values }
+ | _ -> assert false (* realloc_builtin_aux always returns Full *)
+ else res
+
+let () =
+ let name = "Frama_C_reallocarray" in
+ let replace = "reallocarray" in
+ let typ () =
+ Cil.(voidPtrType,
+ [voidPtrType; theMachine.typeOfSizeOf; theMachine.typeOfSizeOf])
+ in
+ Builtins.register_builtin
+ ~replace name NoCacheCallers reallocarray_builtin ~typ
+
(* ----------------------------- Leak detection ----------------------------- *)
(* Experimental, not to be released, leak detection built-in. *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
index c34c3155dc5..917497f430e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
@@ -11,9 +11,9 @@
Missing terminates clause for declaration, populates 'terminates \true'
[wp] terminates_call_options.c:33: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] FRAMAC_SHARE/libc/stdlib.h:475: Warning:
+[wp] FRAMAC_SHARE/libc/stdlib.h:510: Warning:
Missing terminates clause for exit, populates 'terminates \true'
-[wp] FRAMAC_SHARE/libc/stdlib.h:606: Warning:
+[wp] FRAMAC_SHARE/libc/stdlib.h:641: Warning:
Missing terminates clause for div, populates 'terminates \true'
------------------------------------------------------------
Function call_declaration
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
index fc71ff0b795..255e0df6d99 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
@@ -11,9 +11,9 @@
Missing terminates clause for declaration, populates 'terminates \true'
[wp] terminates_call_options.c:33: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] FRAMAC_SHARE/libc/stdlib.h:475: Warning:
+[wp] FRAMAC_SHARE/libc/stdlib.h:510: Warning:
Missing terminates clause for exit, populates 'terminates \true'
-[wp] FRAMAC_SHARE/libc/stdlib.h:606: Warning:
+[wp] FRAMAC_SHARE/libc/stdlib.h:641: Warning:
Missing terminates clause for div, populates 'terminates \true'
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
diff --git a/tests/builtins/oracle/realloc.res.oracle b/tests/builtins/oracle/realloc.res.oracle
index d92b1ad7dcd..3441c23c27b 100644
--- a/tests/builtins/oracle/realloc.res.oracle
+++ b/tests/builtins/oracle/realloc.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from realloc.c:160.
+ Called from realloc.c:177.
[eva] realloc.c:12: Call to builtin malloc
[eva] realloc.c:12: allocating variable __malloc_main1_l12
[eva] realloc.c:15:
@@ -67,7 +67,7 @@
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from realloc.c:161.
+ Called from realloc.c:178.
[eva] computing for function Frama_C_interval <- main2 <- main.
Called from realloc.c:22.
[eva] using specification for function Frama_C_interval
@@ -114,7 +114,7 @@
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from realloc.c:162.
+ Called from realloc.c:179.
[eva] realloc.c:32: Call to builtin malloc
[eva] realloc.c:32: allocating variable __malloc_main3_l32
[eva] realloc.c:35: Call to builtin malloc
@@ -204,7 +204,7 @@
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from realloc.c:163.
+ Called from realloc.c:180.
[eva] computing for function Frama_C_interval <- main4 <- main.
Called from realloc.c:53.
[eva] realloc.c:53:
@@ -329,7 +329,7 @@
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from realloc.c:164.
+ Called from realloc.c:181.
[eva] realloc.c:76: Call to builtin malloc
[eva] realloc.c:76: allocating variable __malloc_main5_l76
[eva] computing for function Frama_C_interval <- main5 <- main.
@@ -405,7 +405,7 @@
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from realloc.c:165.
+ Called from realloc.c:182.
[eva] computing for function Frama_C_interval <- main6 <- main.
Called from realloc.c:92.
[eva] realloc.c:92:
@@ -423,7 +423,7 @@
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from realloc.c:166.
+ Called from realloc.c:183.
[eva] realloc.c:110: Call to builtin malloc
[eva] realloc.c:110: allocating variable __malloc_main7_l110
[eva] realloc.c:115: Call to builtin realloc
@@ -488,7 +488,7 @@
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from realloc.c:167.
+ Called from realloc.c:184.
[eva] realloc.c:123: Call to builtin malloc
[eva] realloc.c:123: allocating variable __malloc_main8_l123
[eva] realloc.c:126: Call to builtin realloc
@@ -525,7 +525,7 @@
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
- Called from realloc.c:168.
+ Called from realloc.c:185.
[eva] realloc.c:132: Call to builtin malloc
[eva] realloc.c:132: allocating variable __malloc_main9_l132
[eva] realloc.c:135: Call to builtin realloc
@@ -562,7 +562,7 @@
[eva] Recording results for main9
[eva] Done for function main9
[eva] computing for function main10 <- main.
- Called from realloc.c:169.
+ Called from realloc.c:186.
[eva] realloc.c:147: Call to builtin malloc
[eva] realloc.c:147: allocating variable __malloc_main10_l147
[eva] realloc.c:152: Call to builtin realloc
@@ -627,6 +627,73 @@
==END OF DUMP==
[eva] Recording results for main10
[eva] Done for function main10
+[eva] computing for function main11 <- main.
+ Called from realloc.c:187.
+[eva] realloc.c:160: Call to builtin malloc
+[eva] realloc.c:160: allocating variable __malloc_main11_l160
+[eva] realloc.c:165: Call to builtin reallocarray
+[eva] realloc.c:165:
+ function reallocarray: precondition 'freeable' got status valid.
+[eva:malloc] bases_to_realloc: {__malloc_main11_l160}
+[eva] realloc.c:165: allocating variable __realloc_main11_l165
+[eva:malloc] realloc.c:165: strong free on bases: {__malloc_main11_l160}
+[eva] realloc.c:167: Call to builtin reallocarray
+[eva] realloc.c:167:
+ function reallocarray: precondition 'freeable' got status valid.
+[eva] realloc.c:167: Warning:
+ reallocarray out of bounds: assert(nmemb * size <= SIZE_MAX)
+[eva] realloc.c:168: assertion got status valid.
+[eva] computing for function Frama_C_interval <- main11 <- main.
+ Called from realloc.c:169.
+[eva] realloc.c:169:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] realloc.c:171: Call to builtin reallocarray
+[eva] realloc.c:171:
+ function reallocarray: precondition 'freeable' got status valid.
+[eva] realloc.c:171: Warning:
+ reallocarray out of bounds: assert(nmemb * size <= SIZE_MAX)
+[eva:malloc] bases_to_realloc: {}
+[eva] realloc.c:171: allocating variable __realloc_main11_l171
+[eva:malloc] realloc.c:171: strong free on bases: {}
+[eva] realloc.c:172: Frama_C_show_each_p: {0}
+[eva] realloc.c:172: Frama_C_show_each_p: {{ &__realloc_main11_l171 }}
+[eva] realloc.c:165: Call to builtin reallocarray
+[eva:malloc] bases_to_realloc: {__realloc_main11_l171}
+[eva:malloc:weak] realloc.c:165:
+ marking variable `__realloc_main11_l165' as weak
+[eva:malloc] realloc.c:165: strong free on bases: {__realloc_main11_l171}
+[eva] realloc.c:165: Call to builtin reallocarray
+[eva:malloc] bases_to_realloc: {}
+[eva:malloc] realloc.c:165: strong free on bases: {}
+[eva:alarm] realloc.c:166: Warning:
+ accessing uninitialized left-value. assert \initialized(p);
+[eva] realloc.c:167: Call to builtin reallocarray
+[eva] realloc.c:167: Call to builtin reallocarray
+[eva] computing for function Frama_C_interval <- main11 <- main.
+ Called from realloc.c:169.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main11 <- main.
+ Called from realloc.c:169.
+[eva] Done for function Frama_C_interval
+[eva] realloc.c:171: Call to builtin reallocarray
+[eva:malloc] bases_to_realloc: {}
+[eva:malloc] realloc.c:171: strong free on bases: {}
+[eva] realloc.c:171: Call to builtin reallocarray
+[eva:malloc] bases_to_realloc: {}
+[eva:malloc] realloc.c:171: strong free on bases: {}
+[eva] realloc.c:172: Frama_C_show_each_p: {0}
+[eva] realloc.c:172: Frama_C_show_each_p: {{ &__realloc_main11_l171 }}
+[eva] realloc.c:172: Frama_C_show_each_p: {0}
+[eva] realloc.c:172: Frama_C_show_each_p: {{ &__realloc_main11_l171 }}
+[eva] realloc.c:165: Call to builtin reallocarray
+[eva:malloc] bases_to_realloc: {__realloc_main11_l171}
+[eva:malloc] realloc.c:165: strong free on bases: {__realloc_main11_l171}
+[eva] realloc.c:165: Call to builtin reallocarray
+[eva:malloc] bases_to_realloc: {}
+[eva:malloc] realloc.c:165: strong free on bases: {}
+[eva] Recording results for main11
+[eva] Done for function main11
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -689,12 +756,23 @@
__fc_heap_status ∈ [--..--]
p ∈ ESCAPINGADDR
q ∈ ESCAPINGADDR
+[eva:final-states] Values at end of function main11:
+ __fc_heap_status ∈ [--..--]
+ Frama_C_entropy_source ∈ [--..--]
+ p ∈ {{ NULL ; &__malloc_main11_l160 ; (int *)&__realloc_main11_l171 }}
+ q ∈ {0} or UNINITIALIZED or ESCAPINGADDR
+ __malloc_main11_l160 ∈ {4}
+ __realloc_w_main11_l165[0] ∈ {4} or UNINITIALIZED
+ [1] ∈ UNINITIALIZED
[eva:final-states] Values at end of function main:
__fc_heap_status ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
__malloc_main10_l147 ∈ {4}
__realloc_w_main10_l152[0] ∈ {4}
[1] ∈ UNINITIALIZED
+ __malloc_main11_l160 ∈ {4}
+ __realloc_w_main11_l165[0] ∈ {4} or UNINITIALIZED
+ [1] ∈ UNINITIALIZED
[from] Computing for function main1
[from] Computing for function malloc <-main1
[from] Done for function malloc
@@ -723,6 +801,10 @@
[from] Done for function main8
[from] Computing for function main9
[from] Done for function main9
+[from] Computing for function main11
+[from] Computing for function reallocarray <-main11
+[from] Done for function reallocarray
+[from] Done for function main11
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
@@ -780,10 +862,21 @@
[from] Function main9:
__fc_heap_status FROM __fc_heap_status (and SELF)
__malloc_main9_l132[0..1] FROM __fc_heap_status
+[from] Function reallocarray:
+ __fc_heap_status FROM __fc_heap_status; nmemb; size (and SELF)
+ \result FROM __fc_heap_status; ptr; nmemb; size
+[from] Function main11:
+ __fc_heap_status FROM __fc_heap_status; Frama_C_entropy_source;
+ v (and SELF)
+ Frama_C_entropy_source FROM Frama_C_entropy_source; v (and SELF)
+ __malloc_main11_l160 FROM __fc_heap_status
+ __realloc_w_main11_l165[0]
+ FROM __fc_heap_status; Frama_C_entropy_source;
+ v; __realloc_w_main11_l165[0] (and SELF)
[from] Function main:
__fc_heap_status FROM __fc_heap_status; Frama_C_entropy_source;
v (and SELF)
- Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ Frama_C_entropy_source FROM Frama_C_entropy_source; v (and SELF)
__malloc_main1_l12 FROM __fc_heap_status
__malloc_main2_l23[0..3]
FROM __fc_heap_status; Frama_C_entropy_source (and SELF)
@@ -803,6 +896,10 @@
__realloc_w_main10_l152[0]
FROM __fc_heap_status; Frama_C_entropy_source;
v; __realloc_w_main10_l152[0] (and SELF)
+ __malloc_main11_l160 FROM __fc_heap_status; Frama_C_entropy_source; v
+ __realloc_w_main11_l165[0]
+ FROM __fc_heap_status; Frama_C_entropy_source;
+ v; __realloc_w_main11_l165[0] (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main1:
__fc_heap_status; p; pp; q; __malloc_main1_l12
@@ -847,12 +944,19 @@
__fc_heap_status; p; q; __malloc_main9_l132[0..1]
[inout] Inputs for function main9:
__fc_heap_status
+[inout] Out (internal) for function main11:
+ __fc_heap_status; Frama_C_entropy_source; p; q; nmemb;
+ __malloc_main11_l160; __realloc_w_main11_l165[0]
+[inout] Inputs for function main11:
+ __fc_heap_status; Frama_C_entropy_source; v; __realloc_w_main11_l165[0]
[inout] Out (internal) for function main:
__fc_heap_status; Frama_C_entropy_source; __malloc_main1_l12;
__malloc_main2_l23[0..3]; __malloc_main3_l32[0..4];
__malloc_main3_l35[0..5]; __malloc_main4_l55[0..9];
__malloc_main4_l56[0..9]; __malloc_main5_l76; __malloc_main7_l110;
__malloc_main8_l123[0..1]; __malloc_main9_l132[0..1]; __malloc_main10_l147;
- __realloc_w_main10_l152[0]
+ __realloc_w_main10_l152[0]; __malloc_main11_l160;
+ __realloc_w_main11_l165[0]
[inout] Inputs for function main:
- __fc_heap_status; Frama_C_entropy_source; v; __realloc_w_main10_l152[0]
+ __fc_heap_status; Frama_C_entropy_source; v; __realloc_w_main10_l152[0];
+ __realloc_w_main11_l165[0]
diff --git a/tests/builtins/oracle_gauges/realloc.res.oracle b/tests/builtins/oracle_gauges/realloc.res.oracle
index 069f27f2969..05fc14b03b3 100644
--- a/tests/builtins/oracle_gauges/realloc.res.oracle
+++ b/tests/builtins/oracle_gauges/realloc.res.oracle
@@ -336,3 +336,76 @@
> __realloc_w_main10_l152[0] ∈ {4}
> [1] ∈ UNINITIALIZED
> ==END OF DUMP==
+694a1032,1096
+> [eva] realloc.c:167: Call to builtin reallocarray
+> [eva] realloc.c:167: Call to builtin reallocarray
+> [eva] computing for function Frama_C_interval <- main11 <- main.
+> Called from realloc.c:169.
+> [eva] Done for function Frama_C_interval
+> [eva] computing for function Frama_C_interval <- main11 <- main.
+> Called from realloc.c:169.
+> [eva] Done for function Frama_C_interval
+> [eva] realloc.c:171: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {}
+> [eva:malloc] realloc.c:171: strong free on bases: {}
+> [eva] realloc.c:171: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {}
+> [eva:malloc] realloc.c:171: strong free on bases: {}
+> [eva] realloc.c:172: Frama_C_show_each_p: {0}
+> [eva] realloc.c:172: Frama_C_show_each_p: {{ &__realloc_main11_l171 }}
+> [eva] realloc.c:172: Frama_C_show_each_p: {0}
+> [eva] realloc.c:172: Frama_C_show_each_p: {{ &__realloc_main11_l171 }}
+> [eva] realloc.c:165: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {__realloc_main11_l171}
+> [eva:malloc] realloc.c:165: weak free on bases: {__realloc_main11_l171}
+> [eva] realloc.c:167: Call to builtin reallocarray
+> [eva] computing for function Frama_C_interval <- main11 <- main.
+> Called from realloc.c:169.
+> [eva] Done for function Frama_C_interval
+> [eva] realloc.c:171: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {}
+> [eva:malloc:weak] realloc.c:171:
+> marking variable `__realloc_main11_l171' as weak
+> [eva:malloc] realloc.c:171: strong free on bases: {}
+> [eva] realloc.c:172: Frama_C_show_each_p: {{ NULL ; &__realloc_w_main11_l171 }}
+> [eva] realloc.c:163: starting to merge loop iterations
+> [eva] realloc.c:165: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {__realloc_w_main11_l171}
+> [eva:malloc] realloc.c:165: weak free on bases: {__realloc_w_main11_l171}
+> [eva] realloc.c:167: Call to builtin reallocarray
+> [eva] computing for function Frama_C_interval <- main11 <- main.
+> Called from realloc.c:169.
+> [eva] Done for function Frama_C_interval
+> [eva] realloc.c:171: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {}
+> [eva:malloc] realloc.c:171: strong free on bases: {}
+> [eva] realloc.c:172: Frama_C_show_each_p: {{ NULL ; &__realloc_w_main11_l171 }}
+> [eva] realloc.c:165: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {__realloc_w_main11_l171}
+> [eva:malloc] realloc.c:165: weak free on bases: {__realloc_w_main11_l171}
+> [eva] realloc.c:167: Call to builtin reallocarray
+> [eva] computing for function Frama_C_interval <- main11 <- main.
+> Called from realloc.c:169.
+> [eva] Done for function Frama_C_interval
+> [eva] realloc.c:171: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {}
+> [eva:malloc] realloc.c:171: strong free on bases: {}
+> [eva] realloc.c:172: Frama_C_show_each_p: {{ NULL ; &__realloc_w_main11_l171 }}
+> [eva] realloc.c:165: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {__realloc_w_main11_l171}
+> [eva:malloc] realloc.c:165: weak free on bases: {__realloc_w_main11_l171}
+> [eva] realloc.c:167: Call to builtin reallocarray
+> [eva] computing for function Frama_C_interval <- main11 <- main.
+> Called from realloc.c:169.
+> [eva] Done for function Frama_C_interval
+> [eva] realloc.c:171: Call to builtin reallocarray
+> [eva:malloc] bases_to_realloc: {}
+> [eva:malloc] realloc.c:171: strong free on bases: {}
+> [eva] realloc.c:172: Frama_C_show_each_p: {{ NULL ; &__realloc_w_main11_l171 }}
+762,763c1164,1166
+< p ∈ {{ NULL ; &__malloc_main11_l160 ; (int *)&__realloc_main11_l171 }}
+< q ∈ {0} or UNINITIALIZED or ESCAPINGADDR
+---
+> p ∈ {{ NULL ; &__malloc_main11_l160 ; (int *)&__realloc_w_main11_l171 }}
+> q ∈
+> {{ NULL ; (int *)&__realloc_w_main11_l171 }} or UNINITIALIZED or ESCAPINGADDR
diff --git a/tests/builtins/realloc.c b/tests/builtins/realloc.c
index bb11b50a7a7..b67d078b18d 100644
--- a/tests/builtins/realloc.c
+++ b/tests/builtins/realloc.c
@@ -1,7 +1,7 @@
/* run.config*
STDOPT: +"-eva-slevel 10 -eva-alloc-builtin by_stack -eva-warn-copy-indeterminate @all"
*/
-
+#include <stdint.h>
#include <stdlib.h>
#include "__fc_builtin.h"
@@ -156,6 +156,23 @@ void main10() {
}
}
+void main11() {
+ int *p = malloc(sizeof(int));
+ int *q;
+ *p = 4;
+ while (v) {
+ q = p;
+ p = reallocarray(p, 2, sizeof(int));
+ *p = *p; // always succeeds (provided realloc does not return NULL)
+ p = reallocarray(p, SIZE_MAX, sizeof(int)); // always fails
+ //@ assert p == \null;
+ int nmemb = Frama_C_interval(3,10);
+ // succeeds sometimes, fails sometimes
+ p = reallocarray(p, nmemb, SIZE_MAX/6); // always fails
+ Frama_C_show_each_p(p);
+ }
+}
+
void main() {
main1();
main2();
@@ -167,5 +184,5 @@ void main() {
main8();
main9();
main10();
+ main11();
}
-
diff --git a/tests/libc/oracle/argz_c.res.oracle b/tests/libc/oracle/argz_c.res.oracle
index c423da43955..b3215f8143a 100644
--- a/tests/libc/oracle/argz_c.res.oracle
+++ b/tests/libc/oracle/argz_c.res.oracle
@@ -18,6 +18,7 @@
\return(calloc) == 0 (auto)
\return(malloc) == 0 (auto)
\return(realloc) == 0 (auto)
+ \return(reallocarray) == 0 (auto)
\return(getenv) == 0 (auto)
\return(bsearch) == 0 (auto)
\return(memchr) == 0 (auto)
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 8f5441c585c..d09173f9031 100644
--- a/tests/libc/oracle/coverage.res.oracle
+++ b/tests/libc/oracle/coverage.res.oracle
@@ -28,7 +28,7 @@
main: 4 stmts out of 4 (100.0%)
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 2 (out of 115)
+ Syntactically reachable functions = 2 (out of 116)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index a2690ea17ce..db63ecd0f20 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1481,6 +1481,44 @@ extern void free(void *p);
*/
extern void *realloc(void *ptr, size_t size);
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status
+ \from (indirect: nmemb), (indirect: size), __fc_heap_status;
+ assigns \result
+ \from ptr, (indirect: nmemb), (indirect: size),
+ (indirect: __fc_heap_status);
+ frees ptr;
+ allocates \result;
+
+ behavior allocation:
+ assumes can_allocate: is_allocable(nmemb * size);
+ ensures
+ allocation: \fresh{Old, Here}(\result,\old(nmemb) * \old(size));
+ allocates \result;
+
+ behavior deallocation:
+ assumes nonnull_ptr: ptr ≢ \null;
+ assumes can_allocate: is_allocable(nmemb * size);
+ ensures freed: \allocable(\old(ptr));
+ ensures freeable: \result ≡ \null ∨ \freeable(\result);
+ frees ptr;
+
+ behavior fail:
+ assumes cannot_allocate: ¬is_allocable(nmemb * size);
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result
+ \from (indirect: nmemb), (indirect: size),
+ (indirect: __fc_heap_status);
+ allocates \nothing;
+
+ complete behaviors fail, deallocation, allocation;
+ disjoint behaviors allocation, fail;
+ disjoint behaviors deallocation, fail;
+ */
+extern void *reallocarray(void *ptr, size_t nmemb, size_t size);
+
/*@ exits status: \exit_status ≢ 0;
ensures never_terminates: \false;
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 7f18a97a720..dd5fb9f0607 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -13,6 +13,7 @@
\return(calloc) == 0 (auto)
\return(malloc) == 0 (auto)
\return(realloc) == 0 (auto)
+ \return(reallocarray) == 0 (auto)
\return(getenv) == 0 (auto)
\return(bsearch) == 0 (auto)
\return(getcwd) == 0 (auto)
--
GitLab