From ecae8c033c11a0fba4b2d9ad43002ee3e28b72de Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 22 Jul 2024 10:42:16 +0200
Subject: [PATCH] [tests] Update test oracles
---
.../e-acsl/tests/builtin/oracle/gen_strcat.c | 10 +-
.../e-acsl/tests/builtin/oracle/gen_strcmp.c | 18 +-
.../e-acsl/tests/builtin/oracle/gen_strcpy.c | 10 +-
.../e-acsl/tests/builtin/oracle/gen_strlen.c | 18 +-
.../tests/builtin/oracle/strcat.res.oracle | 13 +-
.../tests/builtin/oracle/strcmp.res.oracle | 14 +-
.../tests/builtin/oracle/strcpy.res.oracle | 9 +-
.../tests/builtin/oracle/strlen.res.oracle | 14 +-
.../concurrency/oracle/gen_parallel_threads.c | 10 +-
.../concurrency/oracle/gen_threads_debug.c | 10 +-
.../oracle/parallel_threads.res.oracle | 11 +-
.../oracle/threads_debug.res.oracle | 11 +-
.../tests/format/oracle/fprintf.res.oracle | 13 +-
.../e-acsl/tests/format/oracle/gen_fprintf.c | 10 +-
.../e-acsl/tests/format/oracle/gen_printf.c | 18 +-
.../tests/format/oracle/printf.res.oracle | 18 +-
.../tests/memory/oracle/gen_hidden_malloc.c | 14 +-
.../e-acsl/tests/memory/oracle/gen_memalign.c | 8 +-
.../memory/oracle/hidden_malloc.res.oracle | 30 +-
.../tests/memory/oracle/memalign.res.oracle | 14 +-
.../tests/temporal/oracle/gen_t_fun_lib.c | 14 +-
.../temporal/oracle/t_fun_lib.res.oracle | 30 +-
.../tests/temporal/oracle/t_getenv.res.oracle | 8 +-
.../tests/sarif/oracle/std_string.sarif | 1132 +++++++++--------
.../terminates_call_options.0.res.oracle | 13 +-
.../terminates_call_options.1.res.oracle | 13 +-
.../terminates_call_options.0.res.oracle | 16 +-
.../terminates_call_options.1.res.oracle | 16 +-
src/plugins/wp/tests/wp_bts/issue-684-exit.c | 2 +-
.../wp_bts/oracle/issue-684-exit.res.oracle | 3 -
.../oracle_qualif/issue-684-exit.res.oracle | 3 -
tests/libc/oracle/fc_libc.1.res.oracle | 15 +-
32 files changed, 843 insertions(+), 695 deletions(-)
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 a2904448f63..f3b8d9158f2 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -45,7 +45,8 @@ char *__gen_e_acsl_literal_string_4;
char *__gen_e_acsl_literal_string_8;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -648,7 +649,7 @@ pid_t __gen_e_acsl_fork(void)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result > 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "fork";
- __gen_e_acsl_assert_data.line = 853;
+ __gen_e_acsl_assert_data.line = 854;
__gen_e_acsl_assert_data.name = "result_ok_child_or_error";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -777,7 +778,8 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
}
}
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -792,7 +794,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 = 541;
+ __gen_e_acsl_assert_data.line = 543;
__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 aafae25a51c..58862fef589 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -47,14 +47,16 @@ char *__gen_e_acsl_literal_string_5;
char *__gen_e_acsl_literal_string_4;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-/*@ exits status: \exit_status != 0;
+/*@ terminates \false;
+ exits status: \exit_status != 0;
ensures never_terminates: \false;
assigns \exit_status \from \nothing;
*/
void __gen_e_acsl_abort(void);
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -215,7 +217,7 @@ pid_t __gen_e_acsl_fork(void)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result > 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "fork";
- __gen_e_acsl_assert_data.line = 853;
+ __gen_e_acsl_assert_data.line = 854;
__gen_e_acsl_assert_data.name = "result_ok_child_or_error";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -344,7 +346,8 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
}
}
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -359,14 +362,15 @@ 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 = 541;
+ __gen_e_acsl_assert_data.line = 543;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
}
}
-/*@ exits status: \exit_status != 0;
+/*@ terminates \false;
+ exits status: \exit_status != 0;
ensures never_terminates: \false;
assigns \exit_status \from \nothing;
@@ -381,7 +385,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 = 528;
+ __gen_e_acsl_assert_data.line = 529;
__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 4bdf04acd31..72d8735dd4a 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -39,7 +39,8 @@ char *__gen_e_acsl_literal_string_4;
char *__gen_e_acsl_literal_string_8;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -629,7 +630,7 @@ pid_t __gen_e_acsl_fork(void)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result > 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "fork";
- __gen_e_acsl_assert_data.line = 853;
+ __gen_e_acsl_assert_data.line = 854;
__gen_e_acsl_assert_data.name = "result_ok_child_or_error";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -758,7 +759,8 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
}
}
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -773,7 +775,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 = 541;
+ __gen_e_acsl_assert_data.line = 543;
__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 e5c67b3fb3b..4aefe12825d 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -30,14 +30,16 @@ char *__gen_e_acsl_literal_string_4;
char *__gen_e_acsl_literal_string_6;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-/*@ exits status: \exit_status != 0;
+/*@ terminates \false;
+ exits status: \exit_status != 0;
ensures never_terminates: \false;
assigns \exit_status \from \nothing;
*/
void __gen_e_acsl_abort(void);
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -189,7 +191,7 @@ pid_t __gen_e_acsl_fork(void)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result > 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "fork";
- __gen_e_acsl_assert_data.line = 853;
+ __gen_e_acsl_assert_data.line = 854;
__gen_e_acsl_assert_data.name = "result_ok_child_or_error";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -318,7 +320,8 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
}
}
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -333,14 +336,15 @@ 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 = 541;
+ __gen_e_acsl_assert_data.line = 543;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
}
}
-/*@ exits status: \exit_status != 0;
+/*@ terminates \false;
+ exits status: \exit_status != 0;
ensures never_terminates: \false;
assigns \exit_status \from \nothing;
@@ -355,7 +359,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 = 528;
+ __gen_e_acsl_assert_data.line = 529;
__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 d02d6247e7e..88f5b05f952 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
@@ -8,7 +8,7 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:850: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
@@ -17,17 +17,20 @@
[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:538: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:540: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:542: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:853: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:854: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:854: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:855: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
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 bb53260a54c..fe418e3cb58 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -49,7 +49,7 @@
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:850: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
@@ -58,17 +58,23 @@
[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:538: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:540: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:542: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:525: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:525: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:527: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:528: 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 36773318ccf..38f864e7d0f 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -44,7 +44,7 @@
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:850: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
@@ -53,10 +53,13 @@
[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:538: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:540: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:542: 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 ac28c649697..7a5615f923d 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -47,7 +47,7 @@
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:850: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
@@ -56,17 +56,23 @@
[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:538: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:540: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:542: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:525: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:525: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:527: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:528: 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 e9281168b6b..a73f89d3e51 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
@@ -127,7 +127,8 @@ int __gen_e_acsl_pthread_mutex_unlock(pthread_mutex_t *mutex);
*/
void __gen_e_acsl_perror(char const *s);
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -751,7 +752,7 @@ int __gen_e_acsl_usleep(useconds_t usec)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "usleep";
- __gen_e_acsl_assert_data.line = 1152;
+ __gen_e_acsl_assert_data.line = 1153;
__gen_e_acsl_assert_data.name = "result_ok_or_error";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -761,7 +762,8 @@ int __gen_e_acsl_usleep(useconds_t usec)
}
}
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -777,7 +779,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 = 541;
+ __gen_e_acsl_assert_data.line = 543;
__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 cac668b0f9c..7583e2dc85f 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
@@ -127,7 +127,8 @@ int __gen_e_acsl_pthread_mutex_unlock(pthread_mutex_t *mutex);
*/
void __gen_e_acsl_perror(char const *s);
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -433,7 +434,7 @@ int __gen_e_acsl_usleep(useconds_t usec)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "usleep";
- __gen_e_acsl_assert_data.line = 1152;
+ __gen_e_acsl_assert_data.line = 1153;
__gen_e_acsl_assert_data.name = "result_ok_or_error";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -443,7 +444,8 @@ int __gen_e_acsl_usleep(useconds_t usec)
}
}
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -459,7 +461,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 = 541;
+ __gen_e_acsl_assert_data.line = 543;
__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 c2671f31670..97e24b1e6ab 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
@@ -35,13 +35,16 @@
[e-acsl] Warning: annotating undefined function `usleep':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:1149: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:1150: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:538: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:540: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:542: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
@@ -181,6 +184,6 @@
[eva:alarm] FRAMAC_SHARE/libc/pthread.h:316: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1152: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1153: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
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 c2671f31670..97e24b1e6ab 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
@@ -35,13 +35,16 @@
[e-acsl] Warning: annotating undefined function `usleep':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:1149: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:1150: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:538: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:540: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:542: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
@@ -181,6 +184,6 @@
[eva:alarm] FRAMAC_SHARE/libc/pthread.h:316: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1152: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:1153: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
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 2dcda065ad3..313b4259076 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -14,7 +14,7 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:850: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
@@ -23,10 +23,13 @@
[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:538: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:540: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:542: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
@@ -42,9 +45,9 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:853: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:854: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:854: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:855: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
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 7ea82209ac3..8aa685ba92e 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -60,7 +60,8 @@ FILE *__gen_e_acsl_tmpfile(void);
*/
int __gen_e_acsl_fclose(FILE *stream);
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -126,7 +127,7 @@ pid_t __gen_e_acsl_fork(void)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result > 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "fork";
- __gen_e_acsl_assert_data.line = 853;
+ __gen_e_acsl_assert_data.line = 854;
__gen_e_acsl_assert_data.name = "result_ok_child_or_error";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -255,7 +256,8 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
}
}
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -270,7 +272,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 = 541;
+ __gen_e_acsl_assert_data.line = 543;
__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 3303e73fa2a..fed7aed3b60 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -472,14 +472,16 @@ char *__gen_e_acsl_literal_string_34;
char *__gen_e_acsl_literal_string_441;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-/*@ exits status: \exit_status != 0;
+/*@ terminates \false;
+ exits status: \exit_status != 0;
ensures never_terminates: \false;
assigns \exit_status \from \nothing;
*/
void __gen_e_acsl_abort(void);
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -982,7 +984,7 @@ pid_t __gen_e_acsl_fork(void)
__gen_e_acsl_assert_data.pred_txt = "\\result == 0 || \\result > 0 || \\result == -1";
__gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/unistd.h";
__gen_e_acsl_assert_data.fct = "fork";
- __gen_e_acsl_assert_data.line = 853;
+ __gen_e_acsl_assert_data.line = 854;
__gen_e_acsl_assert_data.name = "result_ok_child_or_error";
__e_acsl_assert(__gen_e_acsl_or_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
@@ -1111,7 +1113,8 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
}
}
-/*@ exits status: \exit_status == \old(status);
+/*@ terminates \false;
+ exits status: \exit_status == \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
@@ -1126,14 +1129,15 @@ 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 = 541;
+ __gen_e_acsl_assert_data.line = 543;
__gen_e_acsl_assert_data.name = "never_terminates";
__e_acsl_assert(0,& __gen_e_acsl_assert_data);
return;
}
}
-/*@ exits status: \exit_status != 0;
+/*@ terminates \false;
+ exits status: \exit_status != 0;
ensures never_terminates: \false;
assigns \exit_status \from \nothing;
@@ -1148,7 +1152,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 = 528;
+ __gen_e_acsl_assert_data.line = 529;
__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 f1fb00a4f41..23cc7252106 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -81,7 +81,7 @@
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/unistd.h:850: Warning:
+[e-acsl] FRAMAC_SHARE/libc/unistd.h:851: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:82: Warning:
@@ -90,24 +90,30 @@
[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:538: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:539: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:540: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:542: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:525: Warning:
+ E-ACSL construct `terminates clause' is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:525: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:527: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:528: Warning:
E-ACSL construct `abnormal termination case in behavior'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:853: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:854: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/unistd.h:854: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/unistd.h:855: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
index 321145a5564..a7441e7b6a8 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
@@ -205,7 +205,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_2.pred_txt = "resolved_name == \\null || \\valid(resolved_name + (0 .. 4096 - 1))";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_2.fct = "realpath";
- __gen_e_acsl_assert_data_2.line = 842;
+ __gen_e_acsl_assert_data_2.line = 846;
__gen_e_acsl_assert_data_2.name = "resolved_name_null_or_allocated";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -231,7 +231,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_4.pred_txt = "__fc_errno == 22";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_4.fct = "realpath";
- __gen_e_acsl_assert_data_4.line = 853;
+ __gen_e_acsl_assert_data_4.line = 857;
__gen_e_acsl_assert_data_4.name = "null_file_name/errno_set";
__e_acsl_assert(errno == 22,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -240,7 +240,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_3.pred_txt = "\\result == \\null";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_3.fct = "realpath";
- __gen_e_acsl_assert_data_3.line = 852;
+ __gen_e_acsl_assert_data_3.line = 856;
__gen_e_acsl_assert_data_3.name = "null_file_name/null_result";
__e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -261,7 +261,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_7.pred_txt = "__fc_errno == 12";
__gen_e_acsl_assert_data_7.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_7.fct = "realpath";
- __gen_e_acsl_assert_data_7.line = 868;
+ __gen_e_acsl_assert_data_7.line = 872;
__gen_e_acsl_assert_data_7.name = "not_enough_memory/errno_set";
__e_acsl_assert(errno == 12,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
@@ -270,7 +270,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_6.pred_txt = "\\result == \\null";
__gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_6.fct = "realpath";
- __gen_e_acsl_assert_data_6.line = 867;
+ __gen_e_acsl_assert_data_6.line = 871;
__gen_e_acsl_assert_data_6.name = "not_enough_memory/null_result";
__e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
@@ -290,7 +290,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_9.pred_txt = "\\result == \\old(resolved_name)";
__gen_e_acsl_assert_data_9.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_9.fct = "realpath";
- __gen_e_acsl_assert_data_9.line = 880;
+ __gen_e_acsl_assert_data_9.line = 884;
__gen_e_acsl_assert_data_9.name = "resolved_name_buffer/resolved_result";
__e_acsl_assert(__retres == __gen_e_acsl_at,
& __gen_e_acsl_assert_data_9);
@@ -308,7 +308,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_10.pred_txt = "\\result == \\null";
__gen_e_acsl_assert_data_10.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_10.fct = "realpath";
- __gen_e_acsl_assert_data_10.line = 886;
+ __gen_e_acsl_assert_data_10.line = 890;
__gen_e_acsl_assert_data_10.name = "filesystem_error/null_result";
__e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
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 80d3c12fd94..1592b8cdd10 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
@@ -420,7 +420,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 = 785;
+ __gen_e_acsl_assert_data.line = 789;
__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);
@@ -463,7 +463,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 = 787;
+ __gen_e_acsl_assert_data_2.line = 791;
__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);
@@ -483,7 +483,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 = 799;
+ __gen_e_acsl_assert_data_4.line = 803;
__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);
@@ -507,7 +507,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 = 804;
+ __gen_e_acsl_assert_data_5.line = 808;
__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/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
index 27d93fcb73c..e1c36e05ce0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
@@ -2,57 +2,57 @@
[e-acsl] Warning: annotating undefined function `realpath':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:838: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:840: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:844: Warning:
no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:277: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:855: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:859: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:862: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:866: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:870: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:874: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:882: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:886: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:838: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:838: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:853: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:857: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:860: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:864: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:860: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:864: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:868: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:872: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:876: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:880: Warning:
no assigns clause generated for function valid_string because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:880: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:884: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:888: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:892: Warning:
E-ACSL construct
`logic functions or predicates with no definition nor reads clause'
is not yet supported.
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 f17a43af95d..b9cee10fd6f 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
@@ -2,25 +2,25 @@
[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:784: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:788: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:794: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:798: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:801: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:805: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:784: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:788: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:784: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:788: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:798: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:802: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:799: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:803: 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_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
index 78967c20b82..37f8bf4b801 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
@@ -207,7 +207,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_2.pred_txt = "resolved_name == \\null || \\valid(resolved_name + (0 .. 4096 - 1))";
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_2.fct = "realpath";
- __gen_e_acsl_assert_data_2.line = 842;
+ __gen_e_acsl_assert_data_2.line = 846;
__gen_e_acsl_assert_data_2.name = "resolved_name_null_or_allocated";
__e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
@@ -238,7 +238,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_4.pred_txt = "__fc_errno == 22";
__gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_4.fct = "realpath";
- __gen_e_acsl_assert_data_4.line = 853;
+ __gen_e_acsl_assert_data_4.line = 857;
__gen_e_acsl_assert_data_4.name = "null_file_name/errno_set";
__e_acsl_assert(errno == 22,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -247,7 +247,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_3.pred_txt = "\\result == \\null";
__gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_3.fct = "realpath";
- __gen_e_acsl_assert_data_3.line = 852;
+ __gen_e_acsl_assert_data_3.line = 856;
__gen_e_acsl_assert_data_3.name = "null_file_name/null_result";
__e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -268,7 +268,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_7.pred_txt = "__fc_errno == 12";
__gen_e_acsl_assert_data_7.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_7.fct = "realpath";
- __gen_e_acsl_assert_data_7.line = 868;
+ __gen_e_acsl_assert_data_7.line = 872;
__gen_e_acsl_assert_data_7.name = "not_enough_memory/errno_set";
__e_acsl_assert(errno == 12,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
@@ -277,7 +277,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_6.pred_txt = "\\result == \\null";
__gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_6.fct = "realpath";
- __gen_e_acsl_assert_data_6.line = 867;
+ __gen_e_acsl_assert_data_6.line = 871;
__gen_e_acsl_assert_data_6.name = "not_enough_memory/null_result";
__e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
@@ -297,7 +297,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_9.pred_txt = "\\result == \\old(resolved_name)";
__gen_e_acsl_assert_data_9.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_9.fct = "realpath";
- __gen_e_acsl_assert_data_9.line = 880;
+ __gen_e_acsl_assert_data_9.line = 884;
__gen_e_acsl_assert_data_9.name = "resolved_name_buffer/resolved_result";
__e_acsl_assert(__retres == __gen_e_acsl_at,
& __gen_e_acsl_assert_data_9);
@@ -315,7 +315,7 @@ char *__gen_e_acsl_realpath(char const * restrict file_name,
__gen_e_acsl_assert_data_10.pred_txt = "\\result == \\null";
__gen_e_acsl_assert_data_10.file = "FRAMAC_SHARE/libc/stdlib.h";
__gen_e_acsl_assert_data_10.fct = "realpath";
- __gen_e_acsl_assert_data_10.line = 886;
+ __gen_e_acsl_assert_data_10.line = 890;
__gen_e_acsl_assert_data_10.name = "filesystem_error/null_result";
__e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
index 479597f9129..1fe29a8e392 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
@@ -2,57 +2,57 @@
[e-acsl] Warning: annotating undefined function `realpath':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:838: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:840: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:844: Warning:
no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:277: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:855: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:859: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:862: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:866: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:870: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:874: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:882: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:886: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:838: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:838: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:842: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:853: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:857: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:860: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:864: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:860: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:864: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:868: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:872: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:876: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:880: Warning:
no assigns clause generated for function valid_string because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:274: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:880: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:884: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:888: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:892: Warning:
E-ACSL construct
`logic functions or predicates with no definition nor reads clause'
is not yet supported.
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 8587f5a2e6a..1c517990dc7 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,21 +2,21 @@
[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:554: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:557: Warning:
no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:277: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:553: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:556: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:558: Warning:
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:561: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:558: Warning:
+[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:561: 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 2ed274caed5..dc561a824dd 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -5631,9 +5631,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 549,
+ "startLine": 552,
"startColumn": 12,
- "endLine": 549,
+ "endLine": 552,
"endColumn": 17,
"byteLength": 5
}
@@ -5654,9 +5654,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 547,
+ "startLine": 550,
"startColumn": 28,
- "endLine": 547,
+ "endLine": 550,
"endColumn": 34,
"byteLength": 6
}
@@ -5677,9 +5677,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 549,
+ "startLine": 552,
"startColumn": 12,
- "endLine": 549,
+ "endLine": 552,
"endColumn": 17,
"byteLength": 5
}
@@ -5687,6 +5687,29 @@
}
]
},
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "terminates \\false." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 548,
+ "startColumn": 13,
+ "endLine": 548,
+ "endColumn": 19,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
{
"ruleId": "user-spec",
"kind": "pass",
@@ -5700,9 +5723,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 530,
+ "startLine": 531,
"startColumn": 12,
- "endLine": 530,
+ "endLine": 531,
"endColumn": 17,
"byteLength": 5
}
@@ -5723,9 +5746,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 527,
+ "startLine": 528,
"startColumn": 16,
- "endLine": 527,
+ "endLine": 528,
"endColumn": 33,
"byteLength": 17
}
@@ -5746,9 +5769,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 528,
+ "startLine": 529,
"startColumn": 28,
- "endLine": 528,
+ "endLine": 529,
"endColumn": 34,
"byteLength": 6
}
@@ -5769,9 +5792,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 526,
+ "startLine": 527,
"startColumn": 10,
- "endLine": 526,
+ "endLine": 527,
"endColumn": 22,
"byteLength": 12
}
@@ -5794,9 +5817,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 526,
+ "startLine": 527,
"startColumn": 10,
- "endLine": 526,
+ "endLine": 527,
"endColumn": 22,
"byteLength": 12
}
@@ -5804,6 +5827,29 @@
}
]
},
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "terminates \\false." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 526,
+ "startColumn": 13,
+ "endLine": 526,
+ "endColumn": 19,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
{
"ruleId": "user-spec",
"kind": "pass",
@@ -5817,9 +5863,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 680,
+ "startLine": 684,
"startColumn": 11,
- "endLine": 680,
+ "endLine": 684,
"endColumn": 14,
"byteLength": 3
}
@@ -5840,9 +5886,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 680,
+ "startLine": 684,
"startColumn": 11,
- "endLine": 680,
+ "endLine": 684,
"endColumn": 14,
"byteLength": 3
}
@@ -5863,9 +5909,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 680,
+ "startLine": 684,
"startColumn": 11,
- "endLine": 680,
+ "endLine": 684,
"endColumn": 14,
"byteLength": 3
}
@@ -5886,9 +5932,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 669,
+ "startLine": 673,
"startColumn": 30,
- "endLine": 669,
+ "endLine": 673,
"endColumn": 51,
"byteLength": 21
}
@@ -5909,9 +5955,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 672,
+ "startLine": 676,
"startColumn": 22,
- "endLine": 672,
+ "endLine": 676,
"endColumn": 27,
"byteLength": 5
}
@@ -5932,9 +5978,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 675,
+ "startLine": 679,
"startColumn": 25,
- "endLine": 675,
+ "endLine": 679,
"endColumn": 31,
"byteLength": 6
}
@@ -5955,9 +6001,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 673,
+ "startLine": 677,
"startColumn": 29,
- "endLine": 673,
+ "endLine": 677,
"endColumn": 42,
"byteLength": 13
}
@@ -5978,9 +6024,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 676,
+ "startLine": 680,
"startColumn": 25,
- "endLine": 676,
+ "endLine": 680,
"endColumn": 37,
"byteLength": 12
}
@@ -6001,9 +6047,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 680,
+ "startLine": 684,
"startColumn": 11,
- "endLine": 680,
+ "endLine": 684,
"endColumn": 14,
"byteLength": 3
}
@@ -6026,9 +6072,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 670,
+ "startLine": 674,
"startColumn": 10,
- "endLine": 670,
+ "endLine": 674,
"endColumn": 17,
"byteLength": 7
}
@@ -6049,9 +6095,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 680,
+ "startLine": 684,
"startColumn": 11,
- "endLine": 680,
+ "endLine": 684,
"endColumn": 14,
"byteLength": 3
}
@@ -6072,9 +6118,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 680,
+ "startLine": 684,
"startColumn": 11,
- "endLine": 680,
+ "endLine": 684,
"endColumn": 14,
"byteLength": 3
}
@@ -6097,9 +6143,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 912,
+ "startLine": 916,
"startColumn": 5,
- "endLine": 912,
+ "endLine": 916,
"endColumn": 19,
"byteLength": 14
}
@@ -6120,9 +6166,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 907,
+ "startLine": 911,
"startColumn": 20,
- "endLine": 907,
+ "endLine": 911,
"endColumn": 53,
"byteLength": 33
}
@@ -6143,9 +6189,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 910,
+ "startLine": 914,
"startColumn": 26,
- "endLine": 910,
+ "endLine": 914,
"endColumn": 65,
"byteLength": 39
}
@@ -6166,9 +6212,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 908,
+ "startLine": 912,
"startColumn": 10,
- "endLine": 908,
+ "endLine": 912,
"endColumn": 32,
"byteLength": 22
}
@@ -6191,9 +6237,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 908,
+ "startLine": 912,
"startColumn": 10,
- "endLine": 908,
+ "endLine": 912,
"endColumn": 32,
"byteLength": 22
}
@@ -6216,9 +6262,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 909,
+ "startLine": 913,
"startColumn": 10,
- "endLine": 909,
+ "endLine": 913,
"endColumn": 32,
"byteLength": 22
}
@@ -6241,9 +6287,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 536,
+ "startLine": 537,
"startColumn": 11,
- "endLine": 536,
+ "endLine": 537,
"endColumn": 24,
"byteLength": 13
}
@@ -6264,9 +6310,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 536,
+ "startLine": 537,
"startColumn": 11,
- "endLine": 536,
+ "endLine": 537,
"endColumn": 24,
"byteLength": 13
}
@@ -6289,9 +6335,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 535,
+ "startLine": 536,
"startColumn": 12,
- "endLine": 535,
+ "endLine": 536,
"endColumn": 19,
"byteLength": 7
}
@@ -6312,9 +6358,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 533,
+ "startLine": 534,
"startColumn": 11,
- "endLine": 533,
+ "endLine": 534,
"endColumn": 17,
"byteLength": 6
}
@@ -6335,9 +6381,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 533,
+ "startLine": 534,
"startColumn": 11,
- "endLine": 533,
+ "endLine": 534,
"endColumn": 17,
"byteLength": 6
}
@@ -6360,9 +6406,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 532,
+ "startLine": 533,
"startColumn": 12,
- "endLine": 532,
+ "endLine": 533,
"endColumn": 19,
"byteLength": 7
}
@@ -6759,9 +6805,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 652,
+ "startLine": 656,
"startColumn": 13,
- "endLine": 652,
+ "endLine": 656,
"endColumn": 20,
"byteLength": 7
}
@@ -6782,9 +6828,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 645,
+ "startLine": 649,
"startColumn": 34,
- "endLine": 645,
+ "endLine": 649,
"endColumn": 57,
"byteLength": 23
}
@@ -6805,9 +6851,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 649,
+ "startLine": 653,
"startColumn": 34,
- "endLine": 650,
+ "endLine": 654,
"endColumn": 76,
"byteLength": 96
}
@@ -6828,9 +6874,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 652,
+ "startLine": 656,
"startColumn": 13,
- "endLine": 652,
+ "endLine": 656,
"endColumn": 20,
"byteLength": 7
}
@@ -6853,9 +6899,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 646,
+ "startLine": 650,
"startColumn": 10,
- "endLine": 646,
+ "endLine": 650,
"endColumn": 17,
"byteLength": 7
}
@@ -7438,9 +7484,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 901,
+ "startLine": 905,
"startColumn": 13,
- "endLine": 901,
+ "endLine": 905,
"endColumn": 35,
"byteLength": 22
}
@@ -7463,9 +7509,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 901,
+ "startLine": 905,
"startColumn": 13,
- "endLine": 901,
+ "endLine": 905,
"endColumn": 35,
"byteLength": 22
}
@@ -7488,9 +7534,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 899,
+ "startLine": 903,
"startColumn": 10,
- "endLine": 899,
+ "endLine": 903,
"endColumn": 17,
"byteLength": 7
}
@@ -7513,9 +7559,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 898,
+ "startLine": 902,
"startColumn": 12,
- "endLine": 898,
+ "endLine": 902,
"endColumn": 19,
"byteLength": 7
}
@@ -7611,9 +7657,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 715,
+ "startLine": 719,
"startColumn": 13,
- "endLine": 715,
+ "endLine": 719,
"endColumn": 16,
"byteLength": 3
}
@@ -7634,9 +7680,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 711,
+ "startLine": 715,
"startColumn": 26,
- "endLine": 711,
+ "endLine": 715,
"endColumn": 36,
"byteLength": 10
}
@@ -7657,9 +7703,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 712,
+ "startLine": 716,
"startColumn": 24,
- "endLine": 712,
+ "endLine": 716,
"endColumn": 68,
"byteLength": 44
}
@@ -7680,9 +7726,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 715,
+ "startLine": 719,
"startColumn": 13,
- "endLine": 715,
+ "endLine": 719,
"endColumn": 16,
"byteLength": 3
}
@@ -7705,9 +7751,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 713,
+ "startLine": 717,
"startColumn": 10,
- "endLine": 713,
+ "endLine": 717,
"endColumn": 17,
"byteLength": 7
}
@@ -8035,9 +8081,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 543,
+ "startLine": 545,
"startColumn": 12,
- "endLine": 543,
+ "endLine": 545,
"endColumn": 16,
"byteLength": 4
}
@@ -8058,9 +8104,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 540,
+ "startLine": 542,
"startColumn": 16,
- "endLine": 540,
+ "endLine": 542,
"endColumn": 38,
"byteLength": 22
}
@@ -8081,9 +8127,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 541,
+ "startLine": 543,
"startColumn": 28,
- "endLine": 541,
+ "endLine": 543,
"endColumn": 34,
"byteLength": 6
}
@@ -8104,9 +8150,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 539,
+ "startLine": 541,
"startColumn": 10,
- "endLine": 539,
+ "endLine": 541,
"endColumn": 22,
"byteLength": 12
}
@@ -8129,9 +8175,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 539,
+ "startLine": 541,
"startColumn": 10,
- "endLine": 539,
+ "endLine": 541,
"endColumn": 22,
"byteLength": 12
}
@@ -8139,6 +8185,29 @@
}
]
},
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "terminates \\false." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 540,
+ "startColumn": 13,
+ "endLine": 540,
+ "endColumn": 19,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
{
"ruleId": "user-spec",
"kind": "pass",
@@ -8524,9 +8593,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 560,
+ "startLine": 563,
"startColumn": 13,
- "endLine": 560,
+ "endLine": 563,
"endColumn": 19,
"byteLength": 6
}
@@ -8547,9 +8616,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 554,
+ "startLine": 557,
"startColumn": 23,
- "endLine": 554,
+ "endLine": 557,
"endColumn": 46,
"byteLength": 23
}
@@ -8570,9 +8639,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 558,
+ "startLine": 561,
"startColumn": 4,
- "endLine": 558,
+ "endLine": 561,
"endColumn": 71,
"byteLength": 67
}
@@ -8593,9 +8662,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 560,
+ "startLine": 563,
"startColumn": 13,
- "endLine": 560,
+ "endLine": 563,
"endColumn": 19,
"byteLength": 6
}
@@ -8618,9 +8687,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 555,
+ "startLine": 558,
"startColumn": 10,
- "endLine": 555,
+ "endLine": 558,
"endColumn": 17,
"byteLength": 7
}
@@ -8806,9 +8875,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 694,
+ "startLine": 698,
"startColumn": 16,
- "endLine": 694,
+ "endLine": 698,
"endColumn": 20,
"byteLength": 4
}
@@ -8829,9 +8898,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 694,
+ "startLine": 698,
"startColumn": 16,
- "endLine": 694,
+ "endLine": 698,
"endColumn": 20,
"byteLength": 4
}
@@ -8852,9 +8921,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 694,
+ "startLine": 698,
"startColumn": 16,
- "endLine": 694,
+ "endLine": 698,
"endColumn": 20,
"byteLength": 4
}
@@ -8875,9 +8944,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 683,
+ "startLine": 687,
"startColumn": 30,
- "endLine": 683,
+ "endLine": 687,
"endColumn": 62,
"byteLength": 32
}
@@ -8898,9 +8967,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 686,
+ "startLine": 690,
"startColumn": 22,
- "endLine": 686,
+ "endLine": 690,
"endColumn": 27,
"byteLength": 5
}
@@ -8921,9 +8990,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 689,
+ "startLine": 693,
"startColumn": 25,
- "endLine": 689,
+ "endLine": 693,
"endColumn": 31,
"byteLength": 6
}
@@ -8944,9 +9013,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 687,
+ "startLine": 691,
"startColumn": 29,
- "endLine": 687,
+ "endLine": 691,
"endColumn": 42,
"byteLength": 13
}
@@ -8967,9 +9036,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 690,
+ "startLine": 694,
"startColumn": 25,
- "endLine": 690,
+ "endLine": 694,
"endColumn": 37,
"byteLength": 12
}
@@ -8990,9 +9059,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 694,
+ "startLine": 698,
"startColumn": 16,
- "endLine": 694,
+ "endLine": 698,
"endColumn": 20,
"byteLength": 4
}
@@ -9015,9 +9084,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 684,
+ "startLine": 688,
"startColumn": 10,
- "endLine": 684,
+ "endLine": 688,
"endColumn": 17,
"byteLength": 7
}
@@ -9038,9 +9107,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 694,
+ "startLine": 698,
"startColumn": 16,
- "endLine": 694,
+ "endLine": 698,
"endColumn": 20,
"byteLength": 4
}
@@ -9061,9 +9130,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 694,
+ "startLine": 698,
"startColumn": 16,
- "endLine": 694,
+ "endLine": 698,
"endColumn": 20,
"byteLength": 4
}
@@ -9249,9 +9318,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 722,
+ "startLine": 726,
"startColumn": 14,
- "endLine": 722,
+ "endLine": 726,
"endColumn": 18,
"byteLength": 4
}
@@ -9272,9 +9341,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 718,
+ "startLine": 722,
"startColumn": 26,
- "endLine": 718,
+ "endLine": 722,
"endColumn": 36,
"byteLength": 10
}
@@ -9295,9 +9364,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 719,
+ "startLine": 723,
"startColumn": 24,
- "endLine": 719,
+ "endLine": 723,
"endColumn": 79,
"byteLength": 55
}
@@ -9318,9 +9387,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 722,
+ "startLine": 726,
"startColumn": 14,
- "endLine": 722,
+ "endLine": 726,
"endColumn": 18,
"byteLength": 4
}
@@ -9343,9 +9412,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 720,
+ "startLine": 724,
"startColumn": 10,
- "endLine": 720,
+ "endLine": 724,
"endColumn": 17,
"byteLength": 7
}
@@ -9366,9 +9435,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 708,
+ "startLine": 712,
"startColumn": 21,
- "endLine": 708,
+ "endLine": 712,
"endColumn": 26,
"byteLength": 5
}
@@ -9389,9 +9458,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 708,
+ "startLine": 712,
"startColumn": 21,
- "endLine": 708,
+ "endLine": 712,
"endColumn": 26,
"byteLength": 5
}
@@ -9412,9 +9481,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 708,
+ "startLine": 712,
"startColumn": 21,
- "endLine": 708,
+ "endLine": 712,
"endColumn": 26,
"byteLength": 5
}
@@ -9435,9 +9504,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 697,
+ "startLine": 701,
"startColumn": 30,
- "endLine": 697,
+ "endLine": 701,
"endColumn": 64,
"byteLength": 34
}
@@ -9458,9 +9527,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 700,
+ "startLine": 704,
"startColumn": 22,
- "endLine": 700,
+ "endLine": 704,
"endColumn": 27,
"byteLength": 5
}
@@ -9481,9 +9550,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 703,
+ "startLine": 707,
"startColumn": 25,
- "endLine": 703,
+ "endLine": 707,
"endColumn": 31,
"byteLength": 6
}
@@ -9504,9 +9573,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 701,
+ "startLine": 705,
"startColumn": 29,
- "endLine": 701,
+ "endLine": 705,
"endColumn": 42,
"byteLength": 13
}
@@ -9527,9 +9596,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 704,
+ "startLine": 708,
"startColumn": 25,
- "endLine": 704,
+ "endLine": 708,
"endColumn": 37,
"byteLength": 12
}
@@ -9550,9 +9619,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 708,
+ "startLine": 712,
"startColumn": 21,
- "endLine": 708,
+ "endLine": 712,
"endColumn": 26,
"byteLength": 5
}
@@ -9575,9 +9644,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 698,
+ "startLine": 702,
"startColumn": 10,
- "endLine": 698,
+ "endLine": 702,
"endColumn": 17,
"byteLength": 7
}
@@ -9598,9 +9667,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 708,
+ "startLine": 712,
"startColumn": 21,
- "endLine": 708,
+ "endLine": 712,
"endColumn": 26,
"byteLength": 5
}
@@ -9621,9 +9690,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 708,
+ "startLine": 712,
"startColumn": 21,
- "endLine": 708,
+ "endLine": 712,
"endColumn": 26,
"byteLength": 5
}
@@ -9644,9 +9713,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 729,
+ "startLine": 733,
"startColumn": 15,
- "endLine": 729,
+ "endLine": 733,
"endColumn": 20,
"byteLength": 5
}
@@ -9667,9 +9736,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 725,
+ "startLine": 729,
"startColumn": 26,
- "endLine": 725,
+ "endLine": 729,
"endColumn": 36,
"byteLength": 10
}
@@ -9690,9 +9759,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 726,
+ "startLine": 730,
"startColumn": 24,
- "endLine": 726,
+ "endLine": 730,
"endColumn": 81,
"byteLength": 57
}
@@ -9713,9 +9782,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 729,
+ "startLine": 733,
"startColumn": 15,
- "endLine": 729,
+ "endLine": 733,
"endColumn": 20,
"byteLength": 5
}
@@ -9738,9 +9807,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 727,
+ "startLine": 731,
"startColumn": 10,
- "endLine": 727,
+ "endLine": 731,
"endColumn": 17,
"byteLength": 7
}
@@ -10350,9 +10419,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 737,
+ "startLine": 741,
"startColumn": 11,
- "endLine": 737,
+ "endLine": 741,
"endColumn": 16,
"byteLength": 5
}
@@ -10373,9 +10442,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 735,
+ "startLine": 739,
"startColumn": 12,
- "endLine": 735,
+ "endLine": 739,
"endColumn": 19,
"byteLength": 7
}
@@ -10398,9 +10467,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 735,
+ "startLine": 739,
"startColumn": 12,
- "endLine": 735,
+ "endLine": 739,
"endColumn": 19,
"byteLength": 7
}
@@ -10423,9 +10492,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 735,
+ "startLine": 739,
"startColumn": 21,
- "endLine": 735,
+ "endLine": 739,
"endColumn": 37,
"byteLength": 16
}
@@ -10446,9 +10515,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 769,
+ "startLine": 773,
"startColumn": 14,
- "endLine": 769,
+ "endLine": 773,
"endColumn": 22,
"byteLength": 8
}
@@ -10469,9 +10538,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 765,
+ "startLine": 769,
"startColumn": 23,
- "endLine": 765,
+ "endLine": 769,
"endColumn": 42,
"byteLength": 19
}
@@ -10492,9 +10561,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 766,
+ "startLine": 770,
"startColumn": 10,
- "endLine": 766,
+ "endLine": 770,
"endColumn": 17,
"byteLength": 7
}
@@ -10517,9 +10586,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 766,
+ "startLine": 770,
"startColumn": 10,
- "endLine": 766,
+ "endLine": 770,
"endColumn": 17,
"byteLength": 7
}
@@ -10542,9 +10611,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 767,
+ "startLine": 771,
"startColumn": 10,
- "endLine": 767,
+ "endLine": 771,
"endColumn": 24,
"byteLength": 14
}
@@ -10565,9 +10634,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 749,
+ "startLine": 753,
"startColumn": 11,
- "endLine": 749,
+ "endLine": 753,
"endColumn": 17,
"byteLength": 6
}
@@ -10588,9 +10657,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 742,
+ "startLine": 746,
"startColumn": 23,
- "endLine": 742,
+ "endLine": 746,
"endColumn": 41,
"byteLength": 18
}
@@ -10611,9 +10680,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 747,
+ "startLine": 751,
"startColumn": 26,
- "endLine": 747,
+ "endLine": 751,
"endColumn": 38,
"byteLength": 12
}
@@ -10634,9 +10703,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 743,
+ "startLine": 747,
"startColumn": 10,
- "endLine": 743,
+ "endLine": 747,
"endColumn": 17,
"byteLength": 7
}
@@ -10659,9 +10728,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 743,
+ "startLine": 747,
"startColumn": 10,
- "endLine": 743,
+ "endLine": 747,
"endColumn": 17,
"byteLength": 7
}
@@ -10684,9 +10753,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 745,
+ "startLine": 749,
"startColumn": 10,
- "endLine": 745,
+ "endLine": 749,
"endColumn": 29,
"byteLength": 19
}
@@ -10709,9 +10778,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 745,
+ "startLine": 749,
"startColumn": 31,
- "endLine": 745,
+ "endLine": 749,
"endColumn": 48,
"byteLength": 17
}
@@ -13572,9 +13641,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 820,
+ "startLine": 824,
"startColumn": 11,
- "endLine": 820,
+ "endLine": 824,
"endColumn": 18,
"byteLength": 7
}
@@ -13595,9 +13664,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 813,
+ "startLine": 817,
"startColumn": 27,
- "endLine": 813,
+ "endLine": 817,
"endColumn": 48,
"byteLength": 21
}
@@ -13618,9 +13687,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 814,
+ "startLine": 818,
"startColumn": 25,
- "endLine": 814,
+ "endLine": 818,
"endColumn": 45,
"byteLength": 20
}
@@ -13641,9 +13710,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 817,
+ "startLine": 821,
"startColumn": 36,
- "endLine": 818,
+ "endLine": 822,
"endColumn": 53,
"byteLength": 70
}
@@ -13664,9 +13733,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 815,
+ "startLine": 819,
"startColumn": 10,
- "endLine": 815,
+ "endLine": 819,
"endColumn": 22,
"byteLength": 12
}
@@ -13689,9 +13758,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 815,
+ "startLine": 819,
"startColumn": 10,
- "endLine": 815,
+ "endLine": 819,
"endColumn": 22,
"byteLength": 12
}
@@ -13714,9 +13783,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 816,
+ "startLine": 820,
"startColumn": 10,
- "endLine": 816,
+ "endLine": 820,
"endColumn": 17,
"byteLength": 7
}
@@ -13737,9 +13806,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 833,
+ "startLine": 837,
"startColumn": 11,
- "endLine": 833,
+ "endLine": 837,
"endColumn": 19,
"byteLength": 8
}
@@ -13760,9 +13829,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 825,
+ "startLine": 829,
"startColumn": 27,
- "endLine": 825,
+ "endLine": 829,
"endColumn": 48,
"byteLength": 21
}
@@ -13783,9 +13852,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 826,
+ "startLine": 830,
"startColumn": 25,
- "endLine": 826,
+ "endLine": 830,
"endColumn": 57,
"byteLength": 32
}
@@ -13806,9 +13875,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 827,
+ "startLine": 831,
"startColumn": 35,
- "endLine": 827,
+ "endLine": 831,
"endColumn": 49,
"byteLength": 14
}
@@ -13829,9 +13898,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 830,
+ "startLine": 834,
"startColumn": 36,
- "endLine": 831,
+ "endLine": 835,
"endColumn": 53,
"byteLength": 70
}
@@ -13852,9 +13921,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 828,
+ "startLine": 832,
"startColumn": 10,
- "endLine": 828,
+ "endLine": 832,
"endColumn": 22,
"byteLength": 12
}
@@ -13877,9 +13946,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 828,
+ "startLine": 832,
"startColumn": 10,
- "endLine": 828,
+ "endLine": 832,
"endColumn": 22,
"byteLength": 12
}
@@ -13902,9 +13971,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 829,
+ "startLine": 833,
"startColumn": 10,
- "endLine": 829,
+ "endLine": 833,
"endColumn": 17,
"byteLength": 7
}
@@ -14234,9 +14303,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 808,
+ "startLine": 812,
"startColumn": 11,
- "endLine": 808,
+ "endLine": 812,
"endColumn": 25,
"byteLength": 14
}
@@ -14259,9 +14328,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 808,
+ "startLine": 812,
"startColumn": 11,
- "endLine": 808,
+ "endLine": 812,
"endColumn": 25,
"byteLength": 14
}
@@ -14284,9 +14353,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 808,
+ "startLine": 812,
"startColumn": 11,
- "endLine": 808,
+ "endLine": 812,
"endColumn": 25,
"byteLength": 14
}
@@ -14307,9 +14376,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 785,
+ "startLine": 789,
"startColumn": 25,
- "endLine": 785,
+ "endLine": 789,
"endColumn": 39,
"byteLength": 14
}
@@ -14330,9 +14399,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 787,
+ "startLine": 791,
"startColumn": 4,
- "endLine": 788,
+ "endLine": 792,
"endColumn": 54,
"byteLength": 84
}
@@ -14353,9 +14422,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 794,
+ "startLine": 798,
"startColumn": 26,
- "endLine": 794,
+ "endLine": 798,
"endColumn": 44,
"byteLength": 18
}
@@ -14376,9 +14445,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 801,
+ "startLine": 805,
"startColumn": 29,
- "endLine": 801,
+ "endLine": 805,
"endColumn": 48,
"byteLength": 19
}
@@ -14399,9 +14468,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 798,
+ "startLine": 802,
"startColumn": 24,
- "endLine": 798,
+ "endLine": 802,
"endColumn": 44,
"byteLength": 20
}
@@ -14422,9 +14491,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 799,
+ "startLine": 803,
"startColumn": 25,
- "endLine": 799,
+ "endLine": 803,
"endColumn": 37,
"byteLength": 12
}
@@ -14445,9 +14514,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 804,
+ "startLine": 808,
"startColumn": 29,
- "endLine": 804,
+ "endLine": 808,
"endColumn": 55,
"byteLength": 26
}
@@ -14468,9 +14537,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 795,
+ "startLine": 799,
"startColumn": 12,
- "endLine": 795,
+ "endLine": 799,
"endColumn": 28,
"byteLength": 16
}
@@ -14491,9 +14560,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 790,
+ "startLine": 794,
"startColumn": 10,
- "endLine": 790,
+ "endLine": 794,
"endColumn": 26,
"byteLength": 16
}
@@ -14514,9 +14583,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 808,
+ "startLine": 812,
"startColumn": 11,
- "endLine": 808,
+ "endLine": 812,
"endColumn": 25,
"byteLength": 14
}
@@ -14539,9 +14608,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 795,
+ "startLine": 799,
"startColumn": 12,
- "endLine": 795,
+ "endLine": 799,
"endColumn": 28,
"byteLength": 16
}
@@ -14564,9 +14633,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 796,
+ "startLine": 800,
"startColumn": 12,
- "endLine": 796,
+ "endLine": 800,
"endColumn": 19,
"byteLength": 7
}
@@ -14589,9 +14658,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 790,
+ "startLine": 794,
"startColumn": 10,
- "endLine": 790,
+ "endLine": 794,
"endColumn": 26,
"byteLength": 16
}
@@ -14614,9 +14683,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 791,
+ "startLine": 795,
"startColumn": 10,
- "endLine": 791,
+ "endLine": 795,
"endColumn": 17,
"byteLength": 7
}
@@ -14639,9 +14708,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 803,
+ "startLine": 807,
"startColumn": 12,
- "endLine": 803,
+ "endLine": 807,
"endColumn": 19,
"byteLength": 7
}
@@ -14664,9 +14733,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 789,
+ "startLine": 793,
"startColumn": 12,
- "endLine": 789,
+ "endLine": 793,
"endColumn": 19,
"byteLength": 7
}
@@ -14689,9 +14758,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 808,
+ "startLine": 812,
"startColumn": 11,
- "endLine": 808,
+ "endLine": 812,
"endColumn": 25,
"byteLength": 14
}
@@ -14714,9 +14783,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 808,
+ "startLine": 812,
"startColumn": 11,
- "endLine": 808,
+ "endLine": 812,
"endColumn": 25,
"byteLength": 14
}
@@ -14739,9 +14808,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 808,
+ "startLine": 812,
"startColumn": 11,
- "endLine": 808,
+ "endLine": 812,
"endColumn": 25,
"byteLength": 14
}
@@ -14762,9 +14831,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 567,
+ "startLine": 570,
"startColumn": 11,
- "endLine": 567,
+ "endLine": 570,
"endColumn": 17,
"byteLength": 6
}
@@ -14785,9 +14854,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 563,
+ "startLine": 566,
"startColumn": 25,
- "endLine": 563,
+ "endLine": 566,
"endColumn": 50,
"byteLength": 25
}
@@ -14808,9 +14877,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 564,
+ "startLine": 567,
"startColumn": 10,
- "endLine": 564,
+ "endLine": 567,
"endColumn": 23,
"byteLength": 13
}
@@ -14833,9 +14902,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 564,
+ "startLine": 567,
"startColumn": 10,
- "endLine": 564,
+ "endLine": 567,
"endColumn": 23,
"byteLength": 13
}
@@ -14858,9 +14927,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 565,
+ "startLine": 568,
"startColumn": 10,
- "endLine": 565,
+ "endLine": 568,
"endColumn": 17,
"byteLength": 7
}
@@ -14881,9 +14950,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 663,
+ "startLine": 667,
"startColumn": 12,
- "endLine": 663,
+ "endLine": 667,
"endColumn": 17,
"byteLength": 5
}
@@ -14904,9 +14973,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 658,
+ "startLine": 662,
"startColumn": 34,
- "endLine": 658,
+ "endLine": 662,
"endColumn": 57,
"byteLength": 23
}
@@ -14927,9 +14996,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 659,
+ "startLine": 663,
"startColumn": 10,
- "endLine": 659,
+ "endLine": 663,
"endColumn": 29,
"byteLength": 19
}
@@ -14952,9 +15021,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 659,
+ "startLine": 663,
"startColumn": 10,
- "endLine": 659,
+ "endLine": 663,
"endColumn": 29,
"byteLength": 19
}
@@ -14975,9 +15044,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 625,
+ "startLine": 629,
"startColumn": 12,
- "endLine": 625,
+ "endLine": 629,
"endColumn": 22,
"byteLength": 10
}
@@ -14998,9 +15067,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 623,
+ "startLine": 627,
"startColumn": 28,
- "endLine": 623,
+ "endLine": 627,
"endColumn": 34,
"byteLength": 6
}
@@ -15021,9 +15090,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 625,
+ "startLine": 629,
"startColumn": 12,
- "endLine": 625,
+ "endLine": 629,
"endColumn": 22,
"byteLength": 10
}
@@ -15031,6 +15100,29 @@
}
]
},
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "terminates \\false." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 625,
+ "startColumn": 13,
+ "endLine": 625,
+ "endColumn": 19,
+ "byteLength": 6
+ }
+ }
+ }
+ ]
+ },
{
"ruleId": "user-spec",
"kind": "pass",
@@ -16491,9 +16583,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -16514,9 +16606,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -16539,9 +16631,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -16564,9 +16656,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -16589,9 +16681,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -16614,9 +16706,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -16637,9 +16729,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 840,
+ "startLine": 844,
"startColumn": 4,
- "endLine": 840,
+ "endLine": 844,
"endColumn": 54,
"byteLength": 50
}
@@ -16660,9 +16752,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 842,
+ "startLine": 846,
"startColumn": 4,
- "endLine": 842,
+ "endLine": 846,
"endColumn": 66,
"byteLength": 62
}
@@ -16683,9 +16775,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 850,
+ "startLine": 854,
"startColumn": 28,
- "endLine": 850,
+ "endLine": 854,
"endColumn": 46,
"byteLength": 18
}
@@ -16706,9 +16798,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 855,
+ "startLine": 859,
"startColumn": 29,
- "endLine": 855,
+ "endLine": 859,
"endColumn": 57,
"byteLength": 28
}
@@ -16729,9 +16821,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 856,
+ "startLine": 860,
"startColumn": 32,
- "endLine": 856,
+ "endLine": 860,
"endColumn": 54,
"byteLength": 22
}
@@ -16752,9 +16844,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 857,
+ "startLine": 861,
"startColumn": 26,
- "endLine": 857,
+ "endLine": 861,
"endColumn": 44,
"byteLength": 18
}
@@ -16775,9 +16867,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 862,
+ "startLine": 866,
"startColumn": 29,
- "endLine": 862,
+ "endLine": 866,
"endColumn": 57,
"byteLength": 28
}
@@ -16798,9 +16890,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 863,
+ "startLine": 867,
"startColumn": 32,
- "endLine": 863,
+ "endLine": 867,
"endColumn": 54,
"byteLength": 22
}
@@ -16821,9 +16913,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 864,
+ "startLine": 868,
"startColumn": 29,
- "endLine": 864,
+ "endLine": 868,
"endColumn": 48,
"byteLength": 19
}
@@ -16844,9 +16936,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 870,
+ "startLine": 874,
"startColumn": 29,
- "endLine": 870,
+ "endLine": 874,
"endColumn": 57,
"byteLength": 28
}
@@ -16867,9 +16959,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 872,
+ "startLine": 876,
"startColumn": 6,
- "endLine": 872,
+ "endLine": 876,
"endColumn": 42,
"byteLength": 36
}
@@ -16890,9 +16982,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 882,
+ "startLine": 886,
"startColumn": 29,
- "endLine": 882,
+ "endLine": 886,
"endColumn": 57,
"byteLength": 28
}
@@ -16913,9 +17005,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 852,
+ "startLine": 856,
"startColumn": 25,
- "endLine": 852,
+ "endLine": 856,
"endColumn": 41,
"byteLength": 16
}
@@ -16936,9 +17028,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 853,
+ "startLine": 857,
"startColumn": 23,
- "endLine": 853,
+ "endLine": 857,
"endColumn": 39,
"byteLength": 16
}
@@ -16959,9 +17051,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 860,
+ "startLine": 864,
"startColumn": 24,
- "endLine": 860,
+ "endLine": 864,
"endColumn": 44,
"byteLength": 20
}
@@ -16982,9 +17074,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 867,
+ "startLine": 871,
"startColumn": 25,
- "endLine": 867,
+ "endLine": 871,
"endColumn": 41,
"byteLength": 16
}
@@ -17005,9 +17097,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 868,
+ "startLine": 872,
"startColumn": 23,
- "endLine": 868,
+ "endLine": 872,
"endColumn": 39,
"byteLength": 16
}
@@ -17028,9 +17120,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 876,
+ "startLine": 880,
"startColumn": 40,
- "endLine": 877,
+ "endLine": 881,
"endColumn": 71,
"byteLength": 99
}
@@ -17051,9 +17143,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 880,
+ "startLine": 884,
"startColumn": 29,
- "endLine": 880,
+ "endLine": 884,
"endColumn": 53,
"byteLength": 24
}
@@ -17074,9 +17166,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 886,
+ "startLine": 890,
"startColumn": 25,
- "endLine": 886,
+ "endLine": 890,
"endColumn": 41,
"byteLength": 16
}
@@ -17097,9 +17189,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 888,
+ "startLine": 892,
"startColumn": 6,
- "endLine": 888,
+ "endLine": 892,
"endColumn": 43,
"byteLength": 37
}
@@ -17120,9 +17212,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 858,
+ "startLine": 862,
"startColumn": 12,
- "endLine": 858,
+ "endLine": 862,
"endColumn": 28,
"byteLength": 16
}
@@ -17143,9 +17235,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 843,
+ "startLine": 847,
"startColumn": 10,
- "endLine": 843,
+ "endLine": 847,
"endColumn": 26,
"byteLength": 16
}
@@ -17166,9 +17258,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 884,
+ "startLine": 888,
"startColumn": 12,
- "endLine": 884,
+ "endLine": 888,
"endColumn": 19,
"byteLength": 7
}
@@ -17189,9 +17281,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -17212,9 +17304,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 851,
+ "startLine": 855,
"startColumn": 12,
- "endLine": 851,
+ "endLine": 855,
"endColumn": 19,
"byteLength": 7
}
@@ -17235,9 +17327,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 874,
+ "startLine": 878,
"startColumn": 12,
- "endLine": 874,
+ "endLine": 878,
"endColumn": 19,
"byteLength": 7
}
@@ -17260,9 +17352,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 858,
+ "startLine": 862,
"startColumn": 12,
- "endLine": 858,
+ "endLine": 862,
"endColumn": 28,
"byteLength": 16
}
@@ -17285,9 +17377,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 859,
+ "startLine": 863,
"startColumn": 12,
- "endLine": 859,
+ "endLine": 863,
"endColumn": 19,
"byteLength": 7
}
@@ -17310,9 +17402,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 843,
+ "startLine": 847,
"startColumn": 10,
- "endLine": 843,
+ "endLine": 847,
"endColumn": 26,
"byteLength": 16
}
@@ -17335,9 +17427,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 844,
+ "startLine": 848,
"startColumn": 10,
- "endLine": 844,
+ "endLine": 848,
"endColumn": 31,
"byteLength": 21
}
@@ -17360,9 +17452,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 844,
+ "startLine": 848,
"startColumn": 33,
- "endLine": 844,
+ "endLine": 848,
"endColumn": 60,
"byteLength": 27
}
@@ -17385,9 +17477,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 846,
+ "startLine": 850,
"startColumn": 10,
- "endLine": 846,
+ "endLine": 850,
"endColumn": 20,
"byteLength": 10
}
@@ -17410,9 +17502,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 884,
+ "startLine": 888,
"startColumn": 12,
- "endLine": 884,
+ "endLine": 888,
"endColumn": 19,
"byteLength": 7
}
@@ -17435,9 +17527,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 884,
+ "startLine": 888,
"startColumn": 21,
- "endLine": 884,
+ "endLine": 888,
"endColumn": 31,
"byteLength": 10
}
@@ -17460,9 +17552,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 866,
+ "startLine": 870,
"startColumn": 12,
- "endLine": 866,
+ "endLine": 870,
"endColumn": 19,
"byteLength": 7
}
@@ -17485,9 +17577,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 851,
+ "startLine": 855,
"startColumn": 12,
- "endLine": 851,
+ "endLine": 855,
"endColumn": 19,
"byteLength": 7
}
@@ -17510,9 +17602,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 851,
+ "startLine": 855,
"startColumn": 21,
- "endLine": 851,
+ "endLine": 855,
"endColumn": 31,
"byteLength": 10
}
@@ -17535,9 +17627,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 874,
+ "startLine": 878,
"startColumn": 12,
- "endLine": 874,
+ "endLine": 878,
"endColumn": 19,
"byteLength": 7
}
@@ -17560,9 +17652,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 875,
+ "startLine": 879,
"startColumn": 12,
- "endLine": 875,
+ "endLine": 879,
"endColumn": 39,
"byteLength": 27
}
@@ -17585,9 +17677,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -17610,9 +17702,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -17635,9 +17727,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 890,
+ "startLine": 894,
"startColumn": 13,
- "endLine": 890,
+ "endLine": 894,
"endColumn": 21,
"byteLength": 8
}
@@ -17871,9 +17963,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 611,
+ "startLine": 614,
"startColumn": 11,
- "endLine": 611,
+ "endLine": 614,
"endColumn": 17,
"byteLength": 6
}
@@ -17894,9 +17986,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 611,
+ "startLine": 614,
"startColumn": 11,
- "endLine": 611,
+ "endLine": 614,
"endColumn": 17,
"byteLength": 6
}
@@ -17917,9 +18009,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 611,
+ "startLine": 614,
"startColumn": 11,
- "endLine": 611,
+ "endLine": 614,
"endColumn": 17,
"byteLength": 6
}
@@ -17940,9 +18032,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 611,
+ "startLine": 614,
"startColumn": 11,
- "endLine": 611,
+ "endLine": 614,
"endColumn": 17,
"byteLength": 6
}
@@ -17963,9 +18055,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 570,
+ "startLine": 573,
"startColumn": 23,
- "endLine": 570,
+ "endLine": 573,
"endColumn": 46,
"byteLength": 23
}
@@ -17986,9 +18078,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 571,
+ "startLine": 574,
"startColumn": 24,
- "endLine": 571,
+ "endLine": 574,
"endColumn": 48,
"byteLength": 24
}
@@ -18009,9 +18101,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 583,
+ "startLine": 586,
"startColumn": 6,
- "endLine": 583,
+ "endLine": 586,
"endColumn": 44,
"byteLength": 38
}
@@ -18032,9 +18124,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 590,
+ "startLine": 593,
"startColumn": 31,
- "endLine": 590,
+ "endLine": 593,
"endColumn": 78,
"byteLength": 47
}
@@ -18055,9 +18147,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 598,
+ "startLine": 601,
"startColumn": 28,
- "endLine": 598,
+ "endLine": 601,
"endColumn": 44,
"byteLength": 16
}
@@ -18078,9 +18170,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 599,
+ "startLine": 602,
"startColumn": 37,
- "endLine": 599,
+ "endLine": 602,
"endColumn": 55,
"byteLength": 18
}
@@ -18101,9 +18193,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 600,
+ "startLine": 603,
"startColumn": 27,
- "endLine": 600,
+ "endLine": 603,
"endColumn": 73,
"byteLength": 46
}
@@ -18124,9 +18216,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 580,
+ "startLine": 583,
"startColumn": 30,
- "endLine": 580,
+ "endLine": 583,
"endColumn": 59,
"byteLength": 29
}
@@ -18147,9 +18239,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 587,
+ "startLine": 590,
"startColumn": 19,
- "endLine": 587,
+ "endLine": 590,
"endColumn": 32,
"byteLength": 13
}
@@ -18170,9 +18262,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 588,
+ "startLine": 591,
"startColumn": 23,
- "endLine": 588,
+ "endLine": 591,
"endColumn": 39,
"byteLength": 16
}
@@ -18193,9 +18285,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 595,
+ "startLine": 598,
"startColumn": 19,
- "endLine": 595,
+ "endLine": 598,
"endColumn": 32,
"byteLength": 13
}
@@ -18216,9 +18308,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 596,
+ "startLine": 599,
"startColumn": 23,
- "endLine": 596,
+ "endLine": 599,
"endColumn": 39,
"byteLength": 16
}
@@ -18239,9 +18331,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 609,
+ "startLine": 612,
"startColumn": 16,
- "endLine": 609,
+ "endLine": 612,
"endColumn": 28,
"byteLength": 12
}
@@ -18262,9 +18354,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 573,
+ "startLine": 576,
"startColumn": 10,
- "endLine": 573,
+ "endLine": 576,
"endColumn": 17,
"byteLength": 7
}
@@ -18285,9 +18377,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 585,
+ "startLine": 588,
"startColumn": 12,
- "endLine": 585,
+ "endLine": 588,
"endColumn": 19,
"byteLength": 7
}
@@ -18308,9 +18400,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 602,
+ "startLine": 605,
"startColumn": 12,
- "endLine": 602,
+ "endLine": 605,
"endColumn": 19,
"byteLength": 7
}
@@ -18331,9 +18423,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 592,
+ "startLine": 595,
"startColumn": 12,
- "endLine": 592,
+ "endLine": 595,
"endColumn": 19,
"byteLength": 7
}
@@ -18356,9 +18448,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 573,
+ "startLine": 576,
"startColumn": 10,
- "endLine": 573,
+ "endLine": 576,
"endColumn": 17,
"byteLength": 7
}
@@ -18381,9 +18473,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 573,
+ "startLine": 576,
"startColumn": 19,
- "endLine": 573,
+ "endLine": 576,
"endColumn": 32,
"byteLength": 13
}
@@ -18406,9 +18498,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 573,
+ "startLine": 576,
"startColumn": 34,
- "endLine": 573,
+ "endLine": 576,
"endColumn": 44,
"byteLength": 10
}
@@ -18431,9 +18523,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 576,
+ "startLine": 579,
"startColumn": 10,
- "endLine": 576,
+ "endLine": 579,
"endColumn": 28,
"byteLength": 18
}
@@ -18456,9 +18548,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 585,
+ "startLine": 588,
"startColumn": 12,
- "endLine": 585,
+ "endLine": 588,
"endColumn": 19,
"byteLength": 7
}
@@ -18481,9 +18573,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 586,
+ "startLine": 589,
"startColumn": 12,
- "endLine": 586,
+ "endLine": 589,
"endColumn": 22,
"byteLength": 10
}
@@ -18506,9 +18598,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 602,
+ "startLine": 605,
"startColumn": 12,
- "endLine": 602,
+ "endLine": 605,
"endColumn": 19,
"byteLength": 7
}
@@ -18531,9 +18623,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 602,
+ "startLine": 605,
"startColumn": 21,
- "endLine": 602,
+ "endLine": 605,
"endColumn": 34,
"byteLength": 13
}
@@ -18556,9 +18648,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 605,
+ "startLine": 608,
"startColumn": 12,
- "endLine": 605,
+ "endLine": 608,
"endColumn": 30,
"byteLength": 18
}
@@ -18581,9 +18673,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 592,
+ "startLine": 595,
"startColumn": 12,
- "endLine": 592,
+ "endLine": 595,
"endColumn": 19,
"byteLength": 7
}
@@ -18606,9 +18698,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 592,
+ "startLine": 595,
"startColumn": 21,
- "endLine": 592,
+ "endLine": 595,
"endColumn": 31,
"byteLength": 10
}
@@ -18629,9 +18721,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 572,
+ "startLine": 575,
"startColumn": 12,
- "endLine": 572,
+ "endLine": 575,
"endColumn": 25,
"byteLength": 13
}
@@ -18652,9 +18744,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 611,
+ "startLine": 614,
"startColumn": 11,
- "endLine": 611,
+ "endLine": 614,
"endColumn": 17,
"byteLength": 6
}
@@ -18675,9 +18767,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 601,
+ "startLine": 604,
"startColumn": 14,
- "endLine": 601,
+ "endLine": 604,
"endColumn": 27,
"byteLength": 13
}
@@ -18698,9 +18790,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 611,
+ "startLine": 614,
"startColumn": 11,
- "endLine": 611,
+ "endLine": 614,
"endColumn": 17,
"byteLength": 6
}
@@ -30701,9 +30793,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 633,
+ "startLine": 637,
"startColumn": 11,
- "endLine": 633,
+ "endLine": 637,
"endColumn": 17,
"byteLength": 6
}
@@ -30724,9 +30816,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 629,
+ "startLine": 633,
"startColumn": 5,
- "endLine": 629,
+ "endLine": 633,
"endColumn": 51,
"byteLength": 46
}
@@ -30747,9 +30839,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 633,
+ "startLine": 637,
"startColumn": 11,
- "endLine": 633,
+ "endLine": 637,
"endColumn": 17,
"byteLength": 6
}
@@ -30772,9 +30864,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 630,
+ "startLine": 634,
"startColumn": 10,
- "endLine": 630,
+ "endLine": 634,
"endColumn": 17,
"byteLength": 7
}
@@ -30795,9 +30887,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 619,
+ "startLine": 622,
"startColumn": 11,
- "endLine": 619,
+ "endLine": 622,
"endColumn": 19,
"byteLength": 8
}
@@ -30818,9 +30910,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 614,
+ "startLine": 617,
"startColumn": 23,
- "endLine": 614,
+ "endLine": 617,
"endColumn": 46,
"byteLength": 23
}
@@ -30841,9 +30933,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 617,
+ "startLine": 620,
"startColumn": 30,
- "endLine": 617,
+ "endLine": 620,
"endColumn": 59,
"byteLength": 29
}
@@ -30864,9 +30956,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 615,
+ "startLine": 618,
"startColumn": 10,
- "endLine": 615,
+ "endLine": 618,
"endColumn": 17,
"byteLength": 7
}
@@ -30889,9 +30981,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 615,
+ "startLine": 618,
"startColumn": 10,
- "endLine": 615,
+ "endLine": 618,
"endColumn": 17,
"byteLength": 7
}
@@ -30914,9 +31006,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 615,
+ "startLine": 618,
"startColumn": 19,
- "endLine": 615,
+ "endLine": 618,
"endColumn": 32,
"byteLength": 13
}
@@ -30937,9 +31029,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 778,
+ "startLine": 782,
"startColumn": 14,
- "endLine": 778,
+ "endLine": 782,
"endColumn": 22,
"byteLength": 8
}
@@ -30960,9 +31052,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 774,
+ "startLine": 778,
"startColumn": 23,
- "endLine": 774,
+ "endLine": 778,
"endColumn": 42,
"byteLength": 19
}
@@ -30983,9 +31075,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 775,
+ "startLine": 779,
"startColumn": 10,
- "endLine": 775,
+ "endLine": 779,
"endColumn": 17,
"byteLength": 7
}
@@ -31008,9 +31100,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 775,
+ "startLine": 779,
"startColumn": 10,
- "endLine": 775,
+ "endLine": 779,
"endColumn": 17,
"byteLength": 7
}
@@ -31033,9 +31125,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 776,
+ "startLine": 780,
"startColumn": 10,
- "endLine": 776,
+ "endLine": 780,
"endColumn": 21,
"byteLength": 11
}
@@ -31056,9 +31148,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 760,
+ "startLine": 764,
"startColumn": 11,
- "endLine": 760,
+ "endLine": 764,
"endColumn": 17,
"byteLength": 6
}
@@ -31079,9 +31171,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 757,
+ "startLine": 761,
"startColumn": 10,
- "endLine": 757,
+ "endLine": 761,
"endColumn": 17,
"byteLength": 7
}
@@ -31104,9 +31196,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 757,
+ "startLine": 761,
"startColumn": 10,
- "endLine": 757,
+ "endLine": 761,
"endColumn": 17,
"byteLength": 7
}
@@ -31129,9 +31221,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 758,
+ "startLine": 762,
"startColumn": 10,
- "endLine": 758,
+ "endLine": 762,
"endColumn": 17,
"byteLength": 7
}
@@ -31154,9 +31246,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 758,
+ "startLine": 762,
"startColumn": 19,
- "endLine": 758,
+ "endLine": 762,
"endColumn": 36,
"byteLength": 17
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
index abdd33ee5e2..b9004920458 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle
@@ -1,10 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing terminates_call_options.c (with preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:543: Warning:
- Neither code nor explicit terminates for function exit,
- generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:715: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:719: Warning:
Neither code nor explicit exits and terminates for function div,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
@@ -42,11 +39,17 @@ Prove: true.
Function libc_call
------------------------------------------------------------
-Goal Termination-condition (file terminates_call_options.c, line 36) in 'libc_call':
+Goal Termination-condition (file terminates_call_options.c, line 36) in 'libc_call' (1/2):
Prove: true.
------------------------------------------------------------
+Goal Termination-condition (file terminates_call_options.c, line 36) in 'libc_call' (2/2):
+Call terminates at line 39
+Prove: false.
+
+------------------------------------------------------------
+
Goal Instance of 'Pre-condition 'denom_nonzero' in 'div'' in 'libc_call' at call 'div' (file terminates_call_options.c, line 38)
:
Prove: true.
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 ae3902f9322..caaa30dd88d 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
@@ -4,10 +4,7 @@
[kernel:annot:missing-spec] terminates_call_options.c:17: Warning:
Neither code nor explicit exits and terminates for function declaration,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:543: Warning:
- Neither code nor explicit terminates for function exit,
- generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:715: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:719: Warning:
Neither code nor explicit exits and terminates for function div,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
@@ -54,11 +51,17 @@ Prove: true.
Function libc_call
------------------------------------------------------------
-Goal Termination-condition (file terminates_call_options.c, line 36) in 'libc_call':
+Goal Termination-condition (file terminates_call_options.c, line 36) in 'libc_call' (1/2):
Prove: true.
------------------------------------------------------------
+Goal Termination-condition (file terminates_call_options.c, line 36) in 'libc_call' (2/2):
+Call terminates at line 39
+Prove: false.
+
+------------------------------------------------------------
+
Goal Exit-condition (generated) in 'libc_call':
Prove: false.
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
index d243e276923..9cf86ae72c1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle
@@ -1,10 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing terminates_call_options.c (with preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:543: Warning:
- Neither code nor explicit terminates for function exit,
- generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:715: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:719: Warning:
Neither code nor explicit exits and terminates for function div,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
@@ -12,20 +9,21 @@
Missing terminates clause on call to declaration, defaults to \false
[wp] terminates_call_options.c:29: Warning:
Missing terminates clause on call to definition, defaults to \false
-[wp] 6 goals scheduled
+[wp] 7 goals scheduled
[wp] [Valid] typed_definition_assigns (Qed)
[wp] [Unsuccess] typed_call_declaration_terminates (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_call_definition_terminates (Alt-Ergo) (Cached)
-[wp] [Valid] typed_libc_call_terminates (Qed)
+[wp] [Valid] typed_libc_call_terminates_part1 (Qed)
+[wp] [Unsuccess] typed_libc_call_terminates_part2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_libc_call_call_div_requires_denom_nonzero (Qed)
[wp] [Valid] typed_libc_call_call_div_requires_no_overflow (Qed)
-[wp] Proved goals: 4 / 6
+[wp] Proved goals: 4 / 7
Qed: 4
- Unsuccess: 2
+ Unsuccess: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
definition 1 - 1 100%
call_declaration - - 1 0.0%
call_definition - - 1 0.0%
- libc_call 3 - 3 100%
+ libc_call 3 - 4 75.0%
------------------------------------------------------------
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 386bd2017c8..21329b07a96 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
@@ -4,10 +4,7 @@
[kernel:annot:missing-spec] terminates_call_options.c:17: Warning:
Neither code nor explicit exits and terminates for function declaration,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:543: Warning:
- Neither code nor explicit terminates for function exit,
- generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:715: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:719: Warning:
Neither code nor explicit exits and terminates for function div,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
@@ -16,27 +13,28 @@
[wp] [Valid] Goal no_spec_generates_goal_exits (Cfg) (Unreachable)
[wp] terminates_call_options.c:33: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] 10 goals scheduled
+[wp] 11 goals scheduled
[wp] [Valid] typed_definition_assigns (Qed)
[wp] [Valid] typed_call_declaration_terminates (Qed)
[wp] [Valid] typed_call_declaration_exits (Qed)
[wp] [Valid] typed_call_definition_terminates (Qed)
[wp] [Valid] typed_call_definition_exits (Qed)
[wp] [Unsuccess] typed_no_spec_generates_goal_terminates (Alt-Ergo) (Cached)
-[wp] [Valid] typed_libc_call_terminates (Qed)
+[wp] [Valid] typed_libc_call_terminates_part1 (Qed)
+[wp] [Unsuccess] typed_libc_call_terminates_part2 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_libc_call_exits (Alt-Ergo) (Cached)
[wp] [Valid] typed_libc_call_call_div_requires_denom_nonzero (Qed)
[wp] [Valid] typed_libc_call_call_div_requires_no_overflow (Qed)
-[wp] Proved goals: 11 / 13
+[wp] Proved goals: 11 / 14
Terminating: 1
Unreachable: 2
Qed: 8
- Unsuccess: 2
+ Unsuccess: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
definition 1 - 1 100%
call_declaration 2 - 2 100%
call_definition 2 - 2 100%
no_spec_generates_goal - - 1 0.0%
- libc_call 3 - 4 75.0%
+ libc_call 3 - 5 60.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/issue-684-exit.c b/src/plugins/wp/tests/wp_bts/issue-684-exit.c
index 9776a399902..47f5f4c1a3d 100644
--- a/src/plugins/wp/tests/wp_bts/issue-684-exit.c
+++ b/src/plugins/wp/tests/wp_bts/issue-684-exit.c
@@ -3,6 +3,6 @@
@ exits \exit_status == state;
@ ensures \false;
*/
-void inconditional_exit(int state) {
+__attribute__((noreturn)) void inconditional_exit(int state) {
exit (state);
}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
index a569876861f..22a7a3d89d8 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
@@ -1,9 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing issue-684-exit.c (with preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:543: Warning:
- Neither code nor explicit terminates for function exit,
- generating default clauses. See -generated-spec-* options for more info
[wp] [Valid] Goal inconditional_exit_assigns_normal (Cfg) (Unreachable)
[wp] [Valid] Goal inconditional_exit_ensures (Cfg) (Unreachable)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
index 4a867b0febd..f53701b1b8e 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
@@ -1,9 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing issue-684-exit.c (with preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:543: Warning:
- Neither code nor explicit terminates for function exit,
- generating default clauses. See -generated-spec-* options for more info
[wp] [Valid] Goal inconditional_exit_assigns_normal (Cfg) (Unreachable)
[wp] [Valid] Goal inconditional_exit_ensures (Cfg) (Unreachable)
[wp] Warning: Missing RTE guards
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 4b450b8cdfe..88b5d0e3123 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1754,7 +1754,8 @@ extern void *realloc(void *ptr, size_t size);
*/
extern void *reallocarray(void *ptr, size_t nmemb, size_t size);
-/*@ exits status: \exit_status ≢ 0;
+/*@ terminates \false;
+ exits status: \exit_status ≢ 0;
ensures never_terminates: \false;
assigns \exit_status \from \nothing;
@@ -1769,14 +1770,16 @@ extern int atexit(void (*func)(void));
assigns \result \from \nothing; */
extern int at_quick_exit(void (*func)(void));
-/*@ exits status: \exit_status ≡ \old(status);
+/*@ terminates \false;
+ exits status: \exit_status ≡ \old(status);
ensures never_terminates: \false;
assigns \exit_status \from status;
*/
extern __attribute__((__noreturn__)) void exit(int status);
-/*@ ensures never_terminates: \false;
+/*@ terminates \false;
+ ensures never_terminates: \false;
assigns \nothing; */
extern __attribute__((__noreturn__)) void _Exit(int status);
@@ -1789,7 +1792,8 @@ int setenv(char const *name, char const *value, int overwrite);
int unsetenv(char const *name);
-/*@ ensures never_terminates: \false;
+/*@ terminates \false;
+ ensures never_terminates: \false;
assigns \nothing; */
extern __attribute__((__noreturn__)) void quick_exit(int status);
@@ -9714,7 +9718,8 @@ extern int execve(char const *path, char * const *argv, char * const *env);
*/
extern int execvp(char const *path, char * const *argv);
-/*@ ensures never_terminates: \false;
+/*@ terminates \false;
+ ensures never_terminates: \false;
assigns \nothing; */
extern __attribute__((__noreturn__)) void _exit(int __x0);
--
GitLab