diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 7a5d5138ee15f2eb3a3935ab37c82d596fdd2abb..4c33aba539b7f8afe6bf137ad3e8d23e07830666 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -252,6 +252,7 @@ share/libc/n1362.pdf: .ignore share/libc/net/if.h: CEA_LGPL share/libc/netdb.c: CEA_LGPL share/libc/netdb.h: CEA_LGPL +share/libc/netinet/in.c: CEA_LGPL share/libc/netinet/in.h: CEA_LGPL share/libc/netinet/ip.h: CEA_LGPL share/libc/netinet/tcp.h: CEA_LGPL diff --git a/share/libc/__fc_inet.h b/share/libc/__fc_inet.h index 5904cd5fff16da2ee40276eb02bdac5d8a5d6a7a..ad285285e0b0e835d88f471a3b4a01a846cb5765 100644 --- a/share/libc/__fc_inet.h +++ b/share/libc/__fc_inet.h @@ -76,18 +76,15 @@ struct sockaddr_in6 { // Non-POSIX #define INADDR_NONE ((in_addr_t) 0xffffffff) -#define IN6ADDR_ANY 0 -#define IN6ADDR_BROADCAST 0XFFFFFFFFFFFFFFFFULL +#define IN6ADDR_ANY_INIT {{0}} +#define IN6ADDR_LOOPBACK_INIT {{ 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1 }} #define INET6_ADDRSTRLEN 46 // Not required by POSIX #define INADDR_LOOPBACK (uint32_t)0x7F000001 -const struct in6_addr in6addr_any={{0}}; -const struct in6_addr in6addr_loopback= - {{0xFF,0xFF,0xFF,0xFF,0xFF,0xFF,0xFF,0xFF, - 0xFF,0xFF,0xFF,0xFF,0xFF,0xFF,0xFF,0xFF}} - ; +extern const struct in6_addr in6addr_any; +extern const struct in6_addr in6addr_loopback; struct ipv6_mreq { struct in6_addr ipv6mr_multiaddr; diff --git a/share/libc/__fc_runtime.c b/share/libc/__fc_runtime.c index 6c9dff3a43253b26f03383e547ca4ad30a721faa..fc29185b4ed23085903529b90f0bf401b98674c4 100644 --- a/share/libc/__fc_runtime.c +++ b/share/libc/__fc_runtime.c @@ -31,6 +31,7 @@ #include "locale.c" #include "math.c" #include "netdb.c" +#include "netinet/in.c" #include "signal.c" #include "stdio.c" #include "stdlib.c" diff --git a/share/libc/features.h b/share/libc/features.h index 33ba5c44519ca2dbf961e7feea81bca02f001f58..19fe84cea75cd452a0885c7f0fae822280ac9f88 100644 --- a/share/libc/features.h +++ b/share/libc/features.h @@ -34,27 +34,12 @@ #define __POP_FC_STDLIB #endif -#if defined(__clang__) && defined(__cplusplus) -# define __CLANG_IGNORE_ATTRS_PUSH__ \ -_Pragma("clang diagnostic push") \ -_Pragma("clang diagnostic ignored \"-Wunknown-attributes\"") -# define __CLANG_IGNORE_ATTRS_POP__ \ -_Pragma("clang diagnostic pop") -#else -# define __CLANG_IGNORE_ATTRS_PUSH__ -# define __CLANG_IGNORE_ATTRS_POP__ -#endif - #ifdef __cplusplus -# define __BEGIN_DECLS \ -extern "C" { \ - __CLANG_IGNORE_ATTRS_PUSH__ -# define __END_DECLS \ -__CLANG_IGNORE_ATTRS_POP__ \ -} +# define __BEGIN_DECLS extern "C" { +# define __END_DECLS } #else -# define __BEGIN_DECLS __CLANG_IGNORE_ATTRS_PUSH__ -# define __END_DECLS __CLANG_IGNORE_ATTRS_POP__ +# define __BEGIN_DECLS +# define __END_DECLS #endif #undef __LEAF diff --git a/share/libc/glob.c b/share/libc/glob.c index b4b55cda11a3ad9d9538da387aebb78926345d06..5eff2df86de7f9fd058f710691574e9354edb088 100644 --- a/share/libc/glob.c +++ b/share/libc/glob.c @@ -71,7 +71,7 @@ int glob(const char *pattern, int flags, for (size_t i = 0; i < reserve_offs; i++) pglob->gl_pathv[i] = 0; for (size_t i = 0; i < pglob->gl_pathc; i++) { - pglob->gl_pathv[reserve_offs + prev_len + i] = "glob result"; + pglob->gl_pathv[reserve_offs + prev_len + i] = (char*)"glob result"; } pglob->gl_pathv[prev_len + reserve_offs + pglob->gl_pathc] = 0; // terminator if (Frama_C_nondet(0, 1)) { // simulate "no error" diff --git a/share/libc/locale.c b/share/libc/locale.c index 0b3dc103fce5463b9c65b9522fdb8eb7b2d0d6c4..eb60516c520e490a92aeeaeb5228f8ce70a27632 100644 --- a/share/libc/locale.c +++ b/share/libc/locale.c @@ -23,15 +23,19 @@ #include "locale.h" #include "limits.h" __PUSH_FC_STDLIB -struct lconv __C_locale = {".","","","","","","","","","",CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX}; +struct lconv __C_locale = {(char*)".",(char*)"",(char*)"",(char*)"",(char*)"", + (char*)"",(char*)"",(char*)"",(char*)"",(char*)"", + CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX, + CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX, + CHAR_MAX,CHAR_MAX,CHAR_MAX,CHAR_MAX}; struct lconv *__frama_c_locale=&__C_locale; -char*__frama_c_locale_names[512]={"C"}; +const char *__frama_c_locale_names[512] = {"C"}; char *setlocale(int category, const char *locale) { if (*locale == 'C') { __frama_c_locale = &__C_locale; - return __frama_c_locale_names[0]; + return (char*)__frama_c_locale_names[0]; }; return NULL; } diff --git a/share/libc/math.h b/share/libc/math.h index ec8b3111f434af48b20d7f3f6b75217b3333d9ed..25c122cd2ed7a047e97c86c3be4566de0ba72acb 100644 --- a/share/libc/math.h +++ b/share/libc/math.h @@ -1532,13 +1532,13 @@ extern int __finite(double d); ensures result_is_infinity: \is_plus_infinity(\result); assigns \result \from \nothing; @*/ -extern const float __fc_infinity(int x); +extern float __fc_infinity(int x); /*@ ensures result_is_nan: \is_NaN(\result); assigns \result \from \nothing; @*/ -extern const float __fc_nan(int x); +extern float __fc_nan(int x); #define INFINITY __fc_infinity(0) diff --git a/share/libc/netdb.c b/share/libc/netdb.c index 887b73f5bc84aa43b1f4afdb5be6f54ec884fa53..c208d255aa940004a5719f9dd2b568dd1dbf0811 100644 --- a/share/libc/netdb.c +++ b/share/libc/netdb.c @@ -69,7 +69,9 @@ int getaddrinfo( ai -> ai_protocol = Frama_C_interval(0,IPPROTO_MAX); ai -> ai_addrlen = sizeof(*sa) ; ai -> ai_addr = sa ; - ai -> ai_canonname = "dummy" ; + ai -> ai_canonname = malloc(6); + if (!ai -> ai_canonname) return EAI_MEMORY; + strcpy(ai -> ai_canonname, "dummy"); ai -> ai_next = NULL; *res = ai; return 0; @@ -91,7 +93,7 @@ struct __fc_gethostbyname { struct __fc_gethostbyname __fc_ghbn; -int res_search(const char *dname, int class, int type, +static int res_search(const char *dname, int rec_class, int type, char *answer, int anslen) { for (int i = 0; i < anslen-1; i++) { answer[i] = Frama_C_char_interval(CHAR_MIN, CHAR_MAX); @@ -132,7 +134,7 @@ struct hostent *gethostbyname(const char *name) { return &__fc_ghbn.host; } - if (*cp < '0' && *cp > '9' && *cp != '.') break; + if (*cp < '0' || *cp > '9' || *cp != '.') break; } } diff --git a/share/libc/netdb.h b/share/libc/netdb.h index 68f12a1ccf8e929e753b86f9223ed49031911545..d3efadce2b5aacf50d343166accd17fd451b2eee 100644 --- a/share/libc/netdb.h +++ b/share/libc/netdb.h @@ -121,7 +121,7 @@ extern void endservent(void); */ extern void freeaddrinfo(struct addrinfo * addrinfo); -char *__fc_gai_strerror = "<error message reported by gai_strerror>"; +const char *__fc_gai_strerror = "<error message reported by gai_strerror>"; /*@ assigns \result \from indirect:errcode, __fc_gai_strerror; diff --git a/share/libc/netinet/in.c b/share/libc/netinet/in.c new file mode 100644 index 0000000000000000000000000000000000000000..bc3bc1973cf3cd4675cd04a57d55247f7c03e22b --- /dev/null +++ b/share/libc/netinet/in.c @@ -0,0 +1,26 @@ +/**************************************************************************/ +/* */ +/* This file is part of Frama-C. */ +/* */ +/* Copyright (C) 2007-2021 */ +/* CEA (Commissariat à l'énergie atomique et aux énergies */ +/* alternatives) */ +/* */ +/* you can redistribute it and/or modify it under the terms of the GNU */ +/* Lesser General Public License as published by the Free Software */ +/* Foundation, version 2.1. */ +/* */ +/* It is distributed in the hope that it will be useful, */ +/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ +/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ +/* GNU Lesser General Public License for more details. */ +/* */ +/* See the GNU Lesser General Public License version 2.1 */ +/* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ +/**************************************************************************/ + +#include "in.h" + +const struct in6_addr in6addr_any=IN6ADDR_ANY_INIT; +const struct in6_addr in6addr_loopback=IN6ADDR_LOOPBACK_INIT; diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c index 9874c18211f312864165db98c7e9ac3adef3e402..e473fe89afb026b9a81774ef8121ac3ef6f43d3d 100644 --- a/share/libc/stdlib.c +++ b/share/libc/stdlib.c @@ -111,7 +111,7 @@ char *getenv(const char *name) int putenv(char *string) { - char *separator = strchr(string, '='); + char *separator __attribute__((unused)) = strchr(string, '='); //@ assert string_contains_separator: separator != \null; //@ assert name_is_not_empty: separator != string; diff --git a/share/libc/string.c b/share/libc/string.c index 998ca167775c63aeb536528f925d71204e8637e2..fd18f6236c04c354c87367d755ed3eb38273a6cb 100644 --- a/share/libc/string.c +++ b/share/libc/string.c @@ -272,11 +272,11 @@ char *strstr(const char *haystack, const char *needle) } char __fc_strerror[64]; -static int __fc_strerror_init; char *strerror(int errnum) { #ifdef __FRAMAC__ + static int __fc_strerror_init; if (!__fc_strerror_init) { Frama_C_make_unknown(__fc_strerror, 63); __fc_strerror[63] = 0; @@ -318,11 +318,11 @@ char *strndup(const char *s, size_t n) } char __fc_strsignal[64]; -static int __fc_strsignal_init; char *strsignal(int signum) { #ifdef __FRAMAC__ + static int __fc_strsignal_init; if (!__fc_strsignal_init) { Frama_C_make_unknown(__fc_strsignal, 63); __fc_strsignal[63] = 0; diff --git a/share/libc/string.h b/share/libc/string.h index 2fd6f72d2493a1b407f85a707f348feea8dfdc64..fa5202ebf4aa0bc12b3cc3e015cbc771fdc5ee45 100644 --- a/share/libc/string.h +++ b/share/libc/string.h @@ -87,6 +87,9 @@ extern int memcmp (const void *s1, const void *s2, size_t n); @*/ extern void *memchr(const void *s, int c, size_t n); +// Non-POSIX; GNU extension +extern void *memrchr(const void *s, int c, size_t n); + // Copy memory /*@ requires valid_dest: valid_or_empty(dest, n); diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h index 558129b5165e992f1a3c7eb6ced85231ac759594..f440e7fba8c91ba66bd5b4874b992a93aa9c5735 100644 --- a/share/libc/sys/socket.h +++ b/share/libc/sys/socket.h @@ -291,7 +291,7 @@ struct __fc_sockfds_type { int x; }; //@ ghost struct __fc_sockfds_type __fc_sockfds[__FC_MAX_OPEN_SOCKETS]; /* Represents the creation of new file descriptors for sockets. */ -//@ ghost extern int __fc_socket_counter __attribute__((__FRAMA_C_MODEL__)); +//@ ghost extern int __fc_socket_counter; // __fc_sockfds represents the state of open socket descriptors. //@ ghost volatile int __fc_open_sock_fds; diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle index 9fa7a4c3837305fe11f1259849cd635115a40859..e4a25f71358d728b76754a5a5f6e7a839b9fd553 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle @@ -2,28 +2,28 @@ [e-acsl] Warning: annotating undefined function `strncpy': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:375: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:375: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:363: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:366: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning: Some assumes clauses couldn't be translated. Ignoring complete and disjoint behaviors annotations. -[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:373: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:376: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:376: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c index 2c69667fd676b0b51a8177b25cb3e189a82069e1..5c19045e5d9ddf2c5a963db17e9e6fd3875736ef 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c @@ -108,7 +108,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src, (void *)(& dest)); __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","strncpy", "room_nstring: \\valid(dest + (0 .. n - 1))", - "FRAMAC_SHARE/libc/string.h",364); + "FRAMAC_SHARE/libc/string.h",367); __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add)); __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4; if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL; @@ -120,7 +120,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src, /*@ assert E_ACSL: separated_guard: \valid_read(dest + (0 .. n - 1)); */ __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","strncpy", "separated_guard: \\valid_read(dest + (0 .. n - 1))", - "FRAMAC_SHARE/libc/string.h",366); + "FRAMAC_SHARE/libc/string.h",369); __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add)); __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5; if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL; @@ -132,7 +132,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src, /*@ assert E_ACSL: separated_guard: \valid_read(src + (0 .. n - 1)); */ __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","strncpy", "separated_guard: \\valid_read(src + (0 .. n - 1))", - "FRAMAC_SHARE/libc/string.h",366); + "FRAMAC_SHARE/libc/string.h",369); __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add)); __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__6; if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL; @@ -147,7 +147,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src, __gen_e_acsl_if_5); __e_acsl_assert(__gen_e_acsl_separated,1,"Precondition","strncpy", "separation: \\separated(dest + (0 .. n - 1), src + (0 .. n - 1))", - "FRAMAC_SHARE/libc/string.h",366); + "FRAMAC_SHARE/libc/string.h",369); __gmpz_clear(__gen_e_acsl_n); __gmpz_clear(__gen_e_acsl_); __gmpz_clear(__gen_e_acsl_sub); @@ -177,7 +177,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src, int __gen_e_acsl_initialized; __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strncpy", "result_ptr: \\result == \\old(dest)", - "FRAMAC_SHARE/libc/string.h",369); + "FRAMAC_SHARE/libc/string.h",372); __gmpz_init_set_si(__gen_e_acsl__8,1L); __gmpz_init(__gen_e_acsl_sub_3); __gmpz_sub(__gen_e_acsl_sub_3, @@ -201,7 +201,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src, __gen_e_acsl_if_6); __e_acsl_assert(__gen_e_acsl_initialized,1,"Postcondition","strncpy", "initialization: \\initialized(\\old(dest) + (0 .. \\old(n) - 1))", - "FRAMAC_SHARE/libc/string.h",370); + "FRAMAC_SHARE/libc/string.h",373); __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& src)); __e_acsl_delete_block((void *)(& dest)); diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c index 4d91b86c3f9d8c70ccd6e61e4bdc67f2451b936c..0a22e2db5a4182c7561b607ba8f01f5a337264be 100644 --- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c +++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c @@ -709,7 +709,7 @@ char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src) __retres = strcpy(dest,src); __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strcpy", "result_ptr: \\result == \\old(dest)", - "FRAMAC_SHARE/libc/string.h",358); + "FRAMAC_SHARE/libc/string.h",361); __e_acsl_delete_block((void *)(& src)); __e_acsl_delete_block((void *)(& dest)); return __retres; @@ -777,17 +777,17 @@ char *__gen_e_acsl_strchr(char const *s, int c) else __gen_e_acsl_and = 0; __e_acsl_assert(__gen_e_acsl_and,1,"RTE","strchr", "mem_access: \\valid_read(__retres)", - "FRAMAC_SHARE/libc/string.h",161); + "FRAMAC_SHARE/libc/string.h",164); __gen_e_acsl_base_addr = __e_acsl_base_addr((void *)__retres); __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at_2); __e_acsl_assert(__gen_e_acsl_base_addr == __gen_e_acsl_base_addr_2,1, "Postcondition","strchr", "found: result_same_base: \\base_addr(\\result) == \\base_addr(\\old(s))", - "FRAMAC_SHARE/libc/string.h",162); + "FRAMAC_SHARE/libc/string.h",165); __e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at),1, "Postcondition","strchr", "found: result_char: *\\result == (char)\\old(c)", - "FRAMAC_SHARE/libc/string.h",161); + "FRAMAC_SHARE/libc/string.h",164); } __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); @@ -795,7 +795,7 @@ char *__gen_e_acsl_strchr(char const *s, int c) "Postcondition","strchr", "not_found: result_null: \\result == \\null", "FRAMAC_SHARE/libc/string.h", - 168); + 171); __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)2); if (__gen_e_acsl_assumes_value) { @@ -810,7 +810,7 @@ char *__gen_e_acsl_strchr(char const *s, int c) } __e_acsl_assert(__gen_e_acsl_or,1,"Postcondition","strchr", "default: result_null_or_same_base:\n \\result == \\null || \\base_addr(\\result) == \\base_addr(\\old(s))", - "FRAMAC_SHARE/libc/string.h",171); + "FRAMAC_SHARE/libc/string.h",174); } __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& s)); diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle index 2577a120bee9356da794270e1e72eb885b43d95c..cb01c6b6e06ba3df317b56a4b676a2904122fb39 100644 --- a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle @@ -32,60 +32,60 @@ [e-acsl] FRAMAC_SHARE/libc/unistd.h:854: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:351: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:354: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:352: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:355: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:354: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:357: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:351: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:354: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:357: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:360: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:163: Warning: E-ACSL construct `user-defined logic type' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:167: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:170: Warning: E-ACSL construct `user-defined logic type' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:157: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:157: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning: Some assumes clauses couldn't be translated. Ignoring complete and disjoint behaviors annotations. -[e-acsl] FRAMAC_SHARE/libc/string.h:157: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:163: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:166: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:164: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:167: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:165: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:168: Warning: E-ACSL construct `non integer variable p in quantification found: result_first_occur: ∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c)' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:128: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:128: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:130: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle index 0bd6f13a76d67792511473f7cff8c09b1e5a476d..598567fd7477989f02df51579791eb573d6b5366 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle @@ -2,13 +2,13 @@ [e-acsl] Warning: annotating undefined function `strlen': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:128: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:128: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:130: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. @@ -33,9 +33,9 @@ [eva:alarm] tests/memory/mainargs.c:16: Warning: assertion got status unknown. [eva:alarm] tests/memory/mainargs.c:18: Warning: function __gen_e_acsl_strlen: precondition 'valid_string_s' got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/string.h:125: Warning: +[eva:alarm] FRAMAC_SHARE/libc/string.h:128: Warning: function strlen: precondition 'valid_string_s' got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/string.h:127: Warning: +[eva:alarm] FRAMAC_SHARE/libc/string.h:130: Warning: function __gen_e_acsl_strlen: postcondition 'acsl_c_equiv' got status unknown. [eva:alarm] tests/memory/mainargs.c:19: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c index 82816259efd335076a8819e38bee58b98cc7c608..192cc55320e0e2b05f43cedb5aec085a80331d39 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c +++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c @@ -408,7 +408,7 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n) __retres = memset(s,c,n); __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","memset", "result_ptr: \\result == \\old(s)", - "FRAMAC_SHARE/libc/string.h",119); + "FRAMAC_SHARE/libc/string.h",122); __e_acsl_delete_block((void *)(& s)); return __retres; } @@ -487,7 +487,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src, */ __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","memcpy", "separated_guard: \\valid_read((char *)dest + (0 .. n - 1))", - "FRAMAC_SHARE/libc/string.h",95); + "FRAMAC_SHARE/libc/string.h",98); __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add)); __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4; if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL; @@ -502,7 +502,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src, */ __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","memcpy", "separated_guard: \\valid_read((char *)src + (0 .. n - 1))", - "FRAMAC_SHARE/libc/string.h",95); + "FRAMAC_SHARE/libc/string.h",98); __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add)); __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5; if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL; @@ -518,7 +518,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src, __gen_e_acsl_if_4); __e_acsl_assert(__gen_e_acsl_separated,1,"Precondition","memcpy", "separation:\n \\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))", - "FRAMAC_SHARE/libc/string.h",95); + "FRAMAC_SHARE/libc/string.h",98); __e_acsl_temporal_reset_parameters(); __e_acsl_temporal_reset_return(); __e_acsl_temporal_save_nreferent_parameter((void *)(& dest),0U); @@ -535,7 +535,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src, __retres = memcpy(dest,src,n); __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","memcpy", "result_ptr: \\result == \\old(dest)", - "FRAMAC_SHARE/libc/string.h",99); + "FRAMAC_SHARE/libc/string.h",102); __e_acsl_delete_block((void *)(& src)); __e_acsl_delete_block((void *)(& dest)); return __retres; diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle index 8b4d4539a0c15bbe3739c3af98669e4f10e81024..864651047494fe8fa0b9901bbccf50fa901e57de 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle @@ -5,32 +5,32 @@ [e-acsl] Warning: annotating undefined function `memset': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/string.h:115: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:118: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:115: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:118: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:118: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:121: Warning: E-ACSL construct `user-defined logic type' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:93: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:96: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:98: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] FRAMAC_SHARE/libc/string.h:95: Warning: - function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] FRAMAC_SHARE/libc/string.h:98: Warning: + function __e_acsl_assert, behavior blocking: precondition got status unknown. +[eva:alarm] FRAMAC_SHARE/libc/string.h:101: Warning: function __gen_e_acsl_memcpy: postcondition 'copied_contents' got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/string.h:118: Warning: +[eva:alarm] FRAMAC_SHARE/libc/string.h:121: Warning: function __gen_e_acsl_memset: postcondition 'acsl_c_equiv' got status unknown. diff --git a/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle index a303c721399c9ef094fce2029414b3205d549ab4..6d2973ada4468536c302d6f569eceab93bf4a838 100644 --- a/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle +++ b/src/plugins/markdown-report/tests/md/oracle/cwe126.res.oracle @@ -6,7 +6,7 @@ [eva] tests/md/cwe126.c:76: allocating variable __malloc_goodG2B_l76 [eva] using specification for function exit -[eva] FRAMAC_SHARE/libc/string.h:118: +[eva] FRAMAC_SHARE/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] tests/md/cwe126.c:62: starting to merge loop iterations [eva] tests/md/cwe126.c:40: 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 d898b2528498b8b97d7170ffa8bad67cc0590cad..92989f9ff24ed46cd969d699cbe957a4e091c99f 100644 --- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif +++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif @@ -9551,9 +9551,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 92, + "startLine": 95, "startColumn": 25, - "endLine": 92, + "endLine": 95, "endColumn": 48, "byteLength": 23 } @@ -9574,9 +9574,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 93, + "startLine": 96, "startColumn": 24, - "endLine": 93, + "endLine": 96, "endColumn": 51, "byteLength": 27 } @@ -9597,9 +9597,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 95, + "startLine": 98, "startColumn": 4, - "endLine": 95, + "endLine": 98, "endColumn": 62, "byteLength": 58 } @@ -9620,9 +9620,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 98, + "startLine": 101, "startColumn": 29, - "endLine": 98, + "endLine": 101, "endColumn": 76, "byteLength": 47 } @@ -9643,9 +9643,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 99, + "startLine": 102, "startColumn": 24, - "endLine": 99, + "endLine": 102, "endColumn": 39, "byteLength": 15 } @@ -9666,9 +9666,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 96, + "startLine": 99, "startColumn": 12, - "endLine": 96, + "endLine": 99, "endColumn": 35, "byteLength": 23 } @@ -9692,9 +9692,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 96, + "startLine": 99, "startColumn": 12, - "endLine": 96, + "endLine": 99, "endColumn": 35, "byteLength": 23 } @@ -9717,9 +9717,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 97, + "startLine": 100, "startColumn": 12, - "endLine": 97, + "endLine": 100, "endColumn": 19, "byteLength": 7 } @@ -9901,9 +9901,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 104, + "startLine": 107, "startColumn": 25, - "endLine": 104, + "endLine": 107, "endColumn": 48, "byteLength": 23 } @@ -9924,9 +9924,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 105, + "startLine": 108, "startColumn": 24, - "endLine": 105, + "endLine": 108, "endColumn": 51, "byteLength": 27 } @@ -9947,9 +9947,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 108, + "startLine": 111, "startColumn": 29, - "endLine": 108, + "endLine": 111, "endColumn": 76, "byteLength": 47 } @@ -9970,9 +9970,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 109, + "startLine": 112, "startColumn": 24, - "endLine": 109, + "endLine": 112, "endColumn": 39, "byteLength": 15 } @@ -9993,9 +9993,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 106, + "startLine": 109, "startColumn": 12, - "endLine": 106, + "endLine": 109, "endColumn": 35, "byteLength": 23 } @@ -10019,9 +10019,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 106, + "startLine": 109, "startColumn": 12, - "endLine": 106, + "endLine": 109, "endColumn": 35, "byteLength": 23 } @@ -10044,9 +10044,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 107, + "startLine": 110, "startColumn": 12, - "endLine": 107, + "endLine": 110, "endColumn": 19, "byteLength": 7 } @@ -10786,9 +10786,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 115, + "startLine": 118, "startColumn": 22, - "endLine": 115, + "endLine": 118, "endColumn": 42, "byteLength": 20 } @@ -10809,9 +10809,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 118, + "startLine": 121, "startColumn": 26, - "endLine": 118, + "endLine": 121, "endColumn": 46, "byteLength": 20 } @@ -10832,9 +10832,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 119, + "startLine": 122, "startColumn": 24, - "endLine": 119, + "endLine": 122, "endColumn": 36, "byteLength": 12 } @@ -10855,9 +10855,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 119, "startColumn": 12, - "endLine": 116, + "endLine": 119, "endColumn": 32, "byteLength": 20 } @@ -10881,9 +10881,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 119, "startColumn": 12, - "endLine": 116, + "endLine": 119, "endColumn": 32, "byteLength": 20 } @@ -10906,9 +10906,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 117, + "startLine": 120, "startColumn": 12, - "endLine": 117, + "endLine": 120, "endColumn": 19, "byteLength": 7 } @@ -13650,9 +13650,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 405, + "startLine": 408, "startColumn": 12, - "endLine": 405, + "endLine": 408, "endColumn": 13, "byteLength": 1 } @@ -13673,9 +13673,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 396, + "startLine": 399, "startColumn": 31, - "endLine": 396, + "endLine": 399, "endColumn": 53, "byteLength": 22 } @@ -13696,9 +13696,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 397, + "startLine": 400, "startColumn": 26, - "endLine": 397, + "endLine": 400, "endColumn": 55, "byteLength": 29 } @@ -13719,9 +13719,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 399, + "startLine": 402, "startColumn": 4, - "endLine": 399, + "endLine": 402, "endColumn": 59, "byteLength": 55 } @@ -13742,9 +13742,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 402, + "startLine": 405, "startColumn": 28, - "endLine": 402, + "endLine": 405, "endColumn": 49, "byteLength": 21 } @@ -13765,9 +13765,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 406, "startColumn": 27, - "endLine": 403, + "endLine": 406, "endColumn": 57, "byteLength": 30 } @@ -13788,9 +13788,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 400, + "startLine": 403, "startColumn": 12, - "endLine": 400, + "endLine": 403, "endColumn": 32, "byteLength": 20 } @@ -13814,9 +13814,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 400, + "startLine": 403, "startColumn": 12, - "endLine": 400, + "endLine": 403, "endColumn": 32, "byteLength": 20 } @@ -13839,9 +13839,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 401, + "startLine": 404, "startColumn": 12, - "endLine": 401, + "endLine": 404, "endColumn": 19, "byteLength": 7 } @@ -13979,9 +13979,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 239, + "startLine": 242, "startColumn": 12, - "endLine": 239, + "endLine": 242, "endColumn": 13, "byteLength": 1 } @@ -14002,9 +14002,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 231, + "startLine": 234, "startColumn": 36, - "endLine": 231, + "endLine": 234, "endColumn": 63, "byteLength": 27 } @@ -14025,9 +14025,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 232, + "startLine": 235, "startColumn": 34, - "endLine": 232, + "endLine": 235, "endColumn": 59, "byteLength": 25 } @@ -14048,9 +14048,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 236, + "startLine": 239, "startColumn": 4, - "endLine": 237, + "endLine": 240, "endColumn": 65, "byteLength": 82 } @@ -14071,9 +14071,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 239, + "startLine": 242, "startColumn": 12, - "endLine": 239, + "endLine": 242, "endColumn": 13, "byteLength": 1 } @@ -14096,9 +14096,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 233, + "startLine": 236, "startColumn": 12, - "endLine": 233, + "endLine": 236, "endColumn": 19, "byteLength": 7 } @@ -14142,9 +14142,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 408, + "startLine": 411, "startColumn": 31, - "endLine": 408, + "endLine": 411, "endColumn": 53, "byteLength": 22 } @@ -14165,9 +14165,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 409, + "startLine": 412, "startColumn": 32, - "endLine": 409, + "endLine": 412, "endColumn": 50, "byteLength": 18 } @@ -14188,9 +14188,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 410, + "startLine": 413, "startColumn": 26, - "endLine": 410, + "endLine": 413, "endColumn": 70, "byteLength": 44 } @@ -14211,9 +14211,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 413, + "startLine": 416, "startColumn": 28, - "endLine": 413, + "endLine": 416, "endColumn": 76, "byteLength": 48 } @@ -14234,9 +14234,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 416, + "startLine": 419, "startColumn": 4, - "endLine": 416, + "endLine": 419, "endColumn": 60, "byteLength": 56 } @@ -14257,9 +14257,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 417, + "startLine": 420, "startColumn": 34, - "endLine": 417, + "endLine": 420, "endColumn": 77, "byteLength": 43 } @@ -14280,9 +14280,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 418, + "startLine": 421, "startColumn": 24, - "endLine": 418, + "endLine": 421, "endColumn": 39, "byteLength": 15 } @@ -14303,9 +14303,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 411, + "startLine": 414, "startColumn": 12, - "endLine": 411, + "endLine": 414, "endColumn": 58, "byteLength": 46 } @@ -14329,9 +14329,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 411, + "startLine": 414, "startColumn": 12, - "endLine": 411, + "endLine": 414, "endColumn": 58, "byteLength": 46 } @@ -14354,9 +14354,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 414, + "startLine": 417, "startColumn": 12, - "endLine": 414, + "endLine": 417, "endColumn": 19, "byteLength": 7 } @@ -14517,9 +14517,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 157, + "startLine": 160, "startColumn": 29, - "endLine": 157, + "endLine": 160, "endColumn": 49, "byteLength": 20 } @@ -14540,9 +14540,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 160, + "startLine": 163, "startColumn": 24, - "endLine": 160, + "endLine": 163, "endColumn": 35, "byteLength": 11 } @@ -14563,9 +14563,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 167, + "startLine": 170, "startColumn": 28, - "endLine": 167, + "endLine": 170, "endColumn": 40, "byteLength": 12 } @@ -14586,9 +14586,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 161, + "startLine": 164, "startColumn": 25, - "endLine": 161, + "endLine": 164, "endColumn": 44, "byteLength": 19 } @@ -14609,9 +14609,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 162, + "startLine": 165, "startColumn": 30, - "endLine": 162, + "endLine": 165, "endColumn": 66, "byteLength": 36 } @@ -14632,9 +14632,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 163, + "startLine": 166, "startColumn": 30, - "endLine": 163, + "endLine": 166, "endColumn": 59, "byteLength": 29 } @@ -14655,9 +14655,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 164, + "startLine": 167, "startColumn": 33, - "endLine": 164, + "endLine": 167, "endColumn": 59, "byteLength": 26 } @@ -14678,9 +14678,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 165, + "startLine": 168, "startColumn": 32, - "endLine": 165, + "endLine": 168, "endColumn": 79, "byteLength": 47 } @@ -14701,9 +14701,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 168, + "startLine": 171, "startColumn": 25, - "endLine": 168, + "endLine": 171, "endColumn": 41, "byteLength": 16 } @@ -14724,9 +14724,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 171, + "startLine": 174, "startColumn": 4, - "endLine": 171, + "endLine": 174, "endColumn": 60, "byteLength": 56 } @@ -14772,9 +14772,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 158, + "startLine": 161, "startColumn": 12, - "endLine": 158, + "endLine": 161, "endColumn": 19, "byteLength": 7 } @@ -14795,9 +14795,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 179, + "startLine": 182, "startColumn": 12, - "endLine": 179, + "endLine": 182, "endColumn": 13, "byteLength": 1 } @@ -14818,9 +14818,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 175, + "startLine": 178, "startColumn": 29, - "endLine": 175, + "endLine": 178, "endColumn": 49, "byteLength": 20 } @@ -14841,9 +14841,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 177, + "startLine": 180, "startColumn": 30, - "endLine": 177, + "endLine": 180, "endColumn": 64, "byteLength": 34 } @@ -14864,9 +14864,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 179, + "startLine": 182, "startColumn": 12, - "endLine": 179, + "endLine": 182, "endColumn": 13, "byteLength": 1 } @@ -14889,9 +14889,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 176, + "startLine": 179, "startColumn": 12, - "endLine": 176, + "endLine": 179, "endColumn": 19, "byteLength": 7 } @@ -14935,9 +14935,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 137, + "startLine": 140, "startColumn": 30, - "endLine": 137, + "endLine": 140, "endColumn": 51, "byteLength": 21 } @@ -14958,9 +14958,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 138, + "startLine": 141, "startColumn": 30, - "endLine": 138, + "endLine": 141, "endColumn": 51, "byteLength": 21 } @@ -14981,9 +14981,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 140, + "startLine": 143, "startColumn": 26, - "endLine": 140, + "endLine": 143, "endColumn": 50, "byteLength": 24 } @@ -15029,9 +15029,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 139, + "startLine": 142, "startColumn": 12, - "endLine": 139, + "endLine": 142, "endColumn": 19, "byteLength": 7 } @@ -15052,9 +15052,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 155, + "startLine": 158, "startColumn": 11, - "endLine": 155, + "endLine": 158, "endColumn": 18, "byteLength": 7 } @@ -15075,9 +15075,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 151, + "startLine": 154, "startColumn": 30, - "endLine": 151, + "endLine": 154, "endColumn": 51, "byteLength": 21 } @@ -15098,9 +15098,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 152, + "startLine": 155, "startColumn": 30, - "endLine": 152, + "endLine": 155, "endColumn": 51, "byteLength": 21 } @@ -15121,9 +15121,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 155, + "startLine": 158, "startColumn": 11, - "endLine": 155, + "endLine": 158, "endColumn": 18, "byteLength": 7 } @@ -15146,9 +15146,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 153, + "startLine": 156, "startColumn": 12, - "endLine": 153, + "endLine": 156, "endColumn": 19, "byteLength": 7 } @@ -15192,9 +15192,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 351, + "startLine": 354, "startColumn": 31, - "endLine": 351, + "endLine": 354, "endColumn": 53, "byteLength": 22 } @@ -15215,9 +15215,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 352, + "startLine": 355, "startColumn": 26, - "endLine": 352, + "endLine": 355, "endColumn": 55, "byteLength": 29 } @@ -15238,9 +15238,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 354, + "startLine": 357, "startColumn": 4, - "endLine": 354, + "endLine": 357, "endColumn": 59, "byteLength": 55 } @@ -15261,9 +15261,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 357, + "startLine": 360, "startColumn": 28, - "endLine": 357, + "endLine": 360, "endColumn": 49, "byteLength": 21 } @@ -15284,9 +15284,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 358, + "startLine": 361, "startColumn": 24, - "endLine": 358, + "endLine": 361, "endColumn": 39, "byteLength": 15 } @@ -15307,9 +15307,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 355, + "startLine": 358, "startColumn": 12, - "endLine": 355, + "endLine": 358, "endColumn": 32, "byteLength": 20 } @@ -15333,9 +15333,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 355, + "startLine": 358, "startColumn": 12, - "endLine": 355, + "endLine": 358, "endColumn": 32, "byteLength": 20 } @@ -15358,9 +15358,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 356, + "startLine": 359, "startColumn": 12, - "endLine": 356, + "endLine": 359, "endColumn": 19, "byteLength": 7 } @@ -15381,9 +15381,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 202, + "startLine": 205, "startColumn": 14, - "endLine": 202, + "endLine": 205, "endColumn": 21, "byteLength": 7 } @@ -15404,9 +15404,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 197, + "startLine": 200, "startColumn": 29, - "endLine": 197, + "endLine": 200, "endColumn": 49, "byteLength": 20 } @@ -15427,9 +15427,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 198, + "startLine": 201, "startColumn": 34, - "endLine": 198, + "endLine": 201, "endColumn": 59, "byteLength": 25 } @@ -15450,9 +15450,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 200, + "startLine": 203, "startColumn": 28, - "endLine": 200, + "endLine": 203, "endColumn": 53, "byteLength": 25 } @@ -15473,9 +15473,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 202, + "startLine": 205, "startColumn": 14, - "endLine": 202, + "endLine": 205, "endColumn": 21, "byteLength": 7 } @@ -15498,9 +15498,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 199, + "startLine": 202, "startColumn": 12, - "endLine": 199, + "endLine": 202, "endColumn": 19, "byteLength": 7 } @@ -15590,9 +15590,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 468, + "startLine": 471, "startColumn": 29, - "endLine": 468, + "endLine": 471, "endColumn": 49, "byteLength": 20 } @@ -15613,9 +15613,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 472, + "startLine": 475, "startColumn": 26, - "endLine": 472, + "endLine": 475, "endColumn": 49, "byteLength": 23 } @@ -15636,9 +15636,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 479, + "startLine": 482, "startColumn": 29, - "endLine": 479, + "endLine": 482, "endColumn": 53, "byteLength": 24 } @@ -15659,9 +15659,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 475, + "startLine": 478, "startColumn": 24, - "endLine": 475, + "endLine": 478, "endColumn": 49, "byteLength": 25 } @@ -15682,9 +15682,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 477, + "startLine": 480, "startColumn": 4, - "endLine": 477, + "endLine": 480, "endColumn": 51, "byteLength": 47 } @@ -15705,9 +15705,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 482, + "startLine": 485, "startColumn": 25, - "endLine": 482, + "endLine": 485, "endColumn": 41, "byteLength": 16 } @@ -15728,9 +15728,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 473, + "startLine": 476, "startColumn": 12, - "endLine": 473, + "endLine": 476, "endColumn": 28, "byteLength": 16 } @@ -15800,9 +15800,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 473, + "startLine": 476, "startColumn": 12, - "endLine": 473, + "endLine": 476, "endColumn": 28, "byteLength": 16 } @@ -15825,9 +15825,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 474, + "startLine": 477, "startColumn": 12, - "endLine": 474, + "endLine": 477, "endColumn": 19, "byteLength": 7 } @@ -15850,9 +15850,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 470, + "startLine": 473, "startColumn": 12, - "endLine": 470, + "endLine": 473, "endColumn": 19, "byteLength": 7 } @@ -15875,9 +15875,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 480, + "startLine": 483, "startColumn": 12, - "endLine": 480, + "endLine": 483, "endColumn": 19, "byteLength": 7 } @@ -15898,9 +15898,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 469, + "startLine": 472, "startColumn": 14, - "endLine": 469, + "endLine": 472, "endColumn": 21, "byteLength": 7 } @@ -16084,11 +16084,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 277, + "startLine": 276, "startColumn": 5, "endLine": 287, "endColumn": 1, - "byteLength": 184 + "byteLength": 217 } } } @@ -16107,9 +16107,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 343, + "startLine": 346, "startColumn": 33, - "endLine": 343, + "endLine": 346, "endColumn": 59, "byteLength": 26 } @@ -16130,9 +16130,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 344, + "startLine": 347, "startColumn": 35, - "endLine": 344, + "endLine": 347, "endColumn": 51, "byteLength": 16 } @@ -16153,9 +16153,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 345, + "startLine": 348, "startColumn": 33, - "endLine": 345, + "endLine": 348, "endColumn": 59, "byteLength": 26 } @@ -16176,11 +16176,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 277, + "startLine": 276, "startColumn": 5, "endLine": 287, "endColumn": 1, - "byteLength": 184 + "byteLength": 217 } } } @@ -16201,9 +16201,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 342, + "startLine": 345, "startColumn": 12, - "endLine": 342, + "endLine": 345, "endColumn": 19, "byteLength": 7 } @@ -16270,9 +16270,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 455, + "startLine": 458, "startColumn": 14, - "endLine": 455, + "endLine": 458, "endColumn": 21, "byteLength": 7 } @@ -16293,9 +16293,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 448, + "startLine": 451, "startColumn": 31, - "endLine": 448, + "endLine": 451, "endColumn": 53, "byteLength": 22 } @@ -16316,9 +16316,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 449, + "startLine": 452, "startColumn": 32, - "endLine": 449, + "endLine": 452, "endColumn": 50, "byteLength": 18 } @@ -16339,9 +16339,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 450, + "startLine": 453, "startColumn": 27, - "endLine": 450, + "endLine": 453, "endColumn": 48, "byteLength": 21 } @@ -16362,9 +16362,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 453, + "startLine": 456, "startColumn": 28, - "endLine": 453, + "endLine": 456, "endColumn": 65, "byteLength": 37 } @@ -16385,9 +16385,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 451, + "startLine": 454, "startColumn": 12, - "endLine": 451, + "endLine": 454, "endColumn": 33, "byteLength": 21 } @@ -16411,9 +16411,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 451, + "startLine": 454, "startColumn": 12, - "endLine": 451, + "endLine": 454, "endColumn": 33, "byteLength": 21 } @@ -16436,9 +16436,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 455, "startColumn": 12, - "endLine": 452, + "endLine": 455, "endColumn": 19, "byteLength": 7 } @@ -16459,9 +16459,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 393, + "startLine": 396, "startColumn": 7, - "endLine": 393, + "endLine": 396, "endColumn": 14, "byteLength": 7 } @@ -16482,9 +16482,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 384, + "startLine": 387, "startColumn": 31, - "endLine": 384, + "endLine": 387, "endColumn": 53, "byteLength": 22 } @@ -16505,9 +16505,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 388, "startColumn": 27, - "endLine": 385, + "endLine": 388, "endColumn": 48, "byteLength": 21 } @@ -16528,9 +16528,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 387, + "startLine": 390, "startColumn": 4, - "endLine": 387, + "endLine": 390, "endColumn": 61, "byteLength": 57 } @@ -16551,9 +16551,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 390, + "startLine": 393, "startColumn": 28, - "endLine": 390, + "endLine": 393, "endColumn": 73, "byteLength": 45 } @@ -16574,9 +16574,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 391, + "startLine": 394, "startColumn": 28, - "endLine": 391, + "endLine": 394, "endColumn": 50, "byteLength": 22 } @@ -16597,9 +16597,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 388, + "startLine": 391, "startColumn": 12, - "endLine": 388, + "endLine": 391, "endColumn": 24, "byteLength": 12 } @@ -16623,9 +16623,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 388, + "startLine": 391, "startColumn": 12, - "endLine": 388, + "endLine": 391, "endColumn": 24, "byteLength": 12 } @@ -16648,9 +16648,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 389, + "startLine": 392, "startColumn": 12, - "endLine": 389, + "endLine": 392, "endColumn": 19, "byteLength": 7 } @@ -16694,9 +16694,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 125, + "startLine": 128, "startColumn": 29, - "endLine": 125, + "endLine": 128, "endColumn": 49, "byteLength": 20 } @@ -16717,9 +16717,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 127, + "startLine": 130, "startColumn": 26, - "endLine": 127, + "endLine": 130, "endColumn": 46, "byteLength": 20 } @@ -16765,9 +16765,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 126, + "startLine": 129, "startColumn": 12, - "endLine": 126, + "endLine": 129, "endColumn": 19, "byteLength": 7 } @@ -16974,9 +16974,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 423, + "startLine": 426, "startColumn": 32, - "endLine": 423, + "endLine": 426, "endColumn": 58, "byteLength": 26 } @@ -16997,9 +16997,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 424, + "startLine": 427, "startColumn": 32, - "endLine": 424, + "endLine": 427, "endColumn": 50, "byteLength": 18 } @@ -17020,9 +17020,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 430, + "startLine": 433, "startColumn": 26, - "endLine": 430, + "endLine": 433, "endColumn": 74, "byteLength": 48 } @@ -17043,9 +17043,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 438, + "startLine": 441, "startColumn": 26, - "endLine": 438, + "endLine": 441, "endColumn": 64, "byteLength": 38 } @@ -17066,9 +17066,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 429, + "startLine": 432, "startColumn": 35, - "endLine": 429, + "endLine": 432, "endColumn": 77, "byteLength": 42 } @@ -17089,9 +17089,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 437, + "startLine": 440, "startColumn": 4, - "endLine": 437, + "endLine": 440, "endColumn": 49, "byteLength": 45 } @@ -17112,9 +17112,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 427, + "startLine": 430, "startColumn": 24, - "endLine": 427, + "endLine": 430, "endColumn": 39, "byteLength": 15 } @@ -17135,9 +17135,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 434, + "startLine": 437, "startColumn": 28, - "endLine": 434, + "endLine": 437, "endColumn": 76, "byteLength": 48 } @@ -17158,9 +17158,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 442, + "startLine": 445, "startColumn": 36, - "endLine": 442, + "endLine": 445, "endColumn": 74, "byteLength": 38 } @@ -17181,9 +17181,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 431, + "startLine": 434, "startColumn": 12, - "endLine": 431, + "endLine": 434, "endColumn": 58, "byteLength": 46 } @@ -17204,9 +17204,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 425, + "startLine": 428, "startColumn": 12, - "endLine": 425, + "endLine": 428, "endColumn": 50, "byteLength": 38 } @@ -17227,9 +17227,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 439, + "startLine": 442, "startColumn": 12, - "endLine": 439, + "endLine": 442, "endColumn": 48, "byteLength": 36 } @@ -17253,9 +17253,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 431, + "startLine": 434, "startColumn": 12, - "endLine": 431, + "endLine": 434, "endColumn": 58, "byteLength": 46 } @@ -17278,9 +17278,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 433, + "startLine": 436, "startColumn": 12, - "endLine": 433, + "endLine": 436, "endColumn": 19, "byteLength": 7 } @@ -17304,9 +17304,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 425, + "startLine": 428, "startColumn": 12, - "endLine": 425, + "endLine": 428, "endColumn": 50, "byteLength": 38 } @@ -17329,9 +17329,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 426, + "startLine": 429, "startColumn": 12, - "endLine": 426, + "endLine": 429, "endColumn": 19, "byteLength": 7 } @@ -17355,9 +17355,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 439, + "startLine": 442, "startColumn": 12, - "endLine": 439, + "endLine": 442, "endColumn": 48, "byteLength": 36 } @@ -17380,9 +17380,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 441, + "startLine": 444, "startColumn": 12, - "endLine": 441, + "endLine": 444, "endColumn": 19, "byteLength": 7 } @@ -17474,9 +17474,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 144, + "startLine": 147, "startColumn": 30, - "endLine": 144, + "endLine": 147, "endColumn": 55, "byteLength": 25 } @@ -17497,9 +17497,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 145, + "startLine": 148, "startColumn": 30, - "endLine": 145, + "endLine": 148, "endColumn": 55, "byteLength": 25 } @@ -17520,9 +17520,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 147, + "startLine": 150, "startColumn": 26, - "endLine": 147, + "endLine": 150, "endColumn": 53, "byteLength": 27 } @@ -17568,9 +17568,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 146, + "startLine": 149, "startColumn": 12, - "endLine": 146, + "endLine": 149, "endColumn": 19, "byteLength": 7 } @@ -17660,9 +17660,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 363, + "startLine": 366, "startColumn": 32, - "endLine": 363, + "endLine": 366, "endColumn": 58, "byteLength": 26 } @@ -17683,9 +17683,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 364, + "startLine": 367, "startColumn": 27, - "endLine": 364, + "endLine": 367, "endColumn": 50, "byteLength": 23 } @@ -17706,9 +17706,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 366, + "startLine": 369, "startColumn": 4, - "endLine": 366, + "endLine": 369, "endColumn": 43, "byteLength": 39 } @@ -17729,9 +17729,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 372, + "startLine": 375, "startColumn": 22, - "endLine": 372, + "endLine": 375, "endColumn": 37, "byteLength": 15 } @@ -17752,9 +17752,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 375, + "startLine": 378, "startColumn": 26, - "endLine": 375, + "endLine": 378, "endColumn": 42, "byteLength": 16 } @@ -17775,9 +17775,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 369, + "startLine": 372, "startColumn": 24, - "endLine": 369, + "endLine": 372, "endColumn": 39, "byteLength": 15 } @@ -17798,9 +17798,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 370, + "startLine": 373, "startColumn": 28, - "endLine": 370, + "endLine": 373, "endColumn": 57, "byteLength": 29 } @@ -17821,9 +17821,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 373, + "startLine": 376, "startColumn": 30, - "endLine": 373, + "endLine": 376, "endColumn": 51, "byteLength": 21 } @@ -17844,9 +17844,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 376, + "startLine": 379, "startColumn": 26, - "endLine": 376, + "endLine": 379, "endColumn": 60, "byteLength": 34 } @@ -17867,9 +17867,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 367, + "startLine": 370, "startColumn": 12, - "endLine": 367, + "endLine": 370, "endColumn": 26, "byteLength": 14 } @@ -17893,9 +17893,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 367, + "startLine": 370, "startColumn": 12, - "endLine": 367, + "endLine": 370, "endColumn": 26, "byteLength": 14 } @@ -17918,9 +17918,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 368, + "startLine": 371, "startColumn": 12, - "endLine": 368, + "endLine": 371, "endColumn": 19, "byteLength": 7 } @@ -18012,9 +18012,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 486, + "startLine": 489, "startColumn": 29, - "endLine": 486, + "endLine": 489, "endColumn": 49, "byteLength": 20 } @@ -18035,9 +18035,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 491, + "startLine": 494, "startColumn": 26, - "endLine": 491, + "endLine": 494, "endColumn": 60, "byteLength": 34 } @@ -18058,9 +18058,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 501, + "startLine": 504, "startColumn": 29, - "endLine": 501, + "endLine": 504, "endColumn": 64, "byteLength": 35 } @@ -18081,9 +18081,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 495, + "startLine": 498, "startColumn": 24, - "endLine": 495, + "endLine": 498, "endColumn": 60, "byteLength": 36 } @@ -18106,9 +18106,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 497, + "startLine": 500, "startColumn": 4, - "endLine": 499, + "endLine": 502, "endColumn": 29, "byteLength": 124 } @@ -18129,9 +18129,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 504, + "startLine": 507, "startColumn": 25, - "endLine": 504, + "endLine": 507, "endColumn": 41, "byteLength": 16 } @@ -18152,9 +18152,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 492, + "startLine": 495, "startColumn": 12, - "endLine": 492, + "endLine": 495, "endColumn": 28, "byteLength": 16 } @@ -18224,9 +18224,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 492, + "startLine": 495, "startColumn": 12, - "endLine": 492, + "endLine": 495, "endColumn": 28, "byteLength": 16 } @@ -18249,9 +18249,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 493, + "startLine": 496, "startColumn": 12, - "endLine": 493, + "endLine": 496, "endColumn": 19, "byteLength": 7 } @@ -18274,9 +18274,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 491, "startColumn": 12, - "endLine": 488, + "endLine": 491, "endColumn": 19, "byteLength": 7 } @@ -18299,9 +18299,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 502, + "startLine": 505, "startColumn": 12, - "endLine": 502, + "endLine": 505, "endColumn": 19, "byteLength": 7 } @@ -18324,9 +18324,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 487, + "startLine": 490, "startColumn": 14, - "endLine": 487, + "endLine": 490, "endColumn": 21, "byteLength": 7 } @@ -18487,9 +18487,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 131, + "startLine": 134, "startColumn": 29, - "endLine": 131, + "endLine": 134, "endColumn": 53, "byteLength": 24 } @@ -18510,9 +18510,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 133, + "startLine": 136, "startColumn": 28, - "endLine": 133, + "endLine": 136, "endColumn": 64, "byteLength": 36 } @@ -18558,9 +18558,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 132, + "startLine": 135, "startColumn": 12, - "endLine": 132, + "endLine": 135, "endColumn": 19, "byteLength": 7 } @@ -18581,9 +18581,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 218, + "startLine": 221, "startColumn": 12, - "endLine": 218, + "endLine": 221, "endColumn": 13, "byteLength": 1 } @@ -18604,9 +18604,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 212, + "startLine": 215, "startColumn": 29, - "endLine": 212, + "endLine": 215, "endColumn": 49, "byteLength": 20 } @@ -18627,9 +18627,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 213, + "startLine": 216, "startColumn": 34, - "endLine": 213, + "endLine": 216, "endColumn": 59, "byteLength": 25 } @@ -18650,9 +18650,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 216, + "startLine": 219, "startColumn": 4, - "endLine": 216, + "endLine": 219, "endColumn": 60, "byteLength": 56 } @@ -18673,9 +18673,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 218, + "startLine": 221, "startColumn": 12, - "endLine": 218, + "endLine": 221, "endColumn": 13, "byteLength": 1 } @@ -18698,9 +18698,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 214, + "startLine": 217, "startColumn": 12, - "endLine": 214, + "endLine": 217, "endColumn": 19, "byteLength": 7 } @@ -18813,9 +18813,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 181, + "startLine": 184, "startColumn": 29, - "endLine": 181, + "endLine": 184, "endColumn": 49, "byteLength": 20 } @@ -18836,9 +18836,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 184, + "startLine": 187, "startColumn": 24, - "endLine": 184, + "endLine": 187, "endColumn": 35, "byteLength": 11 } @@ -18859,9 +18859,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 189, + "startLine": 192, "startColumn": 28, - "endLine": 189, + "endLine": 192, "endColumn": 40, "byteLength": 12 } @@ -18882,9 +18882,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 185, + "startLine": 188, "startColumn": 25, - "endLine": 185, + "endLine": 188, "endColumn": 38, "byteLength": 13 } @@ -18905,9 +18905,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 186, + "startLine": 189, "startColumn": 30, - "endLine": 186, + "endLine": 189, "endColumn": 66, "byteLength": 36 } @@ -18928,9 +18928,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 187, + "startLine": 190, "startColumn": 33, - "endLine": 187, + "endLine": 190, "endColumn": 59, "byteLength": 26 } @@ -18951,9 +18951,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 190, + "startLine": 193, "startColumn": 25, - "endLine": 190, + "endLine": 193, "endColumn": 41, "byteLength": 16 } @@ -18974,9 +18974,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 193, + "startLine": 196, "startColumn": 4, - "endLine": 193, + "endLine": 196, "endColumn": 60, "byteLength": 56 } @@ -19022,9 +19022,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 182, + "startLine": 185, "startColumn": 12, - "endLine": 182, + "endLine": 185, "endColumn": 19, "byteLength": 7 } @@ -19093,9 +19093,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 334, + "startLine": 337, "startColumn": 12, - "endLine": 334, + "endLine": 337, "endColumn": 13, "byteLength": 1 } @@ -19116,9 +19116,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 329, + "startLine": 332, "startColumn": 35, - "endLine": 329, + "endLine": 332, "endColumn": 76, "byteLength": 41 } @@ -19139,9 +19139,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 330, + "startLine": 333, "startColumn": 33, - "endLine": 330, + "endLine": 333, "endColumn": 57, "byteLength": 24 } @@ -19162,9 +19162,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 331, + "startLine": 334, "startColumn": 12, - "endLine": 331, + "endLine": 334, "endColumn": 20, "byteLength": 8 } @@ -19187,9 +19187,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 331, + "startLine": 334, "startColumn": 12, - "endLine": 331, + "endLine": 334, "endColumn": 20, "byteLength": 8 } @@ -19212,9 +19212,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 332, + "startLine": 335, "startColumn": 12, - "endLine": 332, + "endLine": 335, "endColumn": 19, "byteLength": 7 } @@ -19235,11 +19235,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 323, + "startLine": 322, "startColumn": 5, "endLine": 333, "endColumn": 1, - "byteLength": 190 + "byteLength": 224 } } } @@ -19258,9 +19258,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 519, + "startLine": 522, "startColumn": 33, - "endLine": 519, + "endLine": 522, "endColumn": 60, "byteLength": 27 } @@ -19281,9 +19281,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 520, + "startLine": 523, "startColumn": 35, - "endLine": 520, + "endLine": 523, "endColumn": 51, "byteLength": 16 } @@ -19304,9 +19304,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 521, + "startLine": 524, "startColumn": 33, - "endLine": 521, + "endLine": 524, "endColumn": 59, "byteLength": 26 } @@ -19327,11 +19327,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 323, + "startLine": 322, "startColumn": 5, "endLine": 333, "endColumn": 1, - "byteLength": 190 + "byteLength": 224 } } } @@ -19352,9 +19352,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 518, + "startLine": 521, "startColumn": 12, - "endLine": 518, + "endLine": 521, "endColumn": 19, "byteLength": 7 } @@ -19423,9 +19423,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 210, + "startLine": 213, "startColumn": 14, - "endLine": 210, + "endLine": 213, "endColumn": 20, "byteLength": 6 } @@ -19446,9 +19446,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 204, + "startLine": 207, "startColumn": 29, - "endLine": 204, + "endLine": 207, "endColumn": 49, "byteLength": 20 } @@ -19469,9 +19469,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 205, + "startLine": 208, "startColumn": 34, - "endLine": 205, + "endLine": 208, "endColumn": 59, "byteLength": 25 } @@ -19492,9 +19492,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 208, + "startLine": 211, "startColumn": 28, - "endLine": 208, + "endLine": 211, "endColumn": 53, "byteLength": 25 } @@ -19515,9 +19515,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 206, + "startLine": 209, "startColumn": 12, - "endLine": 206, + "endLine": 209, "endColumn": 19, "byteLength": 7 } @@ -19540,9 +19540,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 206, + "startLine": 209, "startColumn": 12, - "endLine": 206, + "endLine": 209, "endColumn": 19, "byteLength": 7 } @@ -19565,9 +19565,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 207, + "startLine": 210, "startColumn": 12, - "endLine": 207, + "endLine": 210, "endColumn": 19, "byteLength": 7 } @@ -19611,9 +19611,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 220, + "startLine": 223, "startColumn": 36, - "endLine": 220, + "endLine": 223, "endColumn": 63, "byteLength": 27 } @@ -19634,9 +19634,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 221, + "startLine": 224, "startColumn": 34, - "endLine": 221, + "endLine": 224, "endColumn": 59, "byteLength": 25 } @@ -19657,9 +19657,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 225, + "startLine": 228, "startColumn": 4, - "endLine": 227, + "endLine": 230, "endColumn": 59, "byteLength": 141 } @@ -19705,9 +19705,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 222, + "startLine": 225, "startColumn": 12, - "endLine": 222, + "endLine": 225, "endColumn": 19, "byteLength": 7 } @@ -20718,9 +20718,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -20741,9 +20741,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -20764,9 +20764,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -20787,9 +20787,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 245, + "startLine": 248, "startColumn": 31, - "endLine": 245, + "endLine": 248, "endColumn": 55, "byteLength": 24 } @@ -20810,9 +20810,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 258, + "startLine": 261, "startColumn": 6, - "endLine": 260, + "endLine": 263, "endColumn": 70, "byteLength": 120 } @@ -20833,9 +20833,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 268, + "startLine": 271, "startColumn": 29, - "endLine": 268, + "endLine": 271, "endColumn": 53, "byteLength": 24 } @@ -20856,9 +20856,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 256, + "startLine": 259, "startColumn": 24, - "endLine": 256, + "endLine": 259, "endColumn": 34, "byteLength": 10 } @@ -20879,9 +20879,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 267, + "startLine": 270, "startColumn": 20, - "endLine": 267, + "endLine": 270, "endColumn": 30, "byteLength": 10 } @@ -20902,9 +20902,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 264, + "startLine": 267, "startColumn": 27, - "endLine": 264, + "endLine": 267, "endColumn": 72, "byteLength": 45 } @@ -20925,9 +20925,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 265, + "startLine": 268, "startColumn": 24, - "endLine": 265, + "endLine": 268, "endColumn": 57, "byteLength": 33 } @@ -20948,9 +20948,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 277, + "startLine": 280, "startColumn": 27, - "endLine": 278, + "endLine": 281, "endColumn": 72, "byteLength": 92 } @@ -20971,9 +20971,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 279, + "startLine": 282, "startColumn": 24, - "endLine": 279, + "endLine": 282, "endColumn": 77, "byteLength": 53 } @@ -20994,9 +20994,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 246, + "startLine": 249, "startColumn": 10, - "endLine": 246, + "endLine": 249, "endColumn": 16, "byteLength": 6 } @@ -21017,9 +21017,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 261, + "startLine": 264, "startColumn": 12, - "endLine": 261, + "endLine": 264, "endColumn": 27, "byteLength": 15 } @@ -21040,9 +21040,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 269, + "startLine": 272, "startColumn": 12, - "endLine": 269, + "endLine": 272, "endColumn": 32, "byteLength": 20 } @@ -21065,9 +21065,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 246, + "startLine": 249, "startColumn": 10, - "endLine": 246, + "endLine": 249, "endColumn": 16, "byteLength": 6 } @@ -21091,9 +21091,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 248, + "startLine": 251, "startColumn": 10, - "endLine": 248, + "endLine": 251, "endColumn": 30, "byteLength": 20 } @@ -21116,9 +21116,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 250, + "startLine": 253, "startColumn": 10, - "endLine": 250, + "endLine": 253, "endColumn": 17, "byteLength": 7 } @@ -21141,9 +21141,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 252, + "startLine": 255, "startColumn": 10, - "endLine": 252, + "endLine": 255, "endColumn": 25, "byteLength": 15 } @@ -21166,9 +21166,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 261, + "startLine": 264, "startColumn": 12, - "endLine": 261, + "endLine": 264, "endColumn": 27, "byteLength": 15 } @@ -21191,9 +21191,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 262, + "startLine": 265, "startColumn": 12, - "endLine": 262, + "endLine": 265, "endColumn": 18, "byteLength": 6 } @@ -21216,9 +21216,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 263, + "startLine": 266, "startColumn": 12, - "endLine": 263, + "endLine": 266, "endColumn": 19, "byteLength": 7 } @@ -21242,9 +21242,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 269, + "startLine": 272, "startColumn": 12, - "endLine": 269, + "endLine": 272, "endColumn": 32, "byteLength": 20 } @@ -21267,9 +21267,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 272, + "startLine": 275, "startColumn": 12, - "endLine": 272, + "endLine": 275, "endColumn": 27, "byteLength": 15 } @@ -21292,9 +21292,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 275, + "startLine": 278, "startColumn": 12, - "endLine": 275, + "endLine": 278, "endColumn": 19, "byteLength": 7 } @@ -21315,9 +21315,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -21338,9 +21338,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -21361,9 +21361,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -21384,9 +21384,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -21407,9 +21407,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -21430,9 +21430,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 286, + "startLine": 289, "startColumn": 31, - "endLine": 286, + "endLine": 289, "endColumn": 55, "byteLength": 24 } @@ -21453,9 +21453,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 287, + "startLine": 290, "startColumn": 26, - "endLine": 287, + "endLine": 290, "endColumn": 41, "byteLength": 15 } @@ -21476,9 +21476,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 300, + "startLine": 303, "startColumn": 6, - "endLine": 302, + "endLine": 305, "endColumn": 70, "byteLength": 120 } @@ -21499,9 +21499,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 311, + "startLine": 314, "startColumn": 29, - "endLine": 311, + "endLine": 314, "endColumn": 46, "byteLength": 17 } @@ -21522,9 +21522,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 312, + "startLine": 315, "startColumn": 37, - "endLine": 312, + "endLine": 315, "endColumn": 58, "byteLength": 21 } @@ -21545,9 +21545,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 298, + "startLine": 301, "startColumn": 24, - "endLine": 298, + "endLine": 301, "endColumn": 34, "byteLength": 10 } @@ -21568,9 +21568,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 310, + "startLine": 313, "startColumn": 20, - "endLine": 310, + "endLine": 313, "endColumn": 30, "byteLength": 10 } @@ -21591,9 +21591,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 306, + "startLine": 309, "startColumn": 27, - "endLine": 306, + "endLine": 309, "endColumn": 72, "byteLength": 45 } @@ -21614,9 +21614,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 307, + "startLine": 310, "startColumn": 28, - "endLine": 307, + "endLine": 310, "endColumn": 49, "byteLength": 21 } @@ -21637,9 +21637,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 308, + "startLine": 311, "startColumn": 28, - "endLine": 308, + "endLine": 311, "endColumn": 54, "byteLength": 26 } @@ -21660,9 +21660,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 321, + "startLine": 324, "startColumn": 27, - "endLine": 322, + "endLine": 325, "endColumn": 65, "byteLength": 85 } @@ -21683,9 +21683,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 323, + "startLine": 326, "startColumn": 28, - "endLine": 323, + "endLine": 326, "endColumn": 67, "byteLength": 39 } @@ -21706,9 +21706,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 288, + "startLine": 291, "startColumn": 10, - "endLine": 288, + "endLine": 291, "endColumn": 16, "byteLength": 6 } @@ -21729,9 +21729,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 303, + "startLine": 306, "startColumn": 12, - "endLine": 303, + "endLine": 306, "endColumn": 20, "byteLength": 8 } @@ -21752,9 +21752,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 313, + "startLine": 316, "startColumn": 12, - "endLine": 313, + "endLine": 316, "endColumn": 27, "byteLength": 15 } @@ -21777,9 +21777,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 288, + "startLine": 291, "startColumn": 10, - "endLine": 288, + "endLine": 291, "endColumn": 16, "byteLength": 6 } @@ -21803,9 +21803,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 290, + "startLine": 293, "startColumn": 10, - "endLine": 290, + "endLine": 293, "endColumn": 25, "byteLength": 15 } @@ -21828,9 +21828,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 292, + "startLine": 295, "startColumn": 10, - "endLine": 292, + "endLine": 295, "endColumn": 17, "byteLength": 7 } @@ -21853,9 +21853,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 294, + "startLine": 297, "startColumn": 10, - "endLine": 294, + "endLine": 297, "endColumn": 18, "byteLength": 8 } @@ -21878,9 +21878,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 303, + "startLine": 306, "startColumn": 12, - "endLine": 303, + "endLine": 306, "endColumn": 20, "byteLength": 8 } @@ -21903,9 +21903,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 304, + "startLine": 307, "startColumn": 12, - "endLine": 304, + "endLine": 307, "endColumn": 18, "byteLength": 6 } @@ -21928,9 +21928,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 305, + "startLine": 308, "startColumn": 12, - "endLine": 305, + "endLine": 308, "endColumn": 19, "byteLength": 7 } @@ -21954,9 +21954,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 313, + "startLine": 316, "startColumn": 12, - "endLine": 313, + "endLine": 316, "endColumn": 27, "byteLength": 15 } @@ -21979,9 +21979,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 316, + "startLine": 319, "startColumn": 12, - "endLine": 316, + "endLine": 319, "endColumn": 20, "byteLength": 8 } @@ -22004,9 +22004,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 319, + "startLine": 322, "startColumn": 12, - "endLine": 319, + "endLine": 322, "endColumn": 19, "byteLength": 7 } @@ -22027,9 +22027,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -22050,9 +22050,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -24640,9 +24640,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 463, + "startLine": 466, "startColumn": 14, - "endLine": 463, + "endLine": 466, "endColumn": 21, "byteLength": 7 } @@ -24663,9 +24663,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 458, + "startLine": 461, "startColumn": 25, - "endLine": 458, + "endLine": 461, "endColumn": 48, "byteLength": 23 } @@ -24686,9 +24686,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 459, + "startLine": 462, "startColumn": 31, - "endLine": 459, + "endLine": 462, "endColumn": 53, "byteLength": 22 } @@ -24709,9 +24709,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 460, + "startLine": 463, "startColumn": 12, - "endLine": 460, + "endLine": 463, "endColumn": 26, "byteLength": 14 } @@ -24735,9 +24735,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 460, + "startLine": 463, "startColumn": 12, - "endLine": 460, + "endLine": 463, "endColumn": 26, "byteLength": 14 } @@ -24760,9 +24760,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 461, + "startLine": 464, "startColumn": 12, - "endLine": 461, + "endLine": 464, "endColumn": 19, "byteLength": 7 } diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif index f9bed3f4deea0fcb4cbf40cb71c14458a221fb72..2e65770160b67d52666d872c32c3ccff177cf6d1 100644 --- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif +++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif @@ -1885,9 +1885,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 101, + "startLine": 104, "startColumn": 12, - "endLine": 101, + "endLine": 104, "endColumn": 13, "byteLength": 1 } @@ -1908,9 +1908,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 92, + "startLine": 95, "startColumn": 25, - "endLine": 92, + "endLine": 95, "endColumn": 48, "byteLength": 23 } @@ -1931,9 +1931,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 93, + "startLine": 96, "startColumn": 24, - "endLine": 93, + "endLine": 96, "endColumn": 51, "byteLength": 27 } @@ -1954,9 +1954,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 95, + "startLine": 98, "startColumn": 4, - "endLine": 95, + "endLine": 98, "endColumn": 62, "byteLength": 58 } @@ -1977,9 +1977,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 98, + "startLine": 101, "startColumn": 29, - "endLine": 98, + "endLine": 101, "endColumn": 76, "byteLength": 47 } @@ -2000,9 +2000,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 99, + "startLine": 102, "startColumn": 24, - "endLine": 99, + "endLine": 102, "endColumn": 39, "byteLength": 15 } @@ -2023,9 +2023,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 96, + "startLine": 99, "startColumn": 12, - "endLine": 96, + "endLine": 99, "endColumn": 35, "byteLength": 23 } @@ -2049,9 +2049,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 96, + "startLine": 99, "startColumn": 12, - "endLine": 96, + "endLine": 99, "endColumn": 35, "byteLength": 23 } @@ -2074,9 +2074,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 97, + "startLine": 100, "startColumn": 12, - "endLine": 97, + "endLine": 100, "endColumn": 19, "byteLength": 7 } @@ -2097,9 +2097,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 111, + "startLine": 114, "startColumn": 12, - "endLine": 111, + "endLine": 114, "endColumn": 13, "byteLength": 1 } @@ -2120,9 +2120,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 104, + "startLine": 107, "startColumn": 25, - "endLine": 104, + "endLine": 107, "endColumn": 48, "byteLength": 23 } @@ -2143,9 +2143,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 105, + "startLine": 108, "startColumn": 24, - "endLine": 105, + "endLine": 108, "endColumn": 51, "byteLength": 27 } @@ -2166,9 +2166,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 108, + "startLine": 111, "startColumn": 29, - "endLine": 108, + "endLine": 111, "endColumn": 76, "byteLength": 47 } @@ -2189,9 +2189,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 109, + "startLine": 112, "startColumn": 24, - "endLine": 109, + "endLine": 112, "endColumn": 39, "byteLength": 15 } @@ -2212,9 +2212,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 106, + "startLine": 109, "startColumn": 12, - "endLine": 106, + "endLine": 109, "endColumn": 35, "byteLength": 23 } @@ -2238,9 +2238,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 106, + "startLine": 109, "startColumn": 12, - "endLine": 106, + "endLine": 109, "endColumn": 35, "byteLength": 23 } @@ -2263,9 +2263,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 107, + "startLine": 110, "startColumn": 12, - "endLine": 107, + "endLine": 110, "endColumn": 19, "byteLength": 7 } @@ -2286,9 +2286,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 121, + "startLine": 124, "startColumn": 12, - "endLine": 121, + "endLine": 124, "endColumn": 13, "byteLength": 1 } @@ -2309,9 +2309,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 115, + "startLine": 118, "startColumn": 22, - "endLine": 115, + "endLine": 118, "endColumn": 42, "byteLength": 20 } @@ -2332,9 +2332,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 118, + "startLine": 121, "startColumn": 26, - "endLine": 118, + "endLine": 121, "endColumn": 46, "byteLength": 20 } @@ -2355,9 +2355,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 119, + "startLine": 122, "startColumn": 24, - "endLine": 119, + "endLine": 122, "endColumn": 36, "byteLength": 12 } @@ -2378,9 +2378,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 119, "startColumn": 12, - "endLine": 116, + "endLine": 119, "endColumn": 32, "byteLength": 20 } @@ -2404,9 +2404,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 119, "startColumn": 12, - "endLine": 116, + "endLine": 119, "endColumn": 32, "byteLength": 20 } @@ -2429,9 +2429,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 117, + "startLine": 120, "startColumn": 12, - "endLine": 117, + "endLine": 120, "endColumn": 19, "byteLength": 7 } @@ -2452,9 +2452,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 405, + "startLine": 408, "startColumn": 12, - "endLine": 405, + "endLine": 408, "endColumn": 13, "byteLength": 1 } @@ -2475,9 +2475,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 396, + "startLine": 399, "startColumn": 31, - "endLine": 396, + "endLine": 399, "endColumn": 53, "byteLength": 22 } @@ -2498,9 +2498,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 397, + "startLine": 400, "startColumn": 26, - "endLine": 397, + "endLine": 400, "endColumn": 55, "byteLength": 29 } @@ -2521,9 +2521,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 399, + "startLine": 402, "startColumn": 4, - "endLine": 399, + "endLine": 402, "endColumn": 59, "byteLength": 55 } @@ -2544,9 +2544,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 402, + "startLine": 405, "startColumn": 28, - "endLine": 402, + "endLine": 405, "endColumn": 49, "byteLength": 21 } @@ -2567,9 +2567,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 406, "startColumn": 27, - "endLine": 403, + "endLine": 406, "endColumn": 57, "byteLength": 30 } @@ -2590,9 +2590,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 400, + "startLine": 403, "startColumn": 12, - "endLine": 400, + "endLine": 403, "endColumn": 32, "byteLength": 20 } @@ -2616,9 +2616,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 400, + "startLine": 403, "startColumn": 12, - "endLine": 400, + "endLine": 403, "endColumn": 32, "byteLength": 20 } @@ -2641,9 +2641,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 401, + "startLine": 404, "startColumn": 12, - "endLine": 401, + "endLine": 404, "endColumn": 19, "byteLength": 7 } @@ -2781,9 +2781,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 239, + "startLine": 242, "startColumn": 12, - "endLine": 239, + "endLine": 242, "endColumn": 13, "byteLength": 1 } @@ -2804,9 +2804,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 231, + "startLine": 234, "startColumn": 36, - "endLine": 231, + "endLine": 234, "endColumn": 63, "byteLength": 27 } @@ -2827,9 +2827,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 232, + "startLine": 235, "startColumn": 34, - "endLine": 232, + "endLine": 235, "endColumn": 59, "byteLength": 25 } @@ -2850,9 +2850,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 236, + "startLine": 239, "startColumn": 4, - "endLine": 237, + "endLine": 240, "endColumn": 65, "byteLength": 82 } @@ -2873,9 +2873,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 239, + "startLine": 242, "startColumn": 12, - "endLine": 239, + "endLine": 242, "endColumn": 13, "byteLength": 1 } @@ -2898,9 +2898,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 233, + "startLine": 236, "startColumn": 12, - "endLine": 233, + "endLine": 236, "endColumn": 19, "byteLength": 7 } @@ -2921,9 +2921,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 420, + "startLine": 423, "startColumn": 12, - "endLine": 420, + "endLine": 423, "endColumn": 13, "byteLength": 1 } @@ -2944,9 +2944,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 408, + "startLine": 411, "startColumn": 31, - "endLine": 408, + "endLine": 411, "endColumn": 53, "byteLength": 22 } @@ -2967,9 +2967,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 409, + "startLine": 412, "startColumn": 32, - "endLine": 409, + "endLine": 412, "endColumn": 50, "byteLength": 18 } @@ -2990,9 +2990,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 410, + "startLine": 413, "startColumn": 26, - "endLine": 410, + "endLine": 413, "endColumn": 70, "byteLength": 44 } @@ -3013,9 +3013,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 413, + "startLine": 416, "startColumn": 28, - "endLine": 413, + "endLine": 416, "endColumn": 76, "byteLength": 48 } @@ -3036,9 +3036,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 416, + "startLine": 419, "startColumn": 4, - "endLine": 416, + "endLine": 419, "endColumn": 60, "byteLength": 56 } @@ -3059,9 +3059,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 417, + "startLine": 420, "startColumn": 34, - "endLine": 417, + "endLine": 420, "endColumn": 77, "byteLength": 43 } @@ -3082,9 +3082,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 418, + "startLine": 421, "startColumn": 24, - "endLine": 418, + "endLine": 421, "endColumn": 39, "byteLength": 15 } @@ -3105,9 +3105,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 411, + "startLine": 414, "startColumn": 12, - "endLine": 411, + "endLine": 414, "endColumn": 58, "byteLength": 46 } @@ -3131,9 +3131,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 411, + "startLine": 414, "startColumn": 12, - "endLine": 411, + "endLine": 414, "endColumn": 58, "byteLength": 46 } @@ -3156,9 +3156,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 414, + "startLine": 417, "startColumn": 12, - "endLine": 414, + "endLine": 417, "endColumn": 19, "byteLength": 7 } @@ -3179,9 +3179,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 173, + "startLine": 176, "startColumn": 12, - "endLine": 173, + "endLine": 176, "endColumn": 13, "byteLength": 1 } @@ -3202,9 +3202,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 173, + "startLine": 176, "startColumn": 12, - "endLine": 173, + "endLine": 176, "endColumn": 13, "byteLength": 1 } @@ -3225,9 +3225,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 173, + "startLine": 176, "startColumn": 12, - "endLine": 173, + "endLine": 176, "endColumn": 13, "byteLength": 1 } @@ -3248,9 +3248,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 173, + "startLine": 176, "startColumn": 12, - "endLine": 173, + "endLine": 176, "endColumn": 13, "byteLength": 1 } @@ -3271,9 +3271,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 157, + "startLine": 160, "startColumn": 29, - "endLine": 157, + "endLine": 160, "endColumn": 49, "byteLength": 20 } @@ -3294,9 +3294,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 160, + "startLine": 163, "startColumn": 24, - "endLine": 160, + "endLine": 163, "endColumn": 35, "byteLength": 11 } @@ -3317,9 +3317,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 167, + "startLine": 170, "startColumn": 28, - "endLine": 167, + "endLine": 170, "endColumn": 40, "byteLength": 12 } @@ -3340,9 +3340,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 161, + "startLine": 164, "startColumn": 25, - "endLine": 161, + "endLine": 164, "endColumn": 44, "byteLength": 19 } @@ -3363,9 +3363,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 162, + "startLine": 165, "startColumn": 30, - "endLine": 162, + "endLine": 165, "endColumn": 66, "byteLength": 36 } @@ -3386,9 +3386,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 163, + "startLine": 166, "startColumn": 30, - "endLine": 163, + "endLine": 166, "endColumn": 59, "byteLength": 29 } @@ -3409,9 +3409,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 164, + "startLine": 167, "startColumn": 33, - "endLine": 164, + "endLine": 167, "endColumn": 59, "byteLength": 26 } @@ -3432,9 +3432,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 165, + "startLine": 168, "startColumn": 32, - "endLine": 165, + "endLine": 168, "endColumn": 79, "byteLength": 47 } @@ -3455,9 +3455,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 168, + "startLine": 171, "startColumn": 25, - "endLine": 168, + "endLine": 171, "endColumn": 41, "byteLength": 16 } @@ -3478,9 +3478,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 171, + "startLine": 174, "startColumn": 4, - "endLine": 171, + "endLine": 174, "endColumn": 60, "byteLength": 56 } @@ -3501,9 +3501,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 173, + "startLine": 176, "startColumn": 12, - "endLine": 173, + "endLine": 176, "endColumn": 13, "byteLength": 1 } @@ -3526,9 +3526,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 158, + "startLine": 161, "startColumn": 12, - "endLine": 158, + "endLine": 161, "endColumn": 19, "byteLength": 7 } @@ -3549,9 +3549,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 179, + "startLine": 182, "startColumn": 12, - "endLine": 179, + "endLine": 182, "endColumn": 13, "byteLength": 1 } @@ -3572,9 +3572,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 175, + "startLine": 178, "startColumn": 29, - "endLine": 175, + "endLine": 178, "endColumn": 49, "byteLength": 20 } @@ -3595,9 +3595,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 177, + "startLine": 180, "startColumn": 30, - "endLine": 177, + "endLine": 180, "endColumn": 64, "byteLength": 34 } @@ -3618,9 +3618,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 179, + "startLine": 182, "startColumn": 12, - "endLine": 179, + "endLine": 182, "endColumn": 13, "byteLength": 1 } @@ -3643,9 +3643,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 176, + "startLine": 179, "startColumn": 12, - "endLine": 176, + "endLine": 179, "endColumn": 19, "byteLength": 7 } @@ -3666,9 +3666,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 142, + "startLine": 145, "startColumn": 11, - "endLine": 142, + "endLine": 145, "endColumn": 17, "byteLength": 6 } @@ -3689,9 +3689,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 137, + "startLine": 140, "startColumn": 30, - "endLine": 137, + "endLine": 140, "endColumn": 51, "byteLength": 21 } @@ -3712,9 +3712,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 138, + "startLine": 141, "startColumn": 30, - "endLine": 138, + "endLine": 141, "endColumn": 51, "byteLength": 21 } @@ -3735,9 +3735,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 140, + "startLine": 143, "startColumn": 26, - "endLine": 140, + "endLine": 143, "endColumn": 50, "byteLength": 24 } @@ -3758,9 +3758,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 142, + "startLine": 145, "startColumn": 11, - "endLine": 142, + "endLine": 145, "endColumn": 17, "byteLength": 6 } @@ -3783,9 +3783,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 139, + "startLine": 142, "startColumn": 12, - "endLine": 139, + "endLine": 142, "endColumn": 19, "byteLength": 7 } @@ -3806,9 +3806,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 155, + "startLine": 158, "startColumn": 11, - "endLine": 155, + "endLine": 158, "endColumn": 18, "byteLength": 7 } @@ -3829,9 +3829,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 151, + "startLine": 154, "startColumn": 30, - "endLine": 151, + "endLine": 154, "endColumn": 51, "byteLength": 21 } @@ -3852,9 +3852,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 152, + "startLine": 155, "startColumn": 30, - "endLine": 152, + "endLine": 155, "endColumn": 51, "byteLength": 21 } @@ -3875,9 +3875,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 155, + "startLine": 158, "startColumn": 11, - "endLine": 155, + "endLine": 158, "endColumn": 18, "byteLength": 7 } @@ -3900,9 +3900,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 153, + "startLine": 156, "startColumn": 12, - "endLine": 153, + "endLine": 156, "endColumn": 19, "byteLength": 7 } @@ -3923,9 +3923,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 360, + "startLine": 363, "startColumn": 12, - "endLine": 360, + "endLine": 363, "endColumn": 13, "byteLength": 1 } @@ -3946,9 +3946,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 351, + "startLine": 354, "startColumn": 31, - "endLine": 351, + "endLine": 354, "endColumn": 53, "byteLength": 22 } @@ -3969,9 +3969,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 352, + "startLine": 355, "startColumn": 26, - "endLine": 352, + "endLine": 355, "endColumn": 55, "byteLength": 29 } @@ -3992,9 +3992,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 354, + "startLine": 357, "startColumn": 4, - "endLine": 354, + "endLine": 357, "endColumn": 59, "byteLength": 55 } @@ -4015,9 +4015,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 357, + "startLine": 360, "startColumn": 28, - "endLine": 357, + "endLine": 360, "endColumn": 49, "byteLength": 21 } @@ -4038,9 +4038,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 358, + "startLine": 361, "startColumn": 24, - "endLine": 358, + "endLine": 361, "endColumn": 39, "byteLength": 15 } @@ -4061,9 +4061,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 355, + "startLine": 358, "startColumn": 12, - "endLine": 355, + "endLine": 358, "endColumn": 32, "byteLength": 20 } @@ -4087,9 +4087,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 355, + "startLine": 358, "startColumn": 12, - "endLine": 355, + "endLine": 358, "endColumn": 32, "byteLength": 20 } @@ -4112,9 +4112,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 356, + "startLine": 359, "startColumn": 12, - "endLine": 356, + "endLine": 359, "endColumn": 19, "byteLength": 7 } @@ -4135,9 +4135,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 202, + "startLine": 205, "startColumn": 14, - "endLine": 202, + "endLine": 205, "endColumn": 21, "byteLength": 7 } @@ -4158,9 +4158,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 197, + "startLine": 200, "startColumn": 29, - "endLine": 197, + "endLine": 200, "endColumn": 49, "byteLength": 20 } @@ -4181,9 +4181,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 198, + "startLine": 201, "startColumn": 34, - "endLine": 198, + "endLine": 201, "endColumn": 59, "byteLength": 25 } @@ -4204,9 +4204,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 200, + "startLine": 203, "startColumn": 28, - "endLine": 200, + "endLine": 203, "endColumn": 53, "byteLength": 25 } @@ -4227,9 +4227,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 202, + "startLine": 205, "startColumn": 14, - "endLine": 202, + "endLine": 205, "endColumn": 21, "byteLength": 7 } @@ -4252,9 +4252,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 199, + "startLine": 202, "startColumn": 12, - "endLine": 199, + "endLine": 202, "endColumn": 19, "byteLength": 7 } @@ -4275,9 +4275,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 484, + "startLine": 487, "startColumn": 12, - "endLine": 484, + "endLine": 487, "endColumn": 13, "byteLength": 1 } @@ -4298,9 +4298,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 484, + "startLine": 487, "startColumn": 12, - "endLine": 484, + "endLine": 487, "endColumn": 13, "byteLength": 1 } @@ -4321,9 +4321,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 484, + "startLine": 487, "startColumn": 12, - "endLine": 484, + "endLine": 487, "endColumn": 13, "byteLength": 1 } @@ -4344,9 +4344,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 468, + "startLine": 471, "startColumn": 29, - "endLine": 468, + "endLine": 471, "endColumn": 49, "byteLength": 20 } @@ -4367,9 +4367,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 472, + "startLine": 475, "startColumn": 26, - "endLine": 472, + "endLine": 475, "endColumn": 49, "byteLength": 23 } @@ -4390,9 +4390,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 479, + "startLine": 482, "startColumn": 29, - "endLine": 479, + "endLine": 482, "endColumn": 53, "byteLength": 24 } @@ -4413,9 +4413,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 475, + "startLine": 478, "startColumn": 24, - "endLine": 475, + "endLine": 478, "endColumn": 49, "byteLength": 25 } @@ -4436,9 +4436,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 477, + "startLine": 480, "startColumn": 4, - "endLine": 477, + "endLine": 480, "endColumn": 51, "byteLength": 47 } @@ -4459,9 +4459,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 482, + "startLine": 485, "startColumn": 25, - "endLine": 482, + "endLine": 485, "endColumn": 41, "byteLength": 16 } @@ -4482,9 +4482,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 473, + "startLine": 476, "startColumn": 12, - "endLine": 473, + "endLine": 476, "endColumn": 28, "byteLength": 16 } @@ -4505,9 +4505,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 484, + "startLine": 487, "startColumn": 12, - "endLine": 484, + "endLine": 487, "endColumn": 13, "byteLength": 1 } @@ -4528,9 +4528,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 484, + "startLine": 487, "startColumn": 12, - "endLine": 484, + "endLine": 487, "endColumn": 13, "byteLength": 1 } @@ -4554,9 +4554,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 473, + "startLine": 476, "startColumn": 12, - "endLine": 473, + "endLine": 476, "endColumn": 28, "byteLength": 16 } @@ -4579,9 +4579,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 474, + "startLine": 477, "startColumn": 12, - "endLine": 474, + "endLine": 477, "endColumn": 19, "byteLength": 7 } @@ -4604,9 +4604,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 470, + "startLine": 473, "startColumn": 12, - "endLine": 470, + "endLine": 473, "endColumn": 19, "byteLength": 7 } @@ -4629,9 +4629,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 480, + "startLine": 483, "startColumn": 12, - "endLine": 480, + "endLine": 483, "endColumn": 19, "byteLength": 7 } @@ -4652,9 +4652,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 469, + "startLine": 472, "startColumn": 14, - "endLine": 469, + "endLine": 472, "endColumn": 21, "byteLength": 7 } @@ -4675,9 +4675,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 484, + "startLine": 487, "startColumn": 12, - "endLine": 484, + "endLine": 487, "endColumn": 13, "byteLength": 1 } @@ -4698,9 +4698,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 347, + "startLine": 350, "startColumn": 12, - "endLine": 347, + "endLine": 350, "endColumn": 13, "byteLength": 1 } @@ -4721,9 +4721,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 343, + "startLine": 346, "startColumn": 33, - "endLine": 343, + "endLine": 346, "endColumn": 59, "byteLength": 26 } @@ -4744,9 +4744,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 344, + "startLine": 347, "startColumn": 35, - "endLine": 344, + "endLine": 347, "endColumn": 51, "byteLength": 16 } @@ -4767,9 +4767,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 345, + "startLine": 348, "startColumn": 33, - "endLine": 345, + "endLine": 348, "endColumn": 59, "byteLength": 26 } @@ -4790,9 +4790,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 347, + "startLine": 350, "startColumn": 12, - "endLine": 347, + "endLine": 350, "endColumn": 13, "byteLength": 1 } @@ -4815,9 +4815,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 342, + "startLine": 345, "startColumn": 12, - "endLine": 342, + "endLine": 345, "endColumn": 19, "byteLength": 7 } @@ -4838,9 +4838,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 455, + "startLine": 458, "startColumn": 14, - "endLine": 455, + "endLine": 458, "endColumn": 21, "byteLength": 7 } @@ -4861,9 +4861,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 448, + "startLine": 451, "startColumn": 31, - "endLine": 448, + "endLine": 451, "endColumn": 53, "byteLength": 22 } @@ -4884,9 +4884,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 449, + "startLine": 452, "startColumn": 32, - "endLine": 449, + "endLine": 452, "endColumn": 50, "byteLength": 18 } @@ -4907,9 +4907,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 450, + "startLine": 453, "startColumn": 27, - "endLine": 450, + "endLine": 453, "endColumn": 48, "byteLength": 21 } @@ -4930,9 +4930,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 453, + "startLine": 456, "startColumn": 28, - "endLine": 453, + "endLine": 456, "endColumn": 65, "byteLength": 37 } @@ -4953,9 +4953,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 451, + "startLine": 454, "startColumn": 12, - "endLine": 451, + "endLine": 454, "endColumn": 33, "byteLength": 21 } @@ -4979,9 +4979,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 451, + "startLine": 454, "startColumn": 12, - "endLine": 451, + "endLine": 454, "endColumn": 33, "byteLength": 21 } @@ -5004,9 +5004,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 455, "startColumn": 12, - "endLine": 452, + "endLine": 455, "endColumn": 19, "byteLength": 7 } @@ -5027,9 +5027,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 393, + "startLine": 396, "startColumn": 7, - "endLine": 393, + "endLine": 396, "endColumn": 14, "byteLength": 7 } @@ -5050,9 +5050,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 384, + "startLine": 387, "startColumn": 31, - "endLine": 384, + "endLine": 387, "endColumn": 53, "byteLength": 22 } @@ -5073,9 +5073,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 388, "startColumn": 27, - "endLine": 385, + "endLine": 388, "endColumn": 48, "byteLength": 21 } @@ -5096,9 +5096,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 387, + "startLine": 390, "startColumn": 4, - "endLine": 387, + "endLine": 390, "endColumn": 61, "byteLength": 57 } @@ -5119,9 +5119,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 390, + "startLine": 393, "startColumn": 28, - "endLine": 390, + "endLine": 393, "endColumn": 73, "byteLength": 45 } @@ -5142,9 +5142,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 391, + "startLine": 394, "startColumn": 28, - "endLine": 391, + "endLine": 394, "endColumn": 50, "byteLength": 22 } @@ -5165,9 +5165,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 388, + "startLine": 391, "startColumn": 12, - "endLine": 388, + "endLine": 391, "endColumn": 24, "byteLength": 12 } @@ -5191,9 +5191,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 388, + "startLine": 391, "startColumn": 12, - "endLine": 388, + "endLine": 391, "endColumn": 24, "byteLength": 12 } @@ -5216,9 +5216,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 389, + "startLine": 392, "startColumn": 12, - "endLine": 389, + "endLine": 392, "endColumn": 19, "byteLength": 7 } @@ -5239,9 +5239,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 129, + "startLine": 132, "startColumn": 14, - "endLine": 129, + "endLine": 132, "endColumn": 20, "byteLength": 6 } @@ -5262,9 +5262,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 125, + "startLine": 128, "startColumn": 29, - "endLine": 125, + "endLine": 128, "endColumn": 49, "byteLength": 20 } @@ -5285,9 +5285,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 127, + "startLine": 130, "startColumn": 26, - "endLine": 127, + "endLine": 130, "endColumn": 46, "byteLength": 20 } @@ -5308,9 +5308,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 129, + "startLine": 132, "startColumn": 14, - "endLine": 129, + "endLine": 132, "endColumn": 20, "byteLength": 6 } @@ -5333,9 +5333,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 126, + "startLine": 129, "startColumn": 12, - "endLine": 126, + "endLine": 129, "endColumn": 19, "byteLength": 7 } @@ -5473,9 +5473,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 444, + "startLine": 447, "startColumn": 12, - "endLine": 444, + "endLine": 447, "endColumn": 13, "byteLength": 1 } @@ -5496,9 +5496,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 444, + "startLine": 447, "startColumn": 12, - "endLine": 444, + "endLine": 447, "endColumn": 13, "byteLength": 1 } @@ -5519,9 +5519,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 444, + "startLine": 447, "startColumn": 12, - "endLine": 444, + "endLine": 447, "endColumn": 13, "byteLength": 1 } @@ -5542,9 +5542,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 423, + "startLine": 426, "startColumn": 32, - "endLine": 423, + "endLine": 426, "endColumn": 58, "byteLength": 26 } @@ -5565,9 +5565,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 424, + "startLine": 427, "startColumn": 32, - "endLine": 424, + "endLine": 427, "endColumn": 50, "byteLength": 18 } @@ -5588,9 +5588,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 430, + "startLine": 433, "startColumn": 26, - "endLine": 430, + "endLine": 433, "endColumn": 74, "byteLength": 48 } @@ -5611,9 +5611,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 438, + "startLine": 441, "startColumn": 26, - "endLine": 438, + "endLine": 441, "endColumn": 64, "byteLength": 38 } @@ -5634,9 +5634,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 429, + "startLine": 432, "startColumn": 35, - "endLine": 429, + "endLine": 432, "endColumn": 77, "byteLength": 42 } @@ -5657,9 +5657,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 437, + "startLine": 440, "startColumn": 4, - "endLine": 437, + "endLine": 440, "endColumn": 49, "byteLength": 45 } @@ -5680,9 +5680,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 427, + "startLine": 430, "startColumn": 24, - "endLine": 427, + "endLine": 430, "endColumn": 39, "byteLength": 15 } @@ -5703,9 +5703,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 434, + "startLine": 437, "startColumn": 28, - "endLine": 434, + "endLine": 437, "endColumn": 76, "byteLength": 48 } @@ -5726,9 +5726,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 442, + "startLine": 445, "startColumn": 36, - "endLine": 442, + "endLine": 445, "endColumn": 74, "byteLength": 38 } @@ -5749,9 +5749,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 431, + "startLine": 434, "startColumn": 12, - "endLine": 431, + "endLine": 434, "endColumn": 58, "byteLength": 46 } @@ -5772,9 +5772,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 425, + "startLine": 428, "startColumn": 12, - "endLine": 425, + "endLine": 428, "endColumn": 50, "byteLength": 38 } @@ -5795,9 +5795,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 439, + "startLine": 442, "startColumn": 12, - "endLine": 439, + "endLine": 442, "endColumn": 48, "byteLength": 36 } @@ -5821,9 +5821,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 431, + "startLine": 434, "startColumn": 12, - "endLine": 431, + "endLine": 434, "endColumn": 58, "byteLength": 46 } @@ -5846,9 +5846,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 433, + "startLine": 436, "startColumn": 12, - "endLine": 433, + "endLine": 436, "endColumn": 19, "byteLength": 7 } @@ -5872,9 +5872,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 425, + "startLine": 428, "startColumn": 12, - "endLine": 425, + "endLine": 428, "endColumn": 50, "byteLength": 38 } @@ -5897,9 +5897,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 426, + "startLine": 429, "startColumn": 12, - "endLine": 426, + "endLine": 429, "endColumn": 19, "byteLength": 7 } @@ -5923,9 +5923,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 439, + "startLine": 442, "startColumn": 12, - "endLine": 439, + "endLine": 442, "endColumn": 48, "byteLength": 36 } @@ -5948,9 +5948,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 441, + "startLine": 444, "startColumn": 12, - "endLine": 441, + "endLine": 444, "endColumn": 19, "byteLength": 7 } @@ -5971,9 +5971,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 149, + "startLine": 152, "startColumn": 11, - "endLine": 149, + "endLine": 152, "endColumn": 18, "byteLength": 7 } @@ -5994,9 +5994,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 144, + "startLine": 147, "startColumn": 30, - "endLine": 144, + "endLine": 147, "endColumn": 55, "byteLength": 25 } @@ -6017,9 +6017,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 145, + "startLine": 148, "startColumn": 30, - "endLine": 145, + "endLine": 148, "endColumn": 55, "byteLength": 25 } @@ -6040,9 +6040,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 147, + "startLine": 150, "startColumn": 26, - "endLine": 147, + "endLine": 150, "endColumn": 53, "byteLength": 27 } @@ -6063,9 +6063,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 149, + "startLine": 152, "startColumn": 11, - "endLine": 149, + "endLine": 152, "endColumn": 18, "byteLength": 7 } @@ -6088,9 +6088,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 146, + "startLine": 149, "startColumn": 12, - "endLine": 146, + "endLine": 149, "endColumn": 19, "byteLength": 7 } @@ -6111,9 +6111,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 378, + "startLine": 381, "startColumn": 12, - "endLine": 378, + "endLine": 381, "endColumn": 13, "byteLength": 1 } @@ -6134,9 +6134,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 378, + "startLine": 381, "startColumn": 12, - "endLine": 378, + "endLine": 381, "endColumn": 13, "byteLength": 1 } @@ -6157,9 +6157,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 378, + "startLine": 381, "startColumn": 12, - "endLine": 378, + "endLine": 381, "endColumn": 13, "byteLength": 1 } @@ -6180,9 +6180,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 363, + "startLine": 366, "startColumn": 32, - "endLine": 363, + "endLine": 366, "endColumn": 58, "byteLength": 26 } @@ -6203,9 +6203,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 364, + "startLine": 367, "startColumn": 27, - "endLine": 364, + "endLine": 367, "endColumn": 50, "byteLength": 23 } @@ -6226,9 +6226,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 366, + "startLine": 369, "startColumn": 4, - "endLine": 366, + "endLine": 369, "endColumn": 43, "byteLength": 39 } @@ -6249,9 +6249,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 372, + "startLine": 375, "startColumn": 22, - "endLine": 372, + "endLine": 375, "endColumn": 37, "byteLength": 15 } @@ -6272,9 +6272,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 375, + "startLine": 378, "startColumn": 26, - "endLine": 375, + "endLine": 378, "endColumn": 42, "byteLength": 16 } @@ -6295,9 +6295,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 369, + "startLine": 372, "startColumn": 24, - "endLine": 369, + "endLine": 372, "endColumn": 39, "byteLength": 15 } @@ -6318,9 +6318,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 370, + "startLine": 373, "startColumn": 28, - "endLine": 370, + "endLine": 373, "endColumn": 57, "byteLength": 29 } @@ -6341,9 +6341,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 373, + "startLine": 376, "startColumn": 30, - "endLine": 373, + "endLine": 376, "endColumn": 51, "byteLength": 21 } @@ -6364,9 +6364,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 376, + "startLine": 379, "startColumn": 26, - "endLine": 376, + "endLine": 379, "endColumn": 60, "byteLength": 34 } @@ -6387,9 +6387,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 367, + "startLine": 370, "startColumn": 12, - "endLine": 367, + "endLine": 370, "endColumn": 26, "byteLength": 14 } @@ -6413,9 +6413,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 367, + "startLine": 370, "startColumn": 12, - "endLine": 367, + "endLine": 370, "endColumn": 26, "byteLength": 14 } @@ -6438,9 +6438,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 368, + "startLine": 371, "startColumn": 12, - "endLine": 368, + "endLine": 371, "endColumn": 19, "byteLength": 7 } @@ -6461,9 +6461,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 506, + "startLine": 509, "startColumn": 12, - "endLine": 506, + "endLine": 509, "endColumn": 13, "byteLength": 1 } @@ -6484,9 +6484,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 506, + "startLine": 509, "startColumn": 12, - "endLine": 506, + "endLine": 509, "endColumn": 13, "byteLength": 1 } @@ -6509,9 +6509,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 506, + "startLine": 509, "startColumn": 12, - "endLine": 506, + "endLine": 509, "endColumn": 13, "byteLength": 1 } @@ -6532,9 +6532,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 486, + "startLine": 489, "startColumn": 29, - "endLine": 486, + "endLine": 489, "endColumn": 49, "byteLength": 20 } @@ -6555,9 +6555,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 491, + "startLine": 494, "startColumn": 26, - "endLine": 491, + "endLine": 494, "endColumn": 60, "byteLength": 34 } @@ -6578,9 +6578,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 501, + "startLine": 504, "startColumn": 29, - "endLine": 501, + "endLine": 504, "endColumn": 64, "byteLength": 35 } @@ -6601,9 +6601,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 495, + "startLine": 498, "startColumn": 24, - "endLine": 495, + "endLine": 498, "endColumn": 60, "byteLength": 36 } @@ -6626,9 +6626,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 497, + "startLine": 500, "startColumn": 4, - "endLine": 499, + "endLine": 502, "endColumn": 29, "byteLength": 124 } @@ -6649,9 +6649,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 504, + "startLine": 507, "startColumn": 25, - "endLine": 504, + "endLine": 507, "endColumn": 41, "byteLength": 16 } @@ -6672,9 +6672,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 492, + "startLine": 495, "startColumn": 12, - "endLine": 492, + "endLine": 495, "endColumn": 28, "byteLength": 16 } @@ -6695,9 +6695,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 506, + "startLine": 509, "startColumn": 12, - "endLine": 506, + "endLine": 509, "endColumn": 13, "byteLength": 1 } @@ -6718,9 +6718,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 506, + "startLine": 509, "startColumn": 12, - "endLine": 506, + "endLine": 509, "endColumn": 13, "byteLength": 1 } @@ -6744,9 +6744,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 492, + "startLine": 495, "startColumn": 12, - "endLine": 492, + "endLine": 495, "endColumn": 28, "byteLength": 16 } @@ -6769,9 +6769,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 493, + "startLine": 496, "startColumn": 12, - "endLine": 493, + "endLine": 496, "endColumn": 19, "byteLength": 7 } @@ -6794,9 +6794,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 491, "startColumn": 12, - "endLine": 488, + "endLine": 491, "endColumn": 19, "byteLength": 7 } @@ -6819,9 +6819,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 502, + "startLine": 505, "startColumn": 12, - "endLine": 502, + "endLine": 505, "endColumn": 19, "byteLength": 7 } @@ -6844,9 +6844,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 487, + "startLine": 490, "startColumn": 14, - "endLine": 487, + "endLine": 490, "endColumn": 21, "byteLength": 7 } @@ -6869,9 +6869,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 506, + "startLine": 509, "startColumn": 12, - "endLine": 506, + "endLine": 509, "endColumn": 13, "byteLength": 1 } @@ -6892,9 +6892,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 135, + "startLine": 138, "startColumn": 14, - "endLine": 135, + "endLine": 138, "endColumn": 21, "byteLength": 7 } @@ -6915,9 +6915,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 131, + "startLine": 134, "startColumn": 29, - "endLine": 131, + "endLine": 134, "endColumn": 53, "byteLength": 24 } @@ -6938,9 +6938,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 133, + "startLine": 136, "startColumn": 28, - "endLine": 133, + "endLine": 136, "endColumn": 64, "byteLength": 36 } @@ -6961,9 +6961,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 135, + "startLine": 138, "startColumn": 14, - "endLine": 135, + "endLine": 138, "endColumn": 21, "byteLength": 7 } @@ -6986,9 +6986,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 132, + "startLine": 135, "startColumn": 12, - "endLine": 132, + "endLine": 135, "endColumn": 19, "byteLength": 7 } @@ -7009,9 +7009,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 218, + "startLine": 221, "startColumn": 12, - "endLine": 218, + "endLine": 221, "endColumn": 13, "byteLength": 1 } @@ -7032,9 +7032,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 212, + "startLine": 215, "startColumn": 29, - "endLine": 212, + "endLine": 215, "endColumn": 49, "byteLength": 20 } @@ -7055,9 +7055,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 213, + "startLine": 216, "startColumn": 34, - "endLine": 213, + "endLine": 216, "endColumn": 59, "byteLength": 25 } @@ -7078,9 +7078,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 216, + "startLine": 219, "startColumn": 4, - "endLine": 216, + "endLine": 219, "endColumn": 60, "byteLength": 56 } @@ -7101,9 +7101,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 218, + "startLine": 221, "startColumn": 12, - "endLine": 218, + "endLine": 221, "endColumn": 13, "byteLength": 1 } @@ -7126,9 +7126,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 214, + "startLine": 217, "startColumn": 12, - "endLine": 214, + "endLine": 217, "endColumn": 19, "byteLength": 7 } @@ -7149,9 +7149,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 195, + "startLine": 198, "startColumn": 12, - "endLine": 195, + "endLine": 198, "endColumn": 13, "byteLength": 1 } @@ -7172,9 +7172,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 195, + "startLine": 198, "startColumn": 12, - "endLine": 195, + "endLine": 198, "endColumn": 13, "byteLength": 1 } @@ -7195,9 +7195,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 195, + "startLine": 198, "startColumn": 12, - "endLine": 195, + "endLine": 198, "endColumn": 13, "byteLength": 1 } @@ -7218,9 +7218,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 195, + "startLine": 198, "startColumn": 12, - "endLine": 195, + "endLine": 198, "endColumn": 13, "byteLength": 1 } @@ -7241,9 +7241,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 181, + "startLine": 184, "startColumn": 29, - "endLine": 181, + "endLine": 184, "endColumn": 49, "byteLength": 20 } @@ -7264,9 +7264,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 184, + "startLine": 187, "startColumn": 24, - "endLine": 184, + "endLine": 187, "endColumn": 35, "byteLength": 11 } @@ -7287,9 +7287,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 189, + "startLine": 192, "startColumn": 28, - "endLine": 189, + "endLine": 192, "endColumn": 40, "byteLength": 12 } @@ -7310,9 +7310,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 185, + "startLine": 188, "startColumn": 25, - "endLine": 185, + "endLine": 188, "endColumn": 38, "byteLength": 13 } @@ -7333,9 +7333,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 186, + "startLine": 189, "startColumn": 30, - "endLine": 186, + "endLine": 189, "endColumn": 66, "byteLength": 36 } @@ -7356,9 +7356,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 187, + "startLine": 190, "startColumn": 33, - "endLine": 187, + "endLine": 190, "endColumn": 59, "byteLength": 26 } @@ -7379,9 +7379,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 190, + "startLine": 193, "startColumn": 25, - "endLine": 190, + "endLine": 193, "endColumn": 41, "byteLength": 16 } @@ -7402,9 +7402,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 193, + "startLine": 196, "startColumn": 4, - "endLine": 193, + "endLine": 196, "endColumn": 60, "byteLength": 56 } @@ -7425,9 +7425,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 195, + "startLine": 198, "startColumn": 12, - "endLine": 195, + "endLine": 198, "endColumn": 13, "byteLength": 1 } @@ -7450,9 +7450,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 182, + "startLine": 185, "startColumn": 12, - "endLine": 182, + "endLine": 185, "endColumn": 19, "byteLength": 7 } @@ -7473,9 +7473,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 334, + "startLine": 337, "startColumn": 12, - "endLine": 334, + "endLine": 337, "endColumn": 13, "byteLength": 1 } @@ -7496,9 +7496,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 329, + "startLine": 332, "startColumn": 35, - "endLine": 329, + "endLine": 332, "endColumn": 76, "byteLength": 41 } @@ -7519,9 +7519,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 330, + "startLine": 333, "startColumn": 33, - "endLine": 330, + "endLine": 333, "endColumn": 57, "byteLength": 24 } @@ -7542,9 +7542,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 331, + "startLine": 334, "startColumn": 12, - "endLine": 331, + "endLine": 334, "endColumn": 20, "byteLength": 8 } @@ -7567,9 +7567,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 331, + "startLine": 334, "startColumn": 12, - "endLine": 331, + "endLine": 334, "endColumn": 20, "byteLength": 8 } @@ -7592,9 +7592,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 332, + "startLine": 335, "startColumn": 12, - "endLine": 332, + "endLine": 335, "endColumn": 19, "byteLength": 7 } @@ -7615,9 +7615,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 523, + "startLine": 526, "startColumn": 12, - "endLine": 523, + "endLine": 526, "endColumn": 13, "byteLength": 1 } @@ -7638,9 +7638,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 519, + "startLine": 522, "startColumn": 33, - "endLine": 519, + "endLine": 522, "endColumn": 60, "byteLength": 27 } @@ -7661,9 +7661,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 520, + "startLine": 523, "startColumn": 35, - "endLine": 520, + "endLine": 523, "endColumn": 51, "byteLength": 16 } @@ -7684,9 +7684,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 521, + "startLine": 524, "startColumn": 33, - "endLine": 521, + "endLine": 524, "endColumn": 59, "byteLength": 26 } @@ -7707,9 +7707,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 523, + "startLine": 526, "startColumn": 12, - "endLine": 523, + "endLine": 526, "endColumn": 13, "byteLength": 1 } @@ -7732,9 +7732,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 518, + "startLine": 521, "startColumn": 12, - "endLine": 518, + "endLine": 521, "endColumn": 19, "byteLength": 7 } @@ -7755,9 +7755,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 210, + "startLine": 213, "startColumn": 14, - "endLine": 210, + "endLine": 213, "endColumn": 20, "byteLength": 6 } @@ -7778,9 +7778,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 204, + "startLine": 207, "startColumn": 29, - "endLine": 204, + "endLine": 207, "endColumn": 49, "byteLength": 20 } @@ -7801,9 +7801,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 205, + "startLine": 208, "startColumn": 34, - "endLine": 205, + "endLine": 208, "endColumn": 59, "byteLength": 25 } @@ -7824,9 +7824,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 208, + "startLine": 211, "startColumn": 28, - "endLine": 208, + "endLine": 211, "endColumn": 53, "byteLength": 25 } @@ -7847,9 +7847,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 206, + "startLine": 209, "startColumn": 12, - "endLine": 206, + "endLine": 209, "endColumn": 19, "byteLength": 7 } @@ -7872,9 +7872,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 206, + "startLine": 209, "startColumn": 12, - "endLine": 206, + "endLine": 209, "endColumn": 19, "byteLength": 7 } @@ -7897,9 +7897,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 207, + "startLine": 210, "startColumn": 12, - "endLine": 207, + "endLine": 210, "endColumn": 19, "byteLength": 7 } @@ -7920,9 +7920,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 229, + "startLine": 232, "startColumn": 12, - "endLine": 229, + "endLine": 232, "endColumn": 13, "byteLength": 1 } @@ -7943,9 +7943,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 220, + "startLine": 223, "startColumn": 36, - "endLine": 220, + "endLine": 223, "endColumn": 63, "byteLength": 27 } @@ -7966,9 +7966,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 221, + "startLine": 224, "startColumn": 34, - "endLine": 221, + "endLine": 224, "endColumn": 59, "byteLength": 25 } @@ -7989,9 +7989,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 225, + "startLine": 228, "startColumn": 4, - "endLine": 227, + "endLine": 230, "endColumn": 59, "byteLength": 141 } @@ -8012,9 +8012,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 229, + "startLine": 232, "startColumn": 12, - "endLine": 229, + "endLine": 232, "endColumn": 13, "byteLength": 1 } @@ -8037,9 +8037,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 222, + "startLine": 225, "startColumn": 12, - "endLine": 222, + "endLine": 225, "endColumn": 19, "byteLength": 7 } @@ -8060,9 +8060,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -8083,9 +8083,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -8106,9 +8106,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -8129,9 +8129,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 245, + "startLine": 248, "startColumn": 31, - "endLine": 245, + "endLine": 248, "endColumn": 55, "byteLength": 24 } @@ -8152,9 +8152,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 258, + "startLine": 261, "startColumn": 6, - "endLine": 260, + "endLine": 263, "endColumn": 70, "byteLength": 120 } @@ -8175,9 +8175,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 268, + "startLine": 271, "startColumn": 29, - "endLine": 268, + "endLine": 271, "endColumn": 53, "byteLength": 24 } @@ -8198,9 +8198,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 256, + "startLine": 259, "startColumn": 24, - "endLine": 256, + "endLine": 259, "endColumn": 34, "byteLength": 10 } @@ -8221,9 +8221,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 267, + "startLine": 270, "startColumn": 20, - "endLine": 267, + "endLine": 270, "endColumn": 30, "byteLength": 10 } @@ -8244,9 +8244,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 264, + "startLine": 267, "startColumn": 27, - "endLine": 264, + "endLine": 267, "endColumn": 72, "byteLength": 45 } @@ -8267,9 +8267,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 265, + "startLine": 268, "startColumn": 24, - "endLine": 265, + "endLine": 268, "endColumn": 57, "byteLength": 33 } @@ -8290,9 +8290,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 277, + "startLine": 280, "startColumn": 27, - "endLine": 278, + "endLine": 281, "endColumn": 72, "byteLength": 92 } @@ -8313,9 +8313,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 279, + "startLine": 282, "startColumn": 24, - "endLine": 279, + "endLine": 282, "endColumn": 77, "byteLength": 53 } @@ -8336,9 +8336,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 246, + "startLine": 249, "startColumn": 10, - "endLine": 246, + "endLine": 249, "endColumn": 16, "byteLength": 6 } @@ -8359,9 +8359,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 261, + "startLine": 264, "startColumn": 12, - "endLine": 261, + "endLine": 264, "endColumn": 27, "byteLength": 15 } @@ -8382,9 +8382,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 269, + "startLine": 272, "startColumn": 12, - "endLine": 269, + "endLine": 272, "endColumn": 32, "byteLength": 20 } @@ -8407,9 +8407,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 246, + "startLine": 249, "startColumn": 10, - "endLine": 246, + "endLine": 249, "endColumn": 16, "byteLength": 6 } @@ -8433,9 +8433,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 248, + "startLine": 251, "startColumn": 10, - "endLine": 248, + "endLine": 251, "endColumn": 30, "byteLength": 20 } @@ -8458,9 +8458,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 250, + "startLine": 253, "startColumn": 10, - "endLine": 250, + "endLine": 253, "endColumn": 17, "byteLength": 7 } @@ -8483,9 +8483,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 252, + "startLine": 255, "startColumn": 10, - "endLine": 252, + "endLine": 255, "endColumn": 25, "byteLength": 15 } @@ -8508,9 +8508,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 261, + "startLine": 264, "startColumn": 12, - "endLine": 261, + "endLine": 264, "endColumn": 27, "byteLength": 15 } @@ -8533,9 +8533,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 262, + "startLine": 265, "startColumn": 12, - "endLine": 262, + "endLine": 265, "endColumn": 18, "byteLength": 6 } @@ -8558,9 +8558,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 263, + "startLine": 266, "startColumn": 12, - "endLine": 263, + "endLine": 266, "endColumn": 19, "byteLength": 7 } @@ -8584,9 +8584,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 269, + "startLine": 272, "startColumn": 12, - "endLine": 269, + "endLine": 272, "endColumn": 32, "byteLength": 20 } @@ -8609,9 +8609,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 272, + "startLine": 275, "startColumn": 12, - "endLine": 272, + "endLine": 275, "endColumn": 27, "byteLength": 15 } @@ -8634,9 +8634,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 275, + "startLine": 278, "startColumn": 12, - "endLine": 275, + "endLine": 278, "endColumn": 19, "byteLength": 7 } @@ -8657,9 +8657,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -8680,9 +8680,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 286, "startColumn": 12, - "endLine": 283, + "endLine": 286, "endColumn": 13, "byteLength": 1 } @@ -8703,9 +8703,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -8726,9 +8726,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -8749,9 +8749,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -8772,9 +8772,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 286, + "startLine": 289, "startColumn": 31, - "endLine": 286, + "endLine": 289, "endColumn": 55, "byteLength": 24 } @@ -8795,9 +8795,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 287, + "startLine": 290, "startColumn": 26, - "endLine": 287, + "endLine": 290, "endColumn": 41, "byteLength": 15 } @@ -8818,9 +8818,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 300, + "startLine": 303, "startColumn": 6, - "endLine": 302, + "endLine": 305, "endColumn": 70, "byteLength": 120 } @@ -8841,9 +8841,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 311, + "startLine": 314, "startColumn": 29, - "endLine": 311, + "endLine": 314, "endColumn": 46, "byteLength": 17 } @@ -8864,9 +8864,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 312, + "startLine": 315, "startColumn": 37, - "endLine": 312, + "endLine": 315, "endColumn": 58, "byteLength": 21 } @@ -8887,9 +8887,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 298, + "startLine": 301, "startColumn": 24, - "endLine": 298, + "endLine": 301, "endColumn": 34, "byteLength": 10 } @@ -8910,9 +8910,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 310, + "startLine": 313, "startColumn": 20, - "endLine": 310, + "endLine": 313, "endColumn": 30, "byteLength": 10 } @@ -8933,9 +8933,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 306, + "startLine": 309, "startColumn": 27, - "endLine": 306, + "endLine": 309, "endColumn": 72, "byteLength": 45 } @@ -8956,9 +8956,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 307, + "startLine": 310, "startColumn": 28, - "endLine": 307, + "endLine": 310, "endColumn": 49, "byteLength": 21 } @@ -8979,9 +8979,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 308, + "startLine": 311, "startColumn": 28, - "endLine": 308, + "endLine": 311, "endColumn": 54, "byteLength": 26 } @@ -9002,9 +9002,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 321, + "startLine": 324, "startColumn": 27, - "endLine": 322, + "endLine": 325, "endColumn": 65, "byteLength": 85 } @@ -9025,9 +9025,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 323, + "startLine": 326, "startColumn": 28, - "endLine": 323, + "endLine": 326, "endColumn": 67, "byteLength": 39 } @@ -9048,9 +9048,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 288, + "startLine": 291, "startColumn": 10, - "endLine": 288, + "endLine": 291, "endColumn": 16, "byteLength": 6 } @@ -9071,9 +9071,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 303, + "startLine": 306, "startColumn": 12, - "endLine": 303, + "endLine": 306, "endColumn": 20, "byteLength": 8 } @@ -9094,9 +9094,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 313, + "startLine": 316, "startColumn": 12, - "endLine": 313, + "endLine": 316, "endColumn": 27, "byteLength": 15 } @@ -9119,9 +9119,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 288, + "startLine": 291, "startColumn": 10, - "endLine": 288, + "endLine": 291, "endColumn": 16, "byteLength": 6 } @@ -9145,9 +9145,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 290, + "startLine": 293, "startColumn": 10, - "endLine": 290, + "endLine": 293, "endColumn": 25, "byteLength": 15 } @@ -9170,9 +9170,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 292, + "startLine": 295, "startColumn": 10, - "endLine": 292, + "endLine": 295, "endColumn": 17, "byteLength": 7 } @@ -9195,9 +9195,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 294, + "startLine": 297, "startColumn": 10, - "endLine": 294, + "endLine": 297, "endColumn": 18, "byteLength": 8 } @@ -9220,9 +9220,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 303, + "startLine": 306, "startColumn": 12, - "endLine": 303, + "endLine": 306, "endColumn": 20, "byteLength": 8 } @@ -9245,9 +9245,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 304, + "startLine": 307, "startColumn": 12, - "endLine": 304, + "endLine": 307, "endColumn": 18, "byteLength": 6 } @@ -9270,9 +9270,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 305, + "startLine": 308, "startColumn": 12, - "endLine": 305, + "endLine": 308, "endColumn": 19, "byteLength": 7 } @@ -9296,9 +9296,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 313, + "startLine": 316, "startColumn": 12, - "endLine": 313, + "endLine": 316, "endColumn": 27, "byteLength": 15 } @@ -9321,9 +9321,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 316, + "startLine": 319, "startColumn": 12, - "endLine": 316, + "endLine": 319, "endColumn": 20, "byteLength": 8 } @@ -9346,9 +9346,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 319, + "startLine": 322, "startColumn": 12, - "endLine": 319, + "endLine": 322, "endColumn": 19, "byteLength": 7 } @@ -9369,9 +9369,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -9392,9 +9392,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 330, "startColumn": 12, - "endLine": 327, + "endLine": 330, "endColumn": 13, "byteLength": 1 } @@ -9415,9 +9415,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 463, + "startLine": 466, "startColumn": 14, - "endLine": 463, + "endLine": 466, "endColumn": 21, "byteLength": 7 } @@ -9438,9 +9438,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 458, + "startLine": 461, "startColumn": 25, - "endLine": 458, + "endLine": 461, "endColumn": 48, "byteLength": 23 } @@ -9461,9 +9461,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 459, + "startLine": 462, "startColumn": 31, - "endLine": 459, + "endLine": 462, "endColumn": 53, "byteLength": 22 } @@ -9484,9 +9484,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 460, + "startLine": 463, "startColumn": 12, - "endLine": 460, + "endLine": 463, "endColumn": 26, "byteLength": 14 } @@ -9510,9 +9510,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 460, + "startLine": 463, "startColumn": 12, - "endLine": 460, + "endLine": 463, "endColumn": 26, "byteLength": 14 } @@ -9535,9 +9535,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 461, + "startLine": 464, "startColumn": 12, - "endLine": 461, + "endLine": 464, "endColumn": 19, "byteLength": 7 } diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml index 4555837a8811f08bce4a738427e8625889174f41..e68db07905a30b2b03d50fe0f8e10dd9826c54f3 100644 --- a/src/plugins/metrics/metrics_base.ml +++ b/src/plugins/metrics/metrics_base.ml @@ -372,7 +372,6 @@ let consider_function ~libc vinfo = ) && (libc || not (Cil.is_in_libc vinfo.vattr)) let consider_variable ~libc vinfo = - not (Cil.hasAttribute "FRAMA_C_MODEL" vinfo.vattr) && (libc || not (Cil.is_in_libc vinfo.vattr)) let float_to_string f = diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli index a93c078c04ecda52d352be849d92e39e9da8174a..79c68f1f025c5007be032b5e16834871a3ec04ad 100644 --- a/src/plugins/metrics/metrics_base.mli +++ b/src/plugins/metrics/metrics_base.mli @@ -157,8 +157,7 @@ val get_file_type: Filepath.Normalized.t -> output_type;; val consider_function: libc:bool -> Cil_types.varinfo -> bool (** [consider_variable vinfo] returns false if the varinfo is not an object - variable we are interested in. Currently excluded variables are those - declared with attribute [__FRAMA_C_MODEL__]. + variable we are interested in. If [libc] is false, do not consider variables from the Frama-C libc. *) val consider_variable: libc:bool -> Cil_types.varinfo -> bool diff --git a/src/plugins/nonterm/tests/nonterm/oracle/builtin_with_body.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/builtin_with_body.res.oracle index 9674c549de3b153c7a69c655bbb5c9af2a4c03ab..e46e4414e778f62fa979a50e1d129c032325373e 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/builtin_with_body.res.oracle +++ b/src/plugins/nonterm/tests/nonterm/oracle/builtin_with_body.res.oracle @@ -12,7 +12,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/nonterm/builtin_with_body.c:13: function memcpy: precondition 'separation' got status valid. -[eva] FRAMAC_SHARE/libc/string.h:98: +[eva] FRAMAC_SHARE/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] Recording results for main [eva] done for function main diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n6.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n6.res.oracle index 09231ee296bba908dea37b0b2359a6a5ce24e2bc..fd3768d1bf381fc61235e5c887345f9a1fdb2207 100644 --- a/src/plugins/nonterm/tests/nonterm/oracle/n6.res.oracle +++ b/src/plugins/nonterm/tests/nonterm/oracle/n6.res.oracle @@ -11,7 +11,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/nonterm/n6.c:9: function memcpy: precondition 'separation' got status valid. -[eva] FRAMAC_SHARE/libc/string.h:98: +[eva] FRAMAC_SHARE/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] Recording results for main [eva] done for function main diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle index e572952cd2d636ef01e856ffca163927fbc024c3..296acd22116d6ed8a14eefa94d1d182981d57523 100644 --- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle +++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle @@ -21,7 +21,7 @@ [eva] Analyzing a complete application starting at main [eva] Computing initial state [eva] Initial state computed -[eva] FRAMAC_SHARE/libc/string.h:118: +[eva] FRAMAC_SHARE/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] using specification for function snprintf_va_1 [eva] tests/known/snprintf.c:12: diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle index 4ec695d3836684961abb135cd11f669f2650370a..6065e895512cd5689727b843c85877c8f0a40a69 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle @@ -153,7 +153,7 @@ Prove: included(a_2, 1, a, n). ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 96) in 'memcpy': +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 99) in 'memcpy': Effect at line 38 Prove: true. @@ -702,41 +702,41 @@ Prove: included(a_3, 1, a, n). ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove': +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 109) in 'memmove': Prove: true. ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (1/7): +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 109) in 'memmove' (1/7): Prove: true. ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (2/7): +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 109) in 'memmove' (2/7): Effect at line 74 Prove: true. ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (3/7): +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 109) in 'memmove' (3/7): Call Result at line 77 Prove: true. ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (4/7): +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 109) in 'memmove' (4/7): Effect at line 85 Prove: true. ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (5/7): +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 109) in 'memmove' (5/7): Effect at line 97 Prove: true. ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (6/7): +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 109) in 'memmove' (6/7): Effect at line 99 Let a = shift_sint8(d, 0). Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n). @@ -777,7 +777,7 @@ Prove: 0 < n. ------------------------------------------------------------ -Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 106) in 'memmove' (7/7): +Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 109) in 'memmove' (7/7): Effect at line 101 Prove: true. diff --git a/tests/builtins/oracle/alloc_weak.res.oracle b/tests/builtins/oracle/alloc_weak.res.oracle index 7705984008d4c08d656c18cda171bb1d1adb99e5..1ab877c03e75945ef4f6690ae0f8aea4546dcbf8 100644 --- a/tests/builtins/oracle/alloc_weak.res.oracle +++ b/tests/builtins/oracle/alloc_weak.res.oracle @@ -22,7 +22,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/builtins/alloc_weak.c:14: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] Recording results for copy [eva] Done for function copy diff --git a/tests/builtins/oracle/fam.res.oracle b/tests/builtins/oracle/fam.res.oracle index e00111b34654556ce0a087c6253a6439733458b7..e13a0a6339747b9fde899dd12f91146c8346de8f 100644 --- a/tests/builtins/oracle/fam.res.oracle +++ b/tests/builtins/oracle/fam.res.oracle @@ -12,7 +12,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/builtins/fam.c:16: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] Recording results for main [eva] done for function main diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle index f93b938207e84054d6ecd4daf5c6a9740816884a..eff74c8d72b3a2557d72f75731a08bea8fb12ef6 100644 --- a/tests/builtins/oracle/imprecise.res.oracle +++ b/tests/builtins/oracle/imprecise.res.oracle @@ -105,7 +105,7 @@ [eva] tests/builtins/imprecise.c:51: Call to builtin memset [eva:alarm] tests/builtins/imprecise.c:51: Warning: function memset: precondition 'valid_s' got status unknown. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva:alarm] tests/builtins/imprecise.c:53: Warning: out of bounds write. assert \valid(p2); diff --git a/tests/builtins/oracle/malloc_bug_tr.res.oracle b/tests/builtins/oracle/malloc_bug_tr.res.oracle index 7504934bb14c0f471348aa417131a4559817c6b1..b94361f0ca6cf504b5c02a580a66732dc4e0bef8 100644 --- a/tests/builtins/oracle/malloc_bug_tr.res.oracle +++ b/tests/builtins/oracle/malloc_bug_tr.res.oracle @@ -19,7 +19,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/builtins/malloc_bug_tr.c:13: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] tests/builtins/malloc_bug_tr.c:14: Call to builtin memcpy [eva:alarm] tests/builtins/malloc_bug_tr.c:14: Warning: diff --git a/tests/builtins/oracle/memchr.res.oracle b/tests/builtins/oracle/memchr.res.oracle index df4a1d526227438f0e5e72bc778aa514d5533a41..5b0ee21abd93b73e51f1a9c21c4ca5a01f8aa72d 100644 --- a/tests/builtins/oracle/memchr.res.oracle +++ b/tests/builtins/oracle/memchr.res.oracle @@ -152,7 +152,7 @@ [eva] tests/builtins/memchr.c:193: Call to builtin memset [eva] tests/builtins/memchr.c:193: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Recording results for init_array_nondet [eva] Done for function init_array_nondet diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle index 2f999a73305848291580c8f7674418100e8ff5c0..a5f20ab0df7f8edf1309e39f0e0d36f15ca80109 100644 --- a/tests/builtins/oracle/memcpy.res.oracle +++ b/tests/builtins/oracle/memcpy.res.oracle @@ -32,7 +32,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/builtins/memcpy.c:28: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] Recording results for buggy [from] Computing for function buggy @@ -1181,11 +1181,11 @@ Unverifiable but considered Valid. [ Extern ] Post-condition 'result_ptr' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 96) +[ Extern ] Assigns (file share/libc/string.h, line 99) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 96) +[ Extern ] Froms (file share/libc/string.h, line 99) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 97) +[ Extern ] Froms (file share/libc/string.h, line 100) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1198,11 +1198,11 @@ Unverifiable but considered Valid. [ Extern ] Post-condition 'result_ptr' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 106) +[ Extern ] Assigns (file share/libc/string.h, line 109) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 106) +[ Extern ] Froms (file share/libc/string.h, line 109) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 107) +[ Extern ] Froms (file share/libc/string.h, line 110) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1215,11 +1215,11 @@ Unverifiable but considered Valid. [ Extern ] Post-condition 'result_ptr' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 116) +[ Extern ] Assigns (file share/libc/string.h, line 119) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 116) +[ Extern ] Froms (file share/libc/string.h, line 119) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 117) +[ Extern ] Froms (file share/libc/string.h, line 120) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1232,7 +1232,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 126) +[ Extern ] Froms (file share/libc/string.h, line 129) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1245,7 +1245,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 132) +[ Extern ] Froms (file share/libc/string.h, line 135) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1258,7 +1258,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 139) +[ Extern ] Froms (file share/libc/string.h, line 142) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1271,7 +1271,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 146) +[ Extern ] Froms (file share/libc/string.h, line 149) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1282,7 +1282,7 @@ [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 153) +[ Extern ] Froms (file share/libc/string.h, line 156) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1307,7 +1307,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 158) +[ Extern ] Froms (file share/libc/string.h, line 161) Unverifiable but considered Valid. [ Valid ] Behavior 'default' by Frama-C kernel. @@ -1326,7 +1326,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 176) +[ Extern ] Froms (file share/libc/string.h, line 179) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1347,7 +1347,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 182) +[ Extern ] Froms (file share/libc/string.h, line 185) Unverifiable but considered Valid. [ Valid ] Behavior 'default' by Frama-C kernel. @@ -1366,7 +1366,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 199) +[ Extern ] Froms (file share/libc/string.h, line 202) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1377,11 +1377,11 @@ [ Extern ] Post-condition 'result_bounded' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 206) +[ Extern ] Assigns (file share/libc/string.h, line 209) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 206) +[ Extern ] Froms (file share/libc/string.h, line 209) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 207) +[ Extern ] Froms (file share/libc/string.h, line 210) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1394,7 +1394,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 214) +[ Extern ] Froms (file share/libc/string.h, line 217) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1407,7 +1407,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 222) +[ Extern ] Froms (file share/libc/string.h, line 225) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1420,7 +1420,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 233) +[ Extern ] Froms (file share/libc/string.h, line 236) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1437,32 +1437,32 @@ Unverifiable but considered Valid. [ Extern ] Post-condition for 'resume_str' 'ptr_subset' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 246) +[ Extern ] Assigns (file share/libc/string.h, line 249) Unverifiable but considered Valid. -[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 261) +[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 264) Unverifiable but considered Valid. -[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 269) +[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 272) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 246) +[ Extern ] Froms (file share/libc/string.h, line 249) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 248) +[ Extern ] Froms (file share/libc/string.h, line 251) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 250) +[ Extern ] Froms (file share/libc/string.h, line 253) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 252) +[ Extern ] Froms (file share/libc/string.h, line 255) Unverifiable but considered Valid. -[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 261) +[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 264) Unverifiable but considered Valid. -[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 262) +[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 265) Unverifiable but considered Valid. -[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 263) - Unverifiable but considered Valid. -[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 269) +[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 266) Unverifiable but considered Valid. [ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 272) Unverifiable but considered Valid. [ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 275) Unverifiable but considered Valid. +[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 278) + Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. [ Valid ] Behavior 'new_str' @@ -1484,32 +1484,32 @@ Unverifiable but considered Valid. [ Extern ] Post-condition for 'resume_str' 'saveptr_subset' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 288) - Unverifiable but considered Valid. -[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 303) +[ Extern ] Assigns (file share/libc/string.h, line 291) Unverifiable but considered Valid. -[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 313) +[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 306) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 288) +[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 316) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 290) +[ Extern ] Froms (file share/libc/string.h, line 291) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 292) +[ Extern ] Froms (file share/libc/string.h, line 293) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 294) +[ Extern ] Froms (file share/libc/string.h, line 295) Unverifiable but considered Valid. -[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 303) +[ Extern ] Froms (file share/libc/string.h, line 297) Unverifiable but considered Valid. -[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 304) +[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 306) Unverifiable but considered Valid. -[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 305) +[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 307) Unverifiable but considered Valid. -[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 313) +[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 308) Unverifiable but considered Valid. [ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 316) Unverifiable but considered Valid. [ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 319) Unverifiable but considered Valid. +[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 322) + Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. [ Valid ] Behavior 'new_str' @@ -1521,11 +1521,11 @@ --- Properties of Function 'strsep' -------------------------------------------------------------------------------- -[ Extern ] Assigns (file share/libc/string.h, line 331) +[ Extern ] Assigns (file share/libc/string.h, line 334) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 331) +[ Extern ] Froms (file share/libc/string.h, line 334) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 332) +[ Extern ] Froms (file share/libc/string.h, line 335) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1542,7 +1542,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 342) +[ Extern ] Froms (file share/libc/string.h, line 345) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1555,11 +1555,11 @@ Unverifiable but considered Valid. [ Extern ] Post-condition 'result_ptr' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 355) +[ Extern ] Assigns (file share/libc/string.h, line 358) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 355) +[ Extern ] Froms (file share/libc/string.h, line 358) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 356) +[ Extern ] Froms (file share/libc/string.h, line 359) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1576,11 +1576,11 @@ Unverifiable but considered Valid. [ Extern ] Post-condition for 'partial' 'equal_prefix' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 367) +[ Extern ] Assigns (file share/libc/string.h, line 370) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 367) +[ Extern ] Froms (file share/libc/string.h, line 370) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 368) +[ Extern ] Froms (file share/libc/string.h, line 371) Unverifiable but considered Valid. [ Valid ] Behavior 'complete' by Frama-C kernel. @@ -1597,11 +1597,11 @@ Unverifiable but considered Valid. [ Extern ] Post-condition 'bounded_result' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 388) +[ Extern ] Assigns (file share/libc/string.h, line 391) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 388) +[ Extern ] Froms (file share/libc/string.h, line 391) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 389) +[ Extern ] Froms (file share/libc/string.h, line 392) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1614,11 +1614,11 @@ Unverifiable but considered Valid. [ Extern ] Post-condition 'points_to_end' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 400) +[ Extern ] Assigns (file share/libc/string.h, line 403) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 400) +[ Extern ] Froms (file share/libc/string.h, line 403) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 401) +[ Extern ] Froms (file share/libc/string.h, line 404) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1635,12 +1635,12 @@ Unverifiable but considered Valid. [ Extern ] Post-condition 'result_ptr' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 411) - Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 411) +[ Extern ] Assigns (file share/libc/string.h, line 414) Unverifiable but considered Valid. [ Extern ] Froms (file share/libc/string.h, line 414) Unverifiable but considered Valid. +[ Extern ] Froms (file share/libc/string.h, line 417) + Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1654,23 +1654,23 @@ Unverifiable but considered Valid. [ Extern ] Post-condition for 'partial' 'sum_of_bounded_lengths' Unverifiable but considered Valid. -[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 431) +[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 434) Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 425) +[ Extern ] Assigns (file share/libc/string.h, line 428) Unverifiable but considered Valid. -[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 439) +[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 442) Unverifiable but considered Valid. -[ Extern ] Froms for 'complete' (file share/libc/string.h, line 431) +[ Extern ] Froms for 'complete' (file share/libc/string.h, line 434) Unverifiable but considered Valid. -[ Extern ] Froms for 'complete' (file share/libc/string.h, line 433) +[ Extern ] Froms for 'complete' (file share/libc/string.h, line 436) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 425) +[ Extern ] Froms (file share/libc/string.h, line 428) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 426) +[ Extern ] Froms (file share/libc/string.h, line 429) Unverifiable but considered Valid. -[ Extern ] Froms for 'partial' (file share/libc/string.h, line 439) +[ Extern ] Froms for 'partial' (file share/libc/string.h, line 442) Unverifiable but considered Valid. -[ Extern ] Froms for 'partial' (file share/libc/string.h, line 441) +[ Extern ] Froms for 'partial' (file share/libc/string.h, line 444) Unverifiable but considered Valid. [ Valid ] Behavior 'complete' by Frama-C kernel. @@ -1685,11 +1685,11 @@ [ Extern ] Post-condition 'bounded_result' Unverifiable but considered Valid. -[ Extern ] Assigns (file share/libc/string.h, line 451) +[ Extern ] Assigns (file share/libc/string.h, line 454) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 451) +[ Extern ] Froms (file share/libc/string.h, line 454) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 452) +[ Extern ] Froms (file share/libc/string.h, line 455) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1698,11 +1698,11 @@ --- Properties of Function 'strxfrm' -------------------------------------------------------------------------------- -[ Extern ] Assigns (file share/libc/string.h, line 460) +[ Extern ] Assigns (file share/libc/string.h, line 463) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 460) +[ Extern ] Froms (file share/libc/string.h, line 463) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 461) +[ Extern ] Froms (file share/libc/string.h, line 464) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1717,19 +1717,19 @@ Unverifiable but considered Valid. [ Extern ] Post-condition for 'no_allocation' 'result_null' Unverifiable but considered Valid. -[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 473) +[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 476) Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. [ Extern ] Assigns for 'no_allocation' nothing Unverifiable but considered Valid. -[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 473) +[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 476) Unverifiable but considered Valid. -[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 474) +[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 477) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 470) +[ Extern ] Froms (file share/libc/string.h, line 473) Unverifiable but considered Valid. -[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 480) +[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 483) Unverifiable but considered Valid. [ Valid ] Behavior 'allocation' by Frama-C kernel. @@ -1737,7 +1737,7 @@ by Frama-C kernel. [ Valid ] Behavior 'no_allocation' by Frama-C kernel. -[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 469) +[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 472) Unverifiable but considered Valid. [ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing Unverifiable but considered Valid. @@ -1752,19 +1752,19 @@ Unverifiable but considered Valid. [ Extern ] Post-condition for 'no_allocation' 'result_null' Unverifiable but considered Valid. -[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 492) +[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 495) Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. [ Extern ] Assigns for 'no_allocation' nothing Unverifiable but considered Valid. -[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 492) +[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 495) Unverifiable but considered Valid. -[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 493) +[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 496) Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 488) +[ Extern ] Froms (file share/libc/string.h, line 491) Unverifiable but considered Valid. -[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 502) +[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 505) Unverifiable but considered Valid. [ Valid ] Behavior 'allocation' by Frama-C kernel. @@ -1772,7 +1772,7 @@ by Frama-C kernel. [ Valid ] Behavior 'no_allocation' by Frama-C kernel. -[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 487) +[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 490) Unverifiable but considered Valid. [ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing Unverifiable but considered Valid. @@ -1789,7 +1789,7 @@ Unverifiable but considered Valid. [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file share/libc/string.h, line 518) +[ Extern ] Froms (file share/libc/string.h, line 521) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. diff --git a/tests/builtins/oracle/memcpy2.res.oracle b/tests/builtins/oracle/memcpy2.res.oracle index 912286440a4435cca2a1146eb60e1d541b313ffe..6aa9466eb01a6c5efe9627043f52a9ed404da247 100644 --- a/tests/builtins/oracle/memcpy2.res.oracle +++ b/tests/builtins/oracle/memcpy2.res.oracle @@ -17,7 +17,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/builtins/memcpy2.c:10: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] tests/builtins/memcpy2.c:12: Frama_C_dump_each: diff --git a/tests/builtins/oracle/memcpy_invalid.res.oracle b/tests/builtins/oracle/memcpy_invalid.res.oracle index 6863c287b84c64f471434b796daa2e840900780a..a9e3c0bbef926760b568b30d259542764471ed65 100644 --- a/tests/builtins/oracle/memcpy_invalid.res.oracle +++ b/tests/builtins/oracle/memcpy_invalid.res.oracle @@ -17,7 +17,7 @@ function memcpy: precondition 'valid_src' got status unknown. [eva] tests/builtins/memcpy_invalid.c:17: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] Recording results for test [from] Computing for function test diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle index e2c146788658bd30ae5e489e1134b1800830daf9..f0aa5e3505dd50604e0f7b10a38d109ac9418922 100644 --- a/tests/builtins/oracle/memset.res.oracle +++ b/tests/builtins/oracle/memset.res.oracle @@ -23,7 +23,7 @@ [eva] tests/builtins/memset.c:33: Call to builtin memset [eva] tests/builtins/memset.c:33: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva:alarm] tests/builtins/memset.c:34: Warning: pointer downcast. assert (unsigned int)((int *)t2) ≤ 2147483647; diff --git a/tests/builtins/oracle/memset_malloc_0.res.oracle b/tests/builtins/oracle/memset_malloc_0.res.oracle index 195b288e51d739105adbc98d9c82f2fd358f4c24..02e895219affaa1e5b95535f9879ce64a699fbbe 100644 --- a/tests/builtins/oracle/memset_malloc_0.res.oracle +++ b/tests/builtins/oracle/memset_malloc_0.res.oracle @@ -9,7 +9,7 @@ [eva] tests/builtins/memset_malloc_0.c:18: Call to builtin memset [eva] tests/builtins/memset_malloc_0.c:18: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Recording results for main [eva] done for function main diff --git a/tests/builtins/oracle/precise_memset.res.oracle b/tests/builtins/oracle/precise_memset.res.oracle index 686392ad5adb2f89c6bd5f13aa2dc44d6fca73cb..4ec1113f41e38ab0f6980768e07ff29ae040700b 100644 --- a/tests/builtins/oracle/precise_memset.res.oracle +++ b/tests/builtins/oracle/precise_memset.res.oracle @@ -22,7 +22,7 @@ [eva] tests/builtins/precise_memset.c:72: Call to builtin memset [eva] tests/builtins/precise_memset.c:72: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] tests/builtins/precise_memset.c:73: Call to builtin memset [eva] tests/builtins/precise_memset.c:73: diff --git a/tests/builtins/oracle/strchr.res.oracle b/tests/builtins/oracle/strchr.res.oracle index 770361f547028d044dea20eeb4bd77a6108ac9bb..476e5595632608dff381b6c0c81fe735880fb468 100644 --- a/tests/builtins/oracle/strchr.res.oracle +++ b/tests/builtins/oracle/strchr.res.oracle @@ -23,7 +23,7 @@ [eva] tests/builtins/strchr.c:88: Call to builtin strchr [eva] tests/builtins/strchr.c:88: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:165: +[eva] share/libc/string.h:168: cannot evaluate ACSL term, unsupported logic var p [eva] tests/builtins/strchr.c:88: Frama_C_show_each_mystrchr: {3} [eva] tests/builtins/strchr.c:89: assertion got status valid. @@ -93,7 +93,7 @@ [eva] tests/builtins/strchr.c:189: Call to builtin memset [eva] tests/builtins/strchr.c:189: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Recording results for init_array_nondet [eva] Done for function init_array_nondet diff --git a/tests/builtins/oracle/strlen.res.oracle b/tests/builtins/oracle/strlen.res.oracle index dcc09a3de5d1cf947b9d8f050733884324be3c76..f6e48b036c4d2a58426db0049c43f911e4c5c36d 100644 --- a/tests/builtins/oracle/strlen.res.oracle +++ b/tests/builtins/oracle/strlen.res.oracle @@ -94,7 +94,7 @@ [eva] tests/builtins/strlen.c:161: Call to builtin memset [eva] tests/builtins/strlen.c:161: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Recording results for init_array_nondet [eva] Done for function init_array_nondet diff --git a/tests/builtins/oracle/strnlen2.res.oracle b/tests/builtins/oracle/strnlen2.res.oracle index 392940b6cb6e3312cb5941f61892dfa13cb007c0..5bc8dab83db2e2fb0947d85d5a50139266d40473 100644 --- a/tests/builtins/oracle/strnlen2.res.oracle +++ b/tests/builtins/oracle/strnlen2.res.oracle @@ -94,7 +94,7 @@ [eva] tests/builtins/strnlen2.c:138: Call to builtin memset [eva] tests/builtins/strnlen2.c:138: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Recording results for init_array_nondet [eva] Done for function init_array_nondet diff --git a/tests/builtins/oracle/wcslen.res.oracle b/tests/builtins/oracle/wcslen.res.oracle index 00a752d3a13c96865b01c5993f4439c578fb0b19..b6224f18bec7a5ac01cd50395e061cbb1a99029f 100644 --- a/tests/builtins/oracle/wcslen.res.oracle +++ b/tests/builtins/oracle/wcslen.res.oracle @@ -94,7 +94,7 @@ [eva] tests/builtins/wcslen.c:161: Call to builtin memset [eva] tests/builtins/wcslen.c:161: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Recording results for init_array_nondet [eva] Done for function init_array_nondet diff --git a/tests/builtins/oracle/write-const.res.oracle b/tests/builtins/oracle/write-const.res.oracle index 8b39ca3d183021f676f5240a91aaf3c582e4e66e..9423005733a661ade90bc56a8a55bb836b7af397 100644 --- a/tests/builtins/oracle/write-const.res.oracle +++ b/tests/builtins/oracle/write-const.res.oracle @@ -15,7 +15,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/builtins/write-const.c:18: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] tests/builtins/write-const.c:19: Frama_C_dump_each: @@ -42,7 +42,7 @@ [eva] tests/builtins/write-const.c:25: Call to builtin memset [eva:alarm] tests/builtins/write-const.c:25: Warning: function memset: precondition 'valid_s' got status unknown. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] tests/builtins/write-const.c:26: Frama_C_dump_each: diff --git a/tests/libc/netinet_in_h.c b/tests/libc/netinet_in_h.c index c82743a5d72dab9470ddac9f94f9008e6a8214e5..a2f20a58370cba620f337639158b18dec687bc28 100644 --- a/tests/libc/netinet_in_h.c +++ b/tests/libc/netinet_in_h.c @@ -4,4 +4,6 @@ int main() { struct in_addr addr = {0}; printf("%s", inet_ntoa(addr)); + struct sockaddr_in6 sockaddr6_any = {0, 0, 0, IN6ADDR_ANY_INIT, 0}; + struct sockaddr_in6 sockaddr6_loopback = {0, 0, 0, IN6ADDR_LOOPBACK_INIT, 0}; } diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle index 4bd29442f2a0010f81c798585313bc45972f55a5..7955573b0c8101d35d2a7b324dcc54e1a9266e80 100644 --- a/tests/libc/oracle/fc_libc.0.res.oracle +++ b/tests/libc/oracle/fc_libc.0.res.oracle @@ -37,7 +37,7 @@ posix_memalign (0 call); putenv (0 call); realpath (0 call); res_search (1 call); setenv (0 call); setlocale (0 call); strcasecmp (0 call); strcat (0 call); strchr (3 calls); strcmp (0 call); - strcpy (0 call); strdup (0 call); strerror (0 call); strlen (6 calls); + strcpy (1 call); strdup (0 call); strerror (0 call); strlen (6 calls); strncat (0 call); strncmp (0 call); strncpy (2 calls); strndup (0 call); strnlen (0 call); strrchr (0 call); strsignal (0 call); strstr (0 call); tolower (0 call); toupper (0 call); unsetenv (0 call); wcscat (0 call); @@ -119,7 +119,7 @@ log10f (0 call); log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call); lseek (0 call); lstat (0 call); makedev (0 call); - malloc (9 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call); + malloc (10 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call); mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call); @@ -174,13 +174,14 @@ ======================================= __builtin_abort (1 call); - 'Extern' global variables (20) + 'Extern' global variables (21) ============================== __fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name; __fc_getpwuid_pw_passwd; __fc_getpwuid_pw_shell; __fc_heap_status; __fc_hostname; __fc_locale; __fc_locale_names; __fc_mblen_state; - __fc_mbtowc_state; __fc_random_counter; __fc_stack_status; __fc_tz; - __fc_wctomb_state; optarg; opterr; optopt; tzname + __fc_mbtowc_state; __fc_random_counter; __fc_socket_counter; + __fc_stack_status; __fc_tz; __fc_wctomb_state; optarg; opterr; optopt; + tzname Potential entry points (1) ========================== @@ -188,18 +189,18 @@ Global metrics ============== - Sloc = 1138 - Decision point = 214 - Global variables = 85 - If = 199 + Sloc = 1145 + Decision point = 215 + Global variables = 86 + If = 200 Loop = 43 - Goto = 98 - Assignment = 465 + Goto = 99 + Assignment = 466 Exit point = 84 Function = 500 - Function call = 96 - Pointer dereferencing = 159 - Cyclomatic complexity = 298 + Function call = 98 + Pointer dereferencing = 161 + Cyclomatic complexity = 299 /* Generated by Frama-C */ #include "__fc_builtin.c" #include "__fc_builtin.h" diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index ad9b0757d8924efaa04327babc5aee2af4aa2c0b..7ede7566e8cec61541875f914b64a6038a2c83e4 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -2740,7 +2740,7 @@ struct lconv __C_locale = .int_p_sign_posn = (char)127, .int_n_sign_posn = (char)127}; struct lconv *__frama_c_locale = & __C_locale; -char *__frama_c_locale_names[512] = {(char *)"C"}; +char const *__frama_c_locale_names[512] = {"C"}; /*@ requires locale_null_or_valid_string: locale ≡ \null ∨ valid_read_string(locale); @@ -2757,7 +2757,7 @@ char *setlocale(int category, char const *locale) char *__retres; if ((int)*locale == 'C') { __frama_c_locale = & __C_locale; - __retres = __frama_c_locale_names[0]; + __retres = (char *)__frama_c_locale_names[0]; goto return_label; } __retres = (char *)0; @@ -3580,8 +3580,7 @@ extern int killpg(pid_t pgrp, int sig); extern ssize_t readv(int fd, struct iovec const *iov, int iovcnt); /*@ ghost struct __fc_sockfds_type __fc_sockfds[1024]; */ -/*@ ghost extern int __fc_socket_counter __attribute__((__FRAMA_C_MODEL__)); -*/ +/*@ ghost extern int __fc_socket_counter; */ /*@ ghost int volatile __fc_open_sock_fds; */ /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; @@ -3885,24 +3884,10 @@ extern int socket(int domain, int type, int protocol); */ extern int socketpair(int domain, int type, int protocol, int sv[2]); -struct in6_addr const in6addr_any = {.s6_addr = {(unsigned char)0}}; -struct in6_addr const in6addr_loopback = - {.s6_addr = {(unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF, - (unsigned char)0xFF}}; +struct in6_addr const in6addr_any; + +struct in6_addr const in6addr_loopback; + /*@ assigns \result; assigns \result \from arg; */ extern uint32_t htonl(uint32_t arg); @@ -3957,7 +3942,7 @@ int h_errno; */ extern void freeaddrinfo(struct addrinfo *addrinfo); -char *__fc_gai_strerror = (char *)"<error message reported by gai_strerror>"; +char const *__fc_gai_strerror = "<error message reported by gai_strerror>"; /*@ ensures result_string: \result ≡ __fc_gai_strerror; ensures result_valid_string: valid_read_string(\result); assigns \result; @@ -3995,6 +3980,8 @@ int memcmp(void const *s1, void const *s2, size_t n); void *memchr(void const *s, int c, size_t n); +void *memrchr(void const *s, int c, size_t n); + void *memcpy(void * restrict dest, void const * restrict src, size_t n); void *memmove(void *dest, void const *src, size_t n); @@ -4412,7 +4399,12 @@ int getaddrinfo(char const * restrict nodename, ai->ai_protocol = Frama_C_interval(0,IPPROTO_MAX); ai->ai_addrlen = sizeof(*sa); ai->ai_addr = sa; - ai->ai_canonname = (char *)"dummy"; + ai->ai_canonname = (char *)malloc((unsigned int)6); + if (! ai->ai_canonname) { + __retres = -10; + goto return_label; + } + strcpy(ai->ai_canonname,"dummy"); ai->ai_next = (struct addrinfo *)0; *res = ai; __retres = 0; @@ -4423,8 +4415,8 @@ int getaddrinfo(char const * restrict nodename, } struct __fc_gethostbyname __fc_ghbn; -int res_search(char const *dname, int class, int type, char *answer, - int anslen) +static int res_search(char const *dname, int rec_class, int type, + char *answer, int anslen) { int tmp; { @@ -4475,8 +4467,10 @@ struct hostent *gethostbyname(char const *name) __retres = & __fc_ghbn.host; goto return_label; } - if ((int)*cp < '0') - if ((int)*cp > '9') + if ((int)*cp < '0') break; + else + if ((int)*cp > '9') break; + else if ((int)*cp != '.') break; cp ++; } @@ -4510,6 +4504,24 @@ struct hostent *gethostbyname(char const *name) return_label: return __retres; } +struct in6_addr const in6addr_any = {.s6_addr = {(unsigned char)0}}; +struct in6_addr const in6addr_loopback = + {.s6_addr = {(unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)0, + (unsigned char)1}}; FILE *__fc_stderr; FILE *__fc_stdin; @@ -5294,7 +5306,8 @@ int putenv(char *string) { int __retres; int tmp_3; - char *separator = strchr((char const *)string,'='); + char *separator __attribute__((__unused__)) = + strchr((char const *)string,'='); /*@ assert string_contains_separator: separator ≢ \null; */ ; /*@ assert name_is_not_empty: separator ≢ string; */ ; __fc_initenv(); @@ -6205,7 +6218,7 @@ char *strstr(char const *haystack, char const *needle) return_label: return __retres; } -static int __fc_strerror_init; +static int strerror___fc_strerror_init; /*@ ensures result_internal_str: \result ≡ __fc_p_strerror; ensures result_nul_terminated: *(\result + 63) ≡ 0; ensures result_valid_string: valid_read_string(\result); @@ -6215,10 +6228,10 @@ static int __fc_strerror_init; char *strerror(int errnum) { char *__retres; - if (! __fc_strerror_init) { + if (! strerror___fc_strerror_init) { Frama_C_make_unknown(__fc_strerror,(unsigned int)63); __fc_strerror[63] = (char)0; - __fc_strerror_init = 1; + strerror___fc_strerror_init = 1; } __retres = __fc_strerror; return __retres; @@ -6319,7 +6332,7 @@ char *strndup(char const *s, size_t n) return_label: return __retres; } -static int __fc_strsignal_init; +static int strsignal___fc_strsignal_init; /*@ ensures result_internal_str: \result ≡ __fc_p_strsignal; ensures result_nul_terminated: *(\result + 63) ≡ 0; ensures result_valid_string: valid_read_string(\result); @@ -6329,10 +6342,10 @@ static int __fc_strsignal_init; char *strsignal(int signum) { char *__retres; - if (! __fc_strsignal_init) { + if (! strsignal___fc_strsignal_init) { Frama_C_make_unknown(__fc_strsignal,(unsigned int)63); __fc_strsignal[63] = (char)0; - __fc_strsignal_init = 1; + strsignal___fc_strsignal_init = 1; } __retres = __fc_strsignal; return __retres; diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle index d3a9ddf8739d7d2f6c2fd17824835df5ae36eff3..ce170ab4761f6c58b3616ea4f242c97c7524ccec 100644 --- a/tests/libc/oracle/netdb_c.res.oracle +++ b/tests/libc/oracle/netdb_c.res.oracle @@ -57,7 +57,7 @@ [eva] tests/libc/netdb_c.c:33: Call to builtin memset [eva] tests/libc/netdb_c.c:33: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] computing for function getaddrinfo <- main. Called from tests/libc/netdb_c.c:42. @@ -125,6 +125,20 @@ [eva] share/libc/netdb.c:69: function Frama_C_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_interval +[eva] share/libc/netdb.c:72: Call to builtin malloc +[eva] share/libc/netdb.c:72: allocating variable __malloc_getaddrinfo_l72 +[eva] computing for function strcpy <- getaddrinfo <- main. + Called from share/libc/netdb.c:74. +[eva] using specification for function strcpy +[eva] share/libc/netdb.c:74: + function strcpy: precondition 'valid_string_src' got status valid. +[eva] share/libc/netdb.c:74: + function strcpy: precondition 'room_string' got status valid. +[eva] share/libc/netdb.c:74: + function strcpy: precondition 'separation' got status valid. +[eva] share/libc/string.h:360: + cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp +[eva] Done for function strcpy [eva] Recording results for getaddrinfo [eva] Done for function getaddrinfo [eva] computing for function gai_strerror <- main. @@ -180,76 +194,76 @@ [eva] computing for function gethostbyname <- main. Called from tests/libc/netdb_c.c:71. [eva] computing for function res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:139. + Called from share/libc/netdb.c:141. [eva] computing for function Frama_C_char_interval <- res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:97. + Called from share/libc/netdb.c:99. [eva] using specification for function Frama_C_char_interval -[eva] share/libc/netdb.c:97: +[eva] share/libc/netdb.c:99: function Frama_C_char_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_char_interval [eva] computing for function Frama_C_char_interval <- res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:97. + Called from share/libc/netdb.c:99. [eva] Done for function Frama_C_char_interval [eva] computing for function Frama_C_char_interval <- res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:97. + Called from share/libc/netdb.c:99. [eva] Done for function Frama_C_char_interval -[eva] share/libc/netdb.c:96: starting to merge loop iterations +[eva] share/libc/netdb.c:98: starting to merge loop iterations [eva] computing for function Frama_C_char_interval <- res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:97. + Called from share/libc/netdb.c:99. [eva] Done for function Frama_C_char_interval [eva] computing for function Frama_C_char_interval <- res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:97. + Called from share/libc/netdb.c:99. [eva] Done for function Frama_C_char_interval [eva] computing for function Frama_C_char_interval <- res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:97. + Called from share/libc/netdb.c:99. [eva] Done for function Frama_C_char_interval [eva] computing for function Frama_C_char_interval <- res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:97. + Called from share/libc/netdb.c:99. [eva] Done for function Frama_C_char_interval [eva] computing for function Frama_C_interval <- res_search <- gethostbyname <- main. - Called from share/libc/netdb.c:100. -[eva] share/libc/netdb.c:100: + Called from share/libc/netdb.c:102. +[eva] share/libc/netdb.c:102: function Frama_C_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_interval [eva] Recording results for res_search [eva] Done for function res_search [eva] computing for function Frama_C_nondet <- gethostbyname <- main. - Called from share/libc/netdb.c:142. + Called from share/libc/netdb.c:144. [eva] using specification for function Frama_C_nondet [eva] Done for function Frama_C_nondet [eva] computing for function inet_addr <- gethostbyname <- main. - Called from share/libc/netdb.c:145. + Called from share/libc/netdb.c:147. [eva] using specification for function inet_addr -[eva] share/libc/netdb.c:145: +[eva] share/libc/netdb.c:147: function inet_addr: precondition 'valid_arg' got status valid. [eva] Done for function inet_addr -[eva] share/libc/netdb.c:146: Call to builtin memcpy -[eva] share/libc/netdb.c:146: +[eva] share/libc/netdb.c:148: Call to builtin memcpy +[eva] share/libc/netdb.c:148: function memcpy: precondition 'valid_dest' got status valid. -[eva] share/libc/netdb.c:146: +[eva] share/libc/netdb.c:148: function memcpy: precondition 'valid_src' got status valid. -[eva] share/libc/netdb.c:146: +[eva] share/libc/netdb.c:148: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] computing for function strncpy <- gethostbyname <- main. - Called from share/libc/netdb.c:147. + Called from share/libc/netdb.c:149. [eva] using specification for function strncpy -[eva] share/libc/netdb.c:147: +[eva] share/libc/netdb.c:149: function strncpy: precondition 'valid_nstring_src' got status valid. -[eva] share/libc/netdb.c:147: +[eva] share/libc/netdb.c:149: function strncpy: precondition 'room_nstring' got status valid. -[eva] share/libc/netdb.c:147: +[eva] share/libc/netdb.c:149: function strncpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:373: +[eva] share/libc/string.h:376: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp [eva] Done for function strncpy [eva] Recording results for gethostbyname @@ -257,6 +271,11 @@ [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== +[eva:final-states] Values at end of function res_search: + Frama_C_entropy_source ∈ [--..--] + buf[0..1] ∈ [--..--] + [2..126] ∈ [--..--] or UNINITIALIZED + [127] ∈ {0} [eva:final-states] Values at end of function getaddrinfo: __fc_errno ∈ [--..--] __fc_heap_status ∈ [--..--] @@ -271,15 +290,12 @@ .ai_addrlen ∈ {16} or UNINITIALIZED .ai_addr ∈ {{ &__malloc_getaddrinfo_l58 }} or UNINITIALIZED - .ai_canonname ∈ {{ "dummy" }} or UNINITIALIZED + .ai_canonname ∈ + {{ NULL ; &__malloc_getaddrinfo_l72[0] }} or UNINITIALIZED .ai_next ∈ {0} or UNINITIALIZED __malloc_getaddrinfo_l58.sa_family ∈ [0..43] .sa_data[0..13] ∈ [--..--] -[eva:final-states] Values at end of function res_search: - Frama_C_entropy_source ∈ [--..--] - buf[0..1] ∈ [--..--] - [2..126] ∈ [--..--] or UNINITIALIZED - [127] ∈ {0} + __malloc_getaddrinfo_l72[0..5] ∈ [--..--] or UNINITIALIZED [eva:final-states] Values at end of function gethostbyname: Frama_C_entropy_source ∈ [--..--] __fc_ghbn.host.h_name ∈ {{ NULL ; &__fc_ghbn.hostbuf[0] }} @@ -332,7 +348,9 @@ .ai_protocol ∈ [0..256] .ai_addrlen ∈ {16} .ai_addr ∈ {{ &__malloc_getaddrinfo_l58 }} - .ai_canonname ∈ {{ "dummy" }} + .ai_canonname ∈ + {{ &__malloc_getaddrinfo_l72[0] }} .ai_next ∈ {0} __malloc_getaddrinfo_l58.sa_family ∈ [0..43] .sa_data[0..13] ∈ [--..--] + __malloc_getaddrinfo_l72[0..5] ∈ [--..--] or UNINITIALIZED diff --git a/tests/libc/oracle/netinet_in_h.res.oracle b/tests/libc/oracle/netinet_in_h.res.oracle index 9617fa5c6d1d379d79aa96ff79b9cb3ceaf8380a..a8fa5453586f36f4e871c4dd82be2f2df0d85e3c 100644 --- a/tests/libc/oracle/netinet_in_h.res.oracle +++ b/tests/libc/oracle/netinet_in_h.res.oracle @@ -23,5 +23,10 @@ __fc_inet_ntoa_array[0..14] ∈ [--..--] [15] ∈ {0} addr ∈ {0} + sockaddr6_any ∈ {0} + sockaddr6_loopback{.sin6_family; .sin6_port; .sin6_flowinfo; .sin6_addr.s6_addr[0..14]} ∈ + {0} + .sin6_addr.s6_addr[15] ∈ {1} + .sin6_scope_id ∈ {0} __retres ∈ {0} S___fc_stdout[0..1] ∈ [--..--] diff --git a/tests/libc/oracle/socket.0.res.oracle b/tests/libc/oracle/socket.0.res.oracle index 48e1188adc1eec3181a98ebf3d7f8042a9e9e061..d3cbc6849dd201722a97d1d88416911658cff675 100644 --- a/tests/libc/oracle/socket.0.res.oracle +++ b/tests/libc/oracle/socket.0.res.oracle @@ -143,7 +143,7 @@ [eva] using specification for function memset [eva] tests/libc/socket.c:103: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Done for function memset [eva] computing for function bind <- test_server_echo <- main. diff --git a/tests/libc/oracle/socket.1.res.oracle b/tests/libc/oracle/socket.1.res.oracle index 75af74969ffec16136e49df67f85b4d6e4cbae09..eb0bfef77cb0ccd765bf162598cac8399cb3dbbf 100644 --- a/tests/libc/oracle/socket.1.res.oracle +++ b/tests/libc/oracle/socket.1.res.oracle @@ -143,7 +143,7 @@ [eva] using specification for function memset [eva] tests/libc/socket.c:103: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Done for function memset [eva] computing for function bind <- test_server_echo <- main. diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle index 37236106c30bd495d092e4bacb9743ac813b498a..f7de7fafd0dfa347db4dc2d2b1a9b568c00e18a6 100644 --- a/tests/libc/oracle/stdlib_c.2.res.oracle +++ b/tests/libc/oracle/stdlib_c.2.res.oracle @@ -13,7 +13,7 @@ [eva] using specification for function memset [eva] share/libc/stdlib.c:73: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] Done for function memset [eva] Recording results for calloc diff --git a/tests/libc/oracle/stdlib_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle index e39d01ba5bf5415cbb065c34c0e0af0a79d49307..ec542fd1b029ce11e98e446bc4c387f8cf332ce2 100644 --- a/tests/libc/oracle/stdlib_c_env.res.oracle +++ b/tests/libc/oracle/stdlib_c_env.res.oracle @@ -9,7 +9,7 @@ [eva] share/libc/stdlib.c:114: Call to builtin strchr [eva] share/libc/stdlib.c:114: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:165: +[eva] share/libc/string.h:168: cannot evaluate ACSL term, unsupported logic var p [eva] share/libc/stdlib.c:115: assertion 'string_contains_separator' got status valid. @@ -107,7 +107,7 @@ function strcpy: precondition 'room_string' got status valid. [eva] tests/libc/stdlib_c_env.c:15: function strcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:357: +[eva] share/libc/string.h:360: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp [eva] Done for function strcpy [eva] computing for function getenv <- main. diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle index 401829973b44023601fe892716db53d08870ea00..092b636ecee8c5ce4cfc48a3e8dadade0e2b235b 100644 --- a/tests/libc/oracle/string_c.res.oracle +++ b/tests/libc/oracle/string_c.res.oracle @@ -14,11 +14,11 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/libc/string_c.c:10: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp -[eva:alarm] share/libc/string.h:98: Warning: +[eva:alarm] share/libc/string.h:101: Warning: function memcpy: postcondition 'copied_contents' got status unknown. -[eva] share/libc/string.h:99: +[eva] share/libc/string.h:102: function memcpy: postcondition 'result_ptr' got status valid. [eva] Recording results for memcpy [eva] Done for function memcpy @@ -95,11 +95,11 @@ function memoverlap, behavior not_separated_gt: postcondition 'result_p_after_q' got status valid. [eva] Recording results for memoverlap [eva] Done for function memoverlap -[eva] share/libc/string.h:108: +[eva] share/libc/string.h:111: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp -[eva:alarm] share/libc/string.h:108: Warning: +[eva:alarm] share/libc/string.h:111: Warning: function memmove: postcondition 'copied_contents' got status unknown. -[eva] share/libc/string.h:109: +[eva] share/libc/string.h:112: function memmove: postcondition 'result_ptr' got status valid. [eva] Recording results for memmove [eva] Done for function memmove @@ -156,7 +156,7 @@ Called from tests/libc/string_c.c:64. [eva] tests/libc/string_c.c:64: function strlen: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:127: +[eva] share/libc/string.h:130: function strlen: postcondition 'acsl_c_equiv' got status valid. [eva] Recording results for strlen [eva] Done for function strlen @@ -183,7 +183,7 @@ Called from tests/libc/string_c.c:75. [eva] tests/libc/string_c.c:75: function strnlen: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:133: +[eva] share/libc/string.h:136: function strnlen: postcondition 'result_bounded' got status valid. [eva] Recording results for strnlen [eva] Done for function strnlen @@ -231,11 +231,11 @@ Called from tests/libc/string_c.c:92. [eva] tests/libc/string_c.c:92: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset -[eva:alarm] share/libc/string.h:118: Warning: +[eva:alarm] share/libc/string.h:121: Warning: function memset: postcondition 'acsl_c_equiv' got status unknown. -[eva] share/libc/string.h:119: +[eva] share/libc/string.h:122: function memset: postcondition 'result_ptr' got status valid. [eva] Recording results for memset [eva] Done for function memset @@ -259,9 +259,9 @@ function strcmp: precondition 'valid_string_s1' got status valid. [eva] tests/libc/string_c.c:104: function strcmp: precondition 'valid_string_s2' got status valid. -[eva] share/libc/string.h:140: +[eva] share/libc/string.h:143: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp -[eva:alarm] share/libc/string.h:140: Warning: +[eva:alarm] share/libc/string.h:143: Warning: function strcmp: postcondition 'acsl_c_equiv' got status unknown. [eva] Recording results for strcmp [eva] Done for function strcmp @@ -330,9 +330,9 @@ function strncmp: precondition 'valid_string_s1' got status valid. [eva] tests/libc/string_c.c:167: function strncmp: precondition 'valid_string_s2' got status valid. -[eva] share/libc/string.h:147: +[eva] share/libc/string.h:150: cannot evaluate ACSL term, unsupported ACSL construct: logic function strncmp -[eva:alarm] share/libc/string.h:147: Warning: +[eva:alarm] share/libc/string.h:150: Warning: function strncmp: postcondition 'acsl_c_equiv' got status unknown. [eva] Recording results for strncmp [eva] Done for function strncmp @@ -494,13 +494,13 @@ function strlen: precondition 'valid_string_s' got status valid. [eva] Recording results for strlen [eva] Done for function strlen -[eva] share/libc/string.h:413: - function strcat: postcondition 'sum_of_lengths' got status valid. [eva] share/libc/string.h:416: + function strcat: postcondition 'sum_of_lengths' got status valid. +[eva] share/libc/string.h:419: function strcat: postcondition 'initialization,dest' got status valid. -[eva] share/libc/string.h:417: +[eva] share/libc/string.h:420: function strcat: postcondition 'dest_null_terminated' got status valid. -[eva] share/libc/string.h:418: +[eva] share/libc/string.h:421: function strcat: postcondition 'result_ptr' got status valid. [eva] Recording results for strcat [eva] Done for function strcat @@ -559,11 +559,11 @@ function strcpy: precondition 'room_string' got status valid. [eva] tests/libc/string_c.c:142: function strcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:357: +[eva] share/libc/string.h:360: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp -[eva:alarm] share/libc/string.h:357: Warning: +[eva:alarm] share/libc/string.h:360: Warning: function strcpy: postcondition 'equal_contents' got status unknown. -[eva] share/libc/string.h:358: +[eva] share/libc/string.h:361: function strcpy: postcondition 'result_ptr' got status valid. [eva] Recording results for strcpy [eva] Done for function strcpy @@ -603,13 +603,13 @@ function strncpy: precondition 'room_nstring' got status valid. [eva] tests/libc/string_c.c:154: function strncpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:369: +[eva] share/libc/string.h:372: function strncpy: postcondition 'result_ptr' got status valid. -[eva] share/libc/string.h:370: - function strncpy: postcondition 'initialization' got status valid. [eva] share/libc/string.h:373: + function strncpy: postcondition 'initialization' got status valid. +[eva] share/libc/string.h:376: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp -[eva:alarm] share/libc/string.h:373: Warning: +[eva:alarm] share/libc/string.h:376: Warning: function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown. [eva] Recording results for strncpy [eva] Done for function strncpy @@ -623,9 +623,9 @@ function strncpy: precondition 'room_nstring' got status valid. [eva] tests/libc/string_c.c:157: function strncpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:376: +[eva] share/libc/string.h:379: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp -[eva:alarm] share/libc/string.h:376: Warning: +[eva:alarm] share/libc/string.h:379: Warning: function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown. [eva] Recording results for strncpy [eva] Done for function strncpy @@ -660,19 +660,19 @@ Called from tests/libc/string_c.c:201. [eva] tests/libc/string_c.c:201: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:161: +[eva] share/libc/string.h:164: function strchr, behavior found: postcondition 'result_char' got status valid. -[eva] share/libc/string.h:162: +[eva] share/libc/string.h:165: function strchr, behavior found: postcondition 'result_same_base' got status valid. -[eva] share/libc/string.h:163: +[eva] share/libc/string.h:166: function strchr, behavior found: postcondition 'result_in_length' got status valid. -[eva] share/libc/string.h:164: +[eva] share/libc/string.h:167: function strchr, behavior found: postcondition 'result_valid_string' got status valid. -[eva] share/libc/string.h:165: +[eva] share/libc/string.h:168: cannot evaluate ACSL term, unsupported logic var p -[eva:alarm] share/libc/string.h:165: Warning: +[eva:alarm] share/libc/string.h:168: Warning: function strchr, behavior found: postcondition 'result_first_occur' got status unknown. -[eva] share/libc/string.h:171: +[eva] share/libc/string.h:174: function strchr, behavior default: postcondition 'result_null_or_same_base' got status valid. [eva] Recording results for strchr [eva] Done for function strchr @@ -681,7 +681,7 @@ Called from tests/libc/string_c.c:203. [eva] tests/libc/string_c.c:203: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:168: +[eva] share/libc/string.h:171: function strchr, behavior not_found: postcondition 'result_null' got status valid. [eva] Recording results for strchr [eva] Done for function strchr @@ -714,13 +714,13 @@ function strlen: precondition 'valid_string_s' got status valid. [eva] Recording results for strlen [eva] Done for function strlen -[eva] share/libc/string.h:185: +[eva] share/libc/string.h:188: function strrchr, behavior found: postcondition 'result_char' got status valid. -[eva] share/libc/string.h:186: +[eva] share/libc/string.h:189: function strrchr, behavior found: postcondition 'result_same_base' got status valid. -[eva] share/libc/string.h:187: +[eva] share/libc/string.h:190: function strrchr, behavior found: postcondition 'result_valid_string' got status valid. -[eva] share/libc/string.h:193: +[eva] share/libc/string.h:196: function strrchr, behavior default: postcondition 'result_null_or_same_base' got status valid. [eva] Recording results for strrchr [eva] Done for function strrchr @@ -730,7 +730,7 @@ [eva] tests/libc/string_c.c:216: function strrchr: precondition 'valid_string_s' got status valid. [eva] share/libc/string.c:237: Reusing old results for call to strlen -[eva] share/libc/string.h:190: +[eva] share/libc/string.h:193: function strrchr, behavior not_found: postcondition 'result_null' got status valid. [eva] Recording results for strrchr [eva] Done for function strrchr @@ -885,9 +885,9 @@ function strstr: precondition 'valid_string_haystack' got status valid. [eva] tests/libc/string_c.c:261: function strstr: precondition 'valid_string_needle' got status valid. -[eva] share/libc/string.h:227: +[eva] share/libc/string.h:230: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp -[eva:alarm] share/libc/string.h:225: Warning: +[eva:alarm] share/libc/string.h:228: Warning: function strstr: postcondition 'result_null_or_in_haystack' got status unknown. [eva] Recording results for strstr [eva] Done for function strstr @@ -907,7 +907,7 @@ function strstr: precondition 'valid_string_haystack' got status valid. [eva] tests/libc/string_c.c:265: function strstr: precondition 'valid_string_needle' got status valid. -[eva] share/libc/string.h:225: +[eva] share/libc/string.h:228: function strstr: postcondition 'result_null_or_in_haystack' got status valid. [eva] Recording results for strstr [eva] Done for function strstr diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle index 4e1e5145535fa6ef9dd6ed43f042e6125df52320..a56dbf77d66ed1dffd06b58ce3ce2ca5189508b9 100644 --- a/tests/libc/oracle/string_c_generic.res.oracle +++ b/tests/libc/oracle/string_c_generic.res.oracle @@ -12,11 +12,11 @@ function strcpy: precondition 'room_string' got status valid. [eva] tests/libc/string_c_generic.c:56: function strcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:357: +[eva] share/libc/string.h:360: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp -[eva:alarm] share/libc/string.h:357: Warning: +[eva:alarm] share/libc/string.h:360: Warning: function strcpy: postcondition 'equal_contents' got status unknown. -[eva] share/libc/string.h:358: +[eva] share/libc/string.h:361: function strcpy: postcondition 'result_ptr' got status valid. [eva] Recording results for strcpy [eva] Done for function strcpy @@ -26,9 +26,9 @@ function strcmp: precondition 'valid_string_s1' got status valid. [eva] tests/libc/string_c_generic.c:57: function strcmp: precondition 'valid_string_s2' got status valid. -[eva] share/libc/string.h:140: +[eva] share/libc/string.h:143: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp -[eva:alarm] share/libc/string.h:140: Warning: +[eva:alarm] share/libc/string.h:143: Warning: function strcmp: postcondition 'acsl_c_equiv' got status unknown. [eva] Recording results for strcmp [eva] Done for function strcmp @@ -144,11 +144,11 @@ Called from tests/libc/string_c_generic.c:72. [eva] tests/libc/string_c_generic.c:72: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset -[eva:alarm] share/libc/string.h:118: Warning: +[eva:alarm] share/libc/string.h:121: Warning: function memset: postcondition 'acsl_c_equiv' got status unknown. -[eva] share/libc/string.h:119: +[eva] share/libc/string.h:122: function memset: postcondition 'result_ptr' got status valid. [eva] Recording results for memset [eva] Done for function memset @@ -161,13 +161,13 @@ [eva] tests/libc/string_c_generic.c:73: function strncpy: precondition 'separation' got status valid. [eva] share/libc/string.c:220: starting to merge loop iterations -[eva] share/libc/string.h:369: +[eva] share/libc/string.h:372: function strncpy: postcondition 'result_ptr' got status valid. -[eva] share/libc/string.h:370: - function strncpy: postcondition 'initialization' got status valid. [eva] share/libc/string.h:373: + function strncpy: postcondition 'initialization' got status valid. +[eva] share/libc/string.h:376: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp -[eva:alarm] share/libc/string.h:373: Warning: +[eva:alarm] share/libc/string.h:376: Warning: function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown. [eva] Recording results for strncpy [eva] Done for function strncpy @@ -199,9 +199,9 @@ function strncpy: precondition 'room_nstring' got status valid. [eva] tests/libc/string_c_generic.c:78: function strncpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:376: +[eva] share/libc/string.h:379: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp -[eva:alarm] share/libc/string.h:376: Warning: +[eva:alarm] share/libc/string.h:379: Warning: function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown. [eva] Recording results for strncpy [eva] Done for function strncpy @@ -212,9 +212,9 @@ [eva] tests/libc/string_c_generic.c:82: function strncmp: precondition 'valid_string_s2' got status valid. [eva] share/libc/string.c:138: starting to merge loop iterations -[eva] share/libc/string.h:147: +[eva] share/libc/string.h:150: cannot evaluate ACSL term, unsupported ACSL construct: logic function strncmp -[eva:alarm] share/libc/string.h:147: Warning: +[eva:alarm] share/libc/string.h:150: Warning: function strncmp: postcondition 'acsl_c_equiv' got status unknown. [eva] Recording results for strncmp [eva] Done for function strncmp @@ -248,13 +248,13 @@ Called from share/libc/string.c:193. [eva] share/libc/string.c:193: function strlen: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:127: +[eva] share/libc/string.h:130: function strlen: postcondition 'acsl_c_equiv' got status valid. [eva] Recording results for strlen [eva] Done for function strlen -[eva] share/libc/string.h:427: +[eva] share/libc/string.h:430: function strncat: postcondition 'result_ptr' got status valid. -[eva] share/libc/string.h:442: +[eva] share/libc/string.h:445: function strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status valid. [eva] Recording results for strncat [eva] Done for function strncat @@ -280,19 +280,19 @@ Called from tests/libc/string_c_generic.c:91. [eva] tests/libc/string_c_generic.c:91: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:161: +[eva] share/libc/string.h:164: function strchr, behavior found: postcondition 'result_char' got status valid. -[eva] share/libc/string.h:162: +[eva] share/libc/string.h:165: function strchr, behavior found: postcondition 'result_same_base' got status valid. -[eva] share/libc/string.h:163: +[eva] share/libc/string.h:166: function strchr, behavior found: postcondition 'result_in_length' got status valid. -[eva] share/libc/string.h:164: +[eva] share/libc/string.h:167: function strchr, behavior found: postcondition 'result_valid_string' got status valid. -[eva] share/libc/string.h:165: +[eva] share/libc/string.h:168: cannot evaluate ACSL term, unsupported logic var p -[eva:alarm] share/libc/string.h:165: Warning: +[eva:alarm] share/libc/string.h:168: Warning: function strchr, behavior found: postcondition 'result_first_occur' got status unknown. -[eva] share/libc/string.h:171: +[eva] share/libc/string.h:174: function strchr, behavior default: postcondition 'result_null_or_same_base' got status valid. [eva] Recording results for strchr [eva] Done for function strchr @@ -300,7 +300,7 @@ Called from tests/libc/string_c_generic.c:92. [eva] tests/libc/string_c_generic.c:92: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:168: +[eva] share/libc/string.h:171: function strchr, behavior not_found: postcondition 'result_null' got status valid. [eva] Recording results for strchr [eva] Done for function strchr @@ -314,13 +314,13 @@ function strlen: precondition 'valid_string_s' got status valid. [eva] Recording results for strlen [eva] Done for function strlen -[eva] share/libc/string.h:185: +[eva] share/libc/string.h:188: function strrchr, behavior found: postcondition 'result_char' got status valid. -[eva] share/libc/string.h:186: +[eva] share/libc/string.h:189: function strrchr, behavior found: postcondition 'result_same_base' got status valid. -[eva] share/libc/string.h:187: +[eva] share/libc/string.h:190: function strrchr, behavior found: postcondition 'result_valid_string' got status valid. -[eva] share/libc/string.h:193: +[eva] share/libc/string.h:196: function strrchr, behavior default: postcondition 'result_null_or_same_base' got status valid. [eva] Recording results for strrchr [eva] Done for function strrchr @@ -330,7 +330,7 @@ function strrchr: precondition 'valid_string_s' got status valid. [eva] share/libc/string.c:237: Reusing old results for call to strlen [eva] share/libc/string.c:237: starting to merge loop iterations -[eva] share/libc/string.h:190: +[eva] share/libc/string.h:193: function strrchr, behavior not_found: postcondition 'result_null' got status valid. [eva] Recording results for strrchr [eva] Done for function strrchr diff --git a/tests/libc/oracle/string_c_strchr.res.oracle b/tests/libc/oracle/string_c_strchr.res.oracle index d389a3cf5615c82c1b364e246fbcfeded5ef7fca..58c1b64452539bdb7fe3553b2bb1a29b2ceebe44 100644 --- a/tests/libc/oracle/string_c_strchr.res.oracle +++ b/tests/libc/oracle/string_c_strchr.res.oracle @@ -12,9 +12,9 @@ Called from tests/libc/string_c_strchr.c:62. [eva] tests/libc/string_c_strchr.c:62: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:168: - function strchr, behavior not_found: postcondition 'result_null' got status valid. [eva] share/libc/string.h:171: + function strchr, behavior not_found: postcondition 'result_null' got status valid. +[eva] share/libc/string.h:174: function strchr, behavior default: postcondition 'result_null_or_same_base' got status valid. [eva] Recording results for strchr [eva] Done for function strchr @@ -59,17 +59,17 @@ Called from tests/libc/string_c_strchr.c:70. [eva] tests/libc/string_c_strchr.c:70: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:161: +[eva] share/libc/string.h:164: function strchr, behavior found: postcondition 'result_char' got status valid. -[eva] share/libc/string.h:162: +[eva] share/libc/string.h:165: function strchr, behavior found: postcondition 'result_same_base' got status valid. -[eva] share/libc/string.h:163: +[eva] share/libc/string.h:166: function strchr, behavior found: postcondition 'result_in_length' got status valid. -[eva] share/libc/string.h:164: +[eva] share/libc/string.h:167: function strchr, behavior found: postcondition 'result_valid_string' got status valid. -[eva] share/libc/string.h:165: +[eva] share/libc/string.h:168: cannot evaluate ACSL term, unsupported logic var p -[eva:alarm] share/libc/string.h:165: Warning: +[eva:alarm] share/libc/string.h:168: Warning: function strchr, behavior found: postcondition 'result_first_occur' got status unknown. [eva] Recording results for strchr [eva] Done for function strchr diff --git a/tests/libc/oracle/string_c_strstr.res.oracle b/tests/libc/oracle/string_c_strstr.res.oracle index ab662fa08022158d2b0489c22f11ea04a4190141..d05d2e49cd3de7f0d9aea564896536061c8b598c 100644 --- a/tests/libc/oracle/string_c_strstr.res.oracle +++ b/tests/libc/oracle/string_c_strstr.res.oracle @@ -10,7 +10,7 @@ function strstr: precondition 'valid_string_haystack' got status valid. [eva] tests/libc/string_c_strstr.c:52: function strstr: precondition 'valid_string_needle' got status valid. -[eva] share/libc/string.h:225: +[eva] share/libc/string.h:228: function strstr: postcondition 'result_null_or_in_haystack' got status valid. [eva] Recording results for strstr [eva] Done for function strstr @@ -101,9 +101,9 @@ function strstr: precondition 'valid_string_haystack' got status valid. [eva] tests/libc/string_c_strstr.c:64: function strstr: precondition 'valid_string_needle' got status valid. -[eva] share/libc/string.h:227: +[eva] share/libc/string.h:230: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp -[eva:alarm] share/libc/string.h:225: Warning: +[eva:alarm] share/libc/string.h:228: Warning: function strstr: postcondition 'result_null_or_in_haystack' got status unknown. [eva] Recording results for strstr [eva] Done for function strstr diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle index 694c2eca6d343c4e01bd0f49cd4dff2a4221be53..a7cb7e2344c89a1c94f386b665431f6bdf0d7a4a 100644 --- a/tests/libc/oracle/string_h.res.oracle +++ b/tests/libc/oracle/string_h.res.oracle @@ -13,7 +13,7 @@ function strcmp: precondition 'valid_string_s1' got status valid. [eva] tests/libc/string_h.c:5: function strcmp: precondition 'valid_string_s2' got status valid. -[eva] share/libc/string.h:140: +[eva] share/libc/string.h:143: cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp [eva] Done for function strcmp [eva:alarm] tests/libc/string_h.c:6: Warning: assertion got status unknown. @@ -51,7 +51,7 @@ function strstr: precondition 'valid_string_haystack' got status valid. [eva] tests/libc/string_h.c:24: function strstr: precondition 'valid_string_needle' got status valid. -[eva] share/libc/string.h:227: +[eva] share/libc/string.h:230: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] Done for function strstr [eva:alarm] tests/libc/string_h.c:25: Warning: assertion got status unknown. @@ -325,7 +325,7 @@ [eva] tests/libc/string_h.c:154: Call to builtin strchr [eva] tests/libc/string_h.c:154: function strchr: precondition 'valid_string_s' got status valid. -[eva] share/libc/string.h:165: +[eva] share/libc/string.h:168: cannot evaluate ACSL term, unsupported logic var p [eva] computing for function strchrnul <- main. Called from tests/libc/string_h.c:155. diff --git a/tests/libc/oracle/sys_select.res.oracle b/tests/libc/oracle/sys_select.res.oracle index 453a3465161df7694e3616278d3db5120e82a673..f784239499a3c4eeef28ff6852ceee7a4c6496b0 100644 --- a/tests/libc/oracle/sys_select.res.oracle +++ b/tests/libc/oracle/sys_select.res.oracle @@ -15,7 +15,7 @@ [eva] tests/libc/sys_select.c:16: Call to builtin memset [eva] tests/libc/sys_select.c:16: function memset: precondition 'valid_s' got status valid. -[eva] share/libc/string.h:118: +[eva] share/libc/string.h:121: cannot evaluate ACSL term, unsupported ACSL construct: logic function memset [eva] computing for function htonl <- main. Called from tests/libc/sys_select.c:18. @@ -57,7 +57,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/libc/sys_select.c:30: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] computing for function select <- main. Called from tests/libc/sys_select.c:31. diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c index 69ea8ad364922e00488a4a0c3c66fec0fbe0d032..bb282df999d8dca402c6ebdf6b5284021f50e629 100644 --- a/tests/libc/runtime.c +++ b/tests/libc/runtime.c @@ -1,6 +1,6 @@ /* run.config* COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...) - CMD: gcc -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null + CMD: gcc -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes -std=c99 -Wall -Wwrite-strings -o /dev/null OPT: */ diff --git a/tests/value/oracle/empty_struct2.res.oracle b/tests/value/oracle/empty_struct2.res.oracle index ce834bb8c236384fcaf9708f9bae281acf4c2809..f0ff1f6a21d1ca7ef93f6bc88b21f3f40fe3a989 100644 --- a/tests/value/oracle/empty_struct2.res.oracle +++ b/tests/value/oracle/empty_struct2.res.oracle @@ -15,7 +15,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/value/empty_struct2.c:52: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] tests/value/empty_struct2.c:57: Call to builtin memcpy [eva] tests/value/empty_struct2.c:57: diff --git a/tests/value/oracle/empty_union.res.oracle b/tests/value/oracle/empty_union.res.oracle index 81eff46197f3d00015306a96bb08116a75fab389..43959a75b22ca032276910afe27ebb5de76d2f91 100644 --- a/tests/value/oracle/empty_union.res.oracle +++ b/tests/value/oracle/empty_union.res.oracle @@ -22,7 +22,7 @@ function memcpy: precondition 'valid_src' got status valid. [eva] tests/value/empty_union.c:72: function memcpy: precondition 'separation' got status valid. -[eva] share/libc/string.h:98: +[eva] share/libc/string.h:101: cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp [eva] tests/value/empty_union.c:77: Call to builtin memcpy [eva] tests/value/empty_union.c:77: