diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h index 8e21ad8b05f21a1c436fe565fc172d5e66d4cf91..c49c989d98518f085d7578f1f8edea8dd5c82941 100644 --- a/share/libc/stdlib.h +++ b/share/libc/stdlib.h @@ -30,6 +30,7 @@ __PUSH_FC_STDLIB #include "__fc_define_wchar_t.h" #include "__fc_alloc_axiomatic.h" #include "__fc_string_axiomatic.h" +#include "errno.h" __BEGIN_DECLS @@ -752,34 +753,57 @@ extern int mkstemps(char *templat, int suffixlen); // some plugins such as Eva. In such cases, it is preferable to use the stub // provided in stdlib.c. /*@ - requires valid_file_name: valid_read_string(file_name); + requires valid_file_name_or_null: + file_name == \null || valid_read_string(file_name); requires resolved_name_null_or_allocated: resolved_name == \null || \valid(resolved_name+(0 .. PATH_MAX-1)); assigns __fc_heap_status \from indirect:resolved_name, __fc_heap_status; - assigns \result, resolved_name[0 .. PATH_MAX-1] \from + assigns \result[0 .. PATH_MAX-1], resolved_name[0 .. PATH_MAX-1] \from indirect:__fc_heap_status, indirect:resolved_name, indirect:file_name[0..]; + assigns __fc_errno \from + indirect:file_name, indirect:file_name[0..], indirect:resolved_name, + indirect:__fc_heap_status; + behavior null_file_name: + assumes null_file_name: file_name == \null; + assigns \result, __fc_errno \from indirect:file_name; + ensures null_result: \result == \null; + ensures errno_set: __fc_errno == EINVAL; behavior allocate_resolved_name: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; assumes can_allocate: is_allocable(PATH_MAX); assigns __fc_heap_status \from __fc_heap_status; assigns \result \from indirect:__fc_heap_status; ensures allocation: \fresh(\result,PATH_MAX); behavior not_enough_memory: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; + assumes cannot_allocate: !is_allocable(PATH_MAX); assigns \result \from \nothing; allocates \nothing; ensures null_result: \result == \null; + ensures errno_set: __fc_errno == ENOMEM; behavior resolved_name_buffer: + assumes valid_file_name: valid_read_string(file_name); assumes allocated_resolved_name_or_fail: \valid(resolved_name+(0 .. PATH_MAX-1)); - assigns \result \from \nothing; + assigns \result \from resolved_name; assigns resolved_name[0 .. PATH_MAX-1] \from indirect:file_name[0..]; - ensures valid_string_resolved_name: valid_string(resolved_name); + ensures valid_string_resolved_name: valid_string(resolved_name) + && strlen(resolved_name) < PATH_MAX; // missing: assigns \result, // resolved_name[0 .. PATH_MAX-1] \from 'filesystem'; ensures resolved_result: \result == resolved_name; allocates \nothing; - */ + behavior filesystem_error: + assumes valid_file_name: valid_read_string(file_name); + assigns \result, __fc_errno + \from indirect:file_name[0..]; // missing: indirect:'filesystem'; + ensures null_result: \result == \null; + ensures errno_set: + __fc_errno \in {EACCES, EIO, ELOOP, ENAMETOOLONG, ENOENT, ENOTDIR}; + allocates \nothing; +*/ extern char *realpath(const char *restrict file_name, char *restrict resolved_name); diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle index c3b727f9f15cbec8d940ee81081ccc586625237f..b17dc493cc2f314c2dec1e370a69f44f9481b406 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle @@ -2,13 +2,13 @@ [e-acsl] Warning: annotating undefined function `atoi': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:77: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:78: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:78: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:79: Warning: function __e_acsl_assert_register_ulong: precondition data->values == \null || \valid(data->values) got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:78: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:79: Warning: function __e_acsl_assert_register_int: precondition data->values == \null || \valid(data->values) got status unknown. diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c index 88da2376fc768869d3c05aa66d4b7b7feb0ed3ee..7db3574598a1c27e47a1159e8259708750fc77b0 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c +++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c @@ -45,7 +45,7 @@ int __gen_e_acsl_atoi(char const *nptr) __gen_e_acsl_assert_data.pred_txt = "\\valid_read(nptr)"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "atoi"; - __gen_e_acsl_assert_data.line = 78; + __gen_e_acsl_assert_data.line = 79; __gen_e_acsl_assert_data.name = "valid_nptr"; __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data); __e_acsl_assert_clean(& __gen_e_acsl_assert_data); diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c index 05ad2ab4d9630b9fc40e315b154e7f330e769fae..4b7638e94a5dcf4c5ad4f2e4c7a2c40e5efc0da5 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c +++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c @@ -792,7 +792,7 @@ void __gen_e_acsl_exit(int status) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "exit"; - __gen_e_acsl_assert_data.line = 508; + __gen_e_acsl_assert_data.line = 509; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c index b8a1cf816d1ff12b4a9d05f038ce82a244df2b9e..9c35a66cd700e4fb8ceffb736ce91231c9018973 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c +++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c @@ -357,7 +357,7 @@ void __gen_e_acsl_exit(int status) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "exit"; - __gen_e_acsl_assert_data.line = 508; + __gen_e_acsl_assert_data.line = 509; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; @@ -379,7 +379,7 @@ void __gen_e_acsl_abort(void) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "abort"; - __gen_e_acsl_assert_data.line = 495; + __gen_e_acsl_assert_data.line = 496; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c index a82b19ca899af10ef56efa8cd421b733dc5a0352..6f9d70db13712a2040066f398ae45df61fb4fb55 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c +++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c @@ -771,7 +771,7 @@ void __gen_e_acsl_exit(int status) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "exit"; - __gen_e_acsl_assert_data.line = 508; + __gen_e_acsl_assert_data.line = 509; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c index 2fc62ec2c840513dda53a243873a8c22eccbcdcb..f664123b0263e0f30b360cc8c7c13fb9e86f93dd 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c +++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c @@ -331,7 +331,7 @@ void __gen_e_acsl_exit(int status) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "exit"; - __gen_e_acsl_assert_data.line = 508; + __gen_e_acsl_assert_data.line = 509; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; @@ -353,7 +353,7 @@ void __gen_e_acsl_abort(void) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "abort"; - __gen_e_acsl_assert_data.line = 495; + __gen_e_acsl_assert_data.line = 496; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle index 3d4daab9ad5c01bd59d126de081bce4a0d624ff8..7f0d1b078e515df1319346ac4b3ced1735c9977d 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle +++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle @@ -17,10 +17,10 @@ [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:506: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:508: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle index f0f2dd6bac7d240b1951d30131abcc48f249fc1b..c5757eeb2476186670ecbd87134e9f890ddc23fd 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle +++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle @@ -58,17 +58,17 @@ [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:506: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:508: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:492: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:493: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:494: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:495: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle index ef798a2e8602f3a65f86a373bfa895fbab1a7e81..03b81f4802fa4f8e3ba5b51f4c87521e71b8e8bd 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle +++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle @@ -53,10 +53,10 @@ [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:506: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:508: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle index 1d60323480135dccc0464552181b36d335b2ba1f..312005092277b3411904efc7842a3a6f846f38b4 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle +++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle @@ -56,17 +56,17 @@ [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:506: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:508: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:492: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:493: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:494: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:495: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c index fae60f07a4bcf944b858ecc1f37eab71b82be061..7f656ff4aa67659c61002e0037cce0e3ea882059 100644 --- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c +++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c @@ -776,7 +776,7 @@ void __gen_e_acsl_exit(int status) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "exit"; - __gen_e_acsl_assert_data.line = 508; + __gen_e_acsl_assert_data.line = 509; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); __e_acsl_delete_block((void *)(& status)); diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c index c1b193f256bdb4dfd424e2e088cc6a97a9929acf..6a4c17bd9fe799e43e81072c64d4c02488159519 100644 --- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c +++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c @@ -458,7 +458,7 @@ void __gen_e_acsl_exit(int status) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "exit"; - __gen_e_acsl_assert_data.line = 508; + __gen_e_acsl_assert_data.line = 509; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); __e_acsl_delete_block((void *)(& status)); diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle index 67745c5779d052fc5f9d8e06f730b6de85791c61..15de4811925f5db10bf980a8b4578b0ec2855879 100644 --- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle +++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle @@ -38,10 +38,10 @@ [e-acsl] FRAMAC_SHARE/libc/unistd.h:1149: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:506: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:508: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle index 67745c5779d052fc5f9d8e06f730b6de85791c61..15de4811925f5db10bf980a8b4578b0ec2855879 100644 --- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle +++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle @@ -38,10 +38,10 @@ [e-acsl] FRAMAC_SHARE/libc/unistd.h:1149: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:506: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:508: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle index 63cbab9a25489dcf48f0a61f9a342c615f78d14e..e0ab74f6877939800c04eb5fb874710696087aba 100644 --- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle @@ -23,10 +23,10 @@ [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:506: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:508: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c index bb0d77edd343e52a469b3adcad7fc8a484a33197..4a33bd3241df783d731134af5c29df82ca0b3ce8 100644 --- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c +++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c @@ -270,7 +270,7 @@ void __gen_e_acsl_exit(int status) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "exit"; - __gen_e_acsl_assert_data.line = 508; + __gen_e_acsl_assert_data.line = 509; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c index 8999413f1a3f573d109e006b22b961daa53ab795..126be8f248f48ba6ae34effa046ec38adb5938bd 100644 --- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c +++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c @@ -1163,7 +1163,7 @@ void __gen_e_acsl_exit(int status) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "exit"; - __gen_e_acsl_assert_data.line = 508; + __gen_e_acsl_assert_data.line = 509; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; @@ -1185,7 +1185,7 @@ void __gen_e_acsl_abort(void) __gen_e_acsl_assert_data.pred_txt = "\\false"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "abort"; - __gen_e_acsl_assert_data.line = 495; + __gen_e_acsl_assert_data.line = 496; __gen_e_acsl_assert_data.name = "never_terminates"; __e_acsl_assert(0,& __gen_e_acsl_assert_data); return; diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle index e425c628ffce293fd2a82251275cb53c5fb3580f..7985a51f133c31c024c129b5931b94976ccb3dcb 100644 --- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle @@ -90,17 +90,17 @@ [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:89: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:505: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:506: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:507: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:508: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:492: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:493: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:494: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:495: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c index e38b61a985d5131b96d70d6eb3e58d3f4779068a..fc9c66c217bb9cac04a30bbc8f7e27e8472ad382 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c +++ b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c @@ -1,4 +1,5 @@ /* Generated by Frama-C */ +#include "errno.h" #include "pthread.h" #include "sched.h" #include "signal.h" @@ -10,21 +11,36 @@ char *__gen_e_acsl_literal_string; extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict; -/*@ requires valid_file_name: valid_read_string(file_name); +/*@ requires + valid_file_name_or_null: + file_name == \null || valid_read_string(file_name); requires resolved_name_null_or_allocated: resolved_name == \null || \valid(resolved_name + (0 .. 4096 - 1)); - assigns __fc_heap_status, \result, *(resolved_name + (0 .. 4096 - 1)); + assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)), + *(resolved_name + (0 .. 4096 - 1)), __fc_errno; assigns __fc_heap_status \from (indirect: resolved_name), __fc_heap_status; - assigns \result + assigns *(\result + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); + assigns __fc_errno + \from (indirect: file_name), (indirect: *(file_name + (0 ..))), + (indirect: resolved_name), (indirect: __fc_heap_status); + + behavior null_file_name: + assumes null_file_name: file_name == \null; + ensures null_result: \result == \null; + ensures errno_set: __fc_errno == 22; + assigns \result, __fc_errno; + assigns \result \from (indirect: file_name); + assigns __fc_errno \from (indirect: file_name); behavior allocate_resolved_name: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; assumes can_allocate: is_allocable(4096); ensures allocation: \fresh{Old, Here}(\result,4096); @@ -33,42 +49,73 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict; assigns \result \from (indirect: __fc_heap_status); behavior not_enough_memory: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; + assumes cannot_allocate: !is_allocable(4096); ensures null_result: \result == \null; + ensures errno_set: __fc_errno == 12; assigns \result; assigns \result \from \nothing; allocates \nothing; behavior resolved_name_buffer: + assumes valid_file_name: valid_read_string(file_name); assumes allocated_resolved_name_or_fail: \valid(resolved_name + (0 .. 4096 - 1)); - ensures valid_string_resolved_name: valid_string(\old(resolved_name)); + ensures + valid_string_resolved_name: + valid_string(\old(resolved_name)) && + strlen(\old(resolved_name)) < 4096; ensures resolved_result: \result == \old(resolved_name); assigns \result, *(resolved_name + (0 .. 4096 - 1)); - assigns \result \from \nothing; + assigns \result \from resolved_name; assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: *(file_name + (0 ..))); allocates \nothing; + + behavior filesystem_error: + assumes valid_file_name: valid_read_string(file_name); + ensures null_result: \result == \null; + ensures errno_set: __fc_errno \in {13, 5, 40, 36, 2, 20}; + assigns \result, __fc_errno; + assigns \result \from (indirect: *(file_name + (0 ..))); + assigns __fc_errno \from (indirect: *(file_name + (0 ..))); + allocates \nothing; */ char *__gen_e_acsl_realpath(char const * restrict file_name, char * restrict resolved_name); -/*@ requires valid_file_name: valid_read_string(file_name); +/*@ requires + valid_file_name_or_null: + file_name == \null || valid_read_string(file_name); requires resolved_name_null_or_allocated: resolved_name == \null || \valid(resolved_name + (0 .. 4096 - 1)); - assigns __fc_heap_status, \result, *(resolved_name + (0 .. 4096 - 1)); + assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)), + *(resolved_name + (0 .. 4096 - 1)), __fc_errno; assigns __fc_heap_status \from (indirect: resolved_name), __fc_heap_status; - assigns \result + assigns *(\result + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); + assigns __fc_errno + \from (indirect: file_name), (indirect: *(file_name + (0 ..))), + (indirect: resolved_name), (indirect: __fc_heap_status); + + behavior null_file_name: + assumes null_file_name: file_name == \null; + ensures null_result: \result == \null; + ensures errno_set: __fc_errno == 22; + assigns \result, __fc_errno; + assigns \result \from (indirect: file_name); + assigns __fc_errno \from (indirect: file_name); behavior allocate_resolved_name: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; assumes can_allocate: is_allocable(4096); ensures allocation: \fresh{Old, Here}(\result,4096); @@ -77,23 +124,39 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, assigns \result \from (indirect: __fc_heap_status); behavior not_enough_memory: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; + assumes cannot_allocate: !is_allocable(4096); ensures null_result: \result == \null; + ensures errno_set: __fc_errno == 12; assigns \result; assigns \result \from \nothing; allocates \nothing; behavior resolved_name_buffer: + assumes valid_file_name: valid_read_string(file_name); assumes allocated_resolved_name_or_fail: \valid(resolved_name + (0 .. 4096 - 1)); - ensures valid_string_resolved_name: valid_string(\old(resolved_name)); + ensures + valid_string_resolved_name: + valid_string(\old(resolved_name)) && + strlen(\old(resolved_name)) < 4096; ensures resolved_result: \result == \old(resolved_name); assigns \result, *(resolved_name + (0 .. 4096 - 1)); - assigns \result \from \nothing; + assigns \result \from resolved_name; assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: *(file_name + (0 ..))); allocates \nothing; + + behavior filesystem_error: + assumes valid_file_name: valid_read_string(file_name); + ensures null_result: \result == \null; + ensures errno_set: __fc_errno \in {13, 5, 40, 36, 2, 20}; + assigns \result, __fc_errno; + assigns \result \from (indirect: *(file_name + (0 ..))); + assigns __fc_errno \from (indirect: *(file_name + (0 ..))); + allocates \nothing; */ char *__gen_e_acsl_realpath(char const * restrict file_name, char * restrict resolved_name) @@ -103,12 +166,9 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, char *__retres; { int __gen_e_acsl_or; - int __gen_e_acsl_size_2; - int __gen_e_acsl_if_2; - int __gen_e_acsl_valid_2; __e_acsl_store_block((void *)(& resolved_name),8UL); __gen_e_acsl_at = resolved_name; - __gen_e_acsl_contract = __e_acsl_contract_init(3UL); + __gen_e_acsl_contract = __e_acsl_contract_init(5UL); __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 = {.values = (void *)0}; __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2, @@ -145,41 +205,45 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, __gen_e_acsl_assert_data_2.pred_txt = "resolved_name == \\null || \\valid(resolved_name + (0 .. 4096 - 1))"; __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_2.fct = "realpath"; - __gen_e_acsl_assert_data_2.line = 757; + __gen_e_acsl_assert_data_2.line = 759; __gen_e_acsl_assert_data_2.name = "resolved_name_null_or_allocated"; __e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2); - __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,1UL, - resolved_name == (char *)0); - __gen_e_acsl_size_2 = 1 * (((4096 - 1) - 0) + 1); - if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0; - else __gen_e_acsl_if_2 = __gen_e_acsl_size_2; - __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(resolved_name + 1 * 0), - (size_t)__gen_e_acsl_if_2, - (void *)resolved_name, - (void *)(& resolved_name)); - __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,2UL, - __gen_e_acsl_valid_2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,0UL, + file_name == (char const *)0); } __retres = realpath(file_name,resolved_name); { int __gen_e_acsl_assumes_value; __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes - ((__e_acsl_contract_t const *)__gen_e_acsl_contract,1UL); + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,0UL); if (__gen_e_acsl_assumes_value) { - __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 = + __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 = {.values = (void *)0}; - __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"\\result", + __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"\\result", (void *)__retres); + __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 = + {.values = (void *)0}; + __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"__fc_errno", + 0,errno); __gen_e_acsl_assert_data_4.blocking = 1; __gen_e_acsl_assert_data_4.kind = "Postcondition"; - __gen_e_acsl_assert_data_4.pred_txt = "\\result == \\null"; + __gen_e_acsl_assert_data_4.pred_txt = "__fc_errno == 22"; __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_4.fct = "realpath"; - __gen_e_acsl_assert_data_4.line = 771; - __gen_e_acsl_assert_data_4.name = "not_enough_memory/null_result"; - __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_4); + __gen_e_acsl_assert_data_4.line = 770; + __gen_e_acsl_assert_data_4.name = "null_file_name/errno_set"; + __e_acsl_assert(errno == 22,& __gen_e_acsl_assert_data_4); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4); + __gen_e_acsl_assert_data_3.blocking = 1; + __gen_e_acsl_assert_data_3.kind = "Postcondition"; + __gen_e_acsl_assert_data_3.pred_txt = "\\result == \\null"; + __gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/stdlib.h"; + __gen_e_acsl_assert_data_3.fct = "realpath"; + __gen_e_acsl_assert_data_3.line = 769; + __gen_e_acsl_assert_data_3.name = "null_file_name/null_result"; + __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_3); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3); } __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes ((__e_acsl_contract_t const *)__gen_e_acsl_contract,2UL); @@ -188,20 +252,67 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, {.values = (void *)0}; __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\result", (void *)__retres); - __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6, - "\\old(resolved_name)", - (void *)__gen_e_acsl_at); + __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 = + {.values = (void *)0}; + __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"__fc_errno", + 0,errno); + __gen_e_acsl_assert_data_7.blocking = 1; + __gen_e_acsl_assert_data_7.kind = "Postcondition"; + __gen_e_acsl_assert_data_7.pred_txt = "__fc_errno == 12"; + __gen_e_acsl_assert_data_7.file = "FRAMAC_SHARE/libc/stdlib.h"; + __gen_e_acsl_assert_data_7.fct = "realpath"; + __gen_e_acsl_assert_data_7.line = 785; + __gen_e_acsl_assert_data_7.name = "not_enough_memory/errno_set"; + __e_acsl_assert(errno == 12,& __gen_e_acsl_assert_data_7); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7); __gen_e_acsl_assert_data_6.blocking = 1; __gen_e_acsl_assert_data_6.kind = "Postcondition"; - __gen_e_acsl_assert_data_6.pred_txt = "\\result == \\old(resolved_name)"; + __gen_e_acsl_assert_data_6.pred_txt = "\\result == \\null"; __gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_6.fct = "realpath"; - __gen_e_acsl_assert_data_6.line = 780; - __gen_e_acsl_assert_data_6.name = "resolved_name_buffer/resolved_result"; - __e_acsl_assert(__retres == __gen_e_acsl_at, - & __gen_e_acsl_assert_data_6); + __gen_e_acsl_assert_data_6.line = 784; + __gen_e_acsl_assert_data_6.name = "not_enough_memory/null_result"; + __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_6); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6); } + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,3UL); + if (__gen_e_acsl_assumes_value) { + __e_acsl_assert_data_t __gen_e_acsl_assert_data_9 = + {.values = (void *)0}; + __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,"\\result", + (void *)__retres); + __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9, + "\\old(resolved_name)", + (void *)__gen_e_acsl_at); + __gen_e_acsl_assert_data_9.blocking = 1; + __gen_e_acsl_assert_data_9.kind = "Postcondition"; + __gen_e_acsl_assert_data_9.pred_txt = "\\result == \\old(resolved_name)"; + __gen_e_acsl_assert_data_9.file = "FRAMAC_SHARE/libc/stdlib.h"; + __gen_e_acsl_assert_data_9.fct = "realpath"; + __gen_e_acsl_assert_data_9.line = 796; + __gen_e_acsl_assert_data_9.name = "resolved_name_buffer/resolved_result"; + __e_acsl_assert(__retres == __gen_e_acsl_at, + & __gen_e_acsl_assert_data_9); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data_9); + } + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,4UL); + if (__gen_e_acsl_assumes_value) { + __e_acsl_assert_data_t __gen_e_acsl_assert_data_10 = + {.values = (void *)0}; + __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_10,"\\result", + (void *)__retres); + __gen_e_acsl_assert_data_10.blocking = 1; + __gen_e_acsl_assert_data_10.kind = "Postcondition"; + __gen_e_acsl_assert_data_10.pred_txt = "\\result == \\null"; + __gen_e_acsl_assert_data_10.file = "FRAMAC_SHARE/libc/stdlib.h"; + __gen_e_acsl_assert_data_10.fct = "realpath"; + __gen_e_acsl_assert_data_10.line = 802; + __gen_e_acsl_assert_data_10.name = "filesystem_error/null_result"; + __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_10); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data_10); + } __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& resolved_name)); return __retres; diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c index 80828f9f5afaa54947cae451071a92de3f411b81..90b363e3678824a5f951d60b97bfc3945c84f774 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c +++ b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c @@ -420,7 +420,7 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size) __gen_e_acsl_assert_data.pred_txt = "\\valid(memptr)"; __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data.fct = "posix_memalign"; - __gen_e_acsl_assert_data.line = 701; + __gen_e_acsl_assert_data.line = 702; __gen_e_acsl_assert_data.name = "valid_memptr"; __e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data); __e_acsl_assert_clean(& __gen_e_acsl_assert_data); @@ -463,7 +463,7 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size) __gen_e_acsl_assert_data_2.pred_txt = "alignment >= sizeof(void *) &&\n((size_t)alignment & (size_t)alignment - 1) == 0"; __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_2.fct = "posix_memalign"; - __gen_e_acsl_assert_data_2.line = 703; + __gen_e_acsl_assert_data_2.line = 704; __gen_e_acsl_assert_data_2.name = "alignment_is_a_suitable_power_of_two"; __e_acsl_assert(__gen_e_acsl_and,& __gen_e_acsl_assert_data_2); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2); @@ -483,7 +483,7 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size) __gen_e_acsl_assert_data_4.pred_txt = "\\result == 0"; __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_4.fct = "posix_memalign"; - __gen_e_acsl_assert_data_4.line = 715; + __gen_e_acsl_assert_data_4.line = 716; __gen_e_acsl_assert_data_4.name = "allocation/result_zero"; __e_acsl_assert(__retres == 0,& __gen_e_acsl_assert_data_4); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4); @@ -507,7 +507,7 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size) __gen_e_acsl_assert_data_5.pred_txt = "\\result < 0 || \\result > 0"; __gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_5.fct = "posix_memalign"; - __gen_e_acsl_assert_data_5.line = 720; + __gen_e_acsl_assert_data_5.line = 721; __gen_e_acsl_assert_data_5.name = "no_allocation/result_non_zero"; __e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_5); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5); diff --git a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle index 526a044a5396eadfa3b42bcd4615a8471722b8a9..25a8a53eceb1175fbdd93ff8adfd73b6b9b8258b 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle @@ -2,36 +2,59 @@ [e-acsl] Warning: annotating undefined function `realpath': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning: - E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:755: Warning: + E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:757: Warning: no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported [e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:763: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:772: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:779: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:787: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:799: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:755: Warning: Some assumes clauses could not be translated. Ignoring complete and disjoint behaviors annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:755: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:770: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:766: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:777: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:766: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:777: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:771: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:785: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:777: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:792: Warning: no assigns clause generated for function valid_string because pointers as arguments is not yet supported [e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:796: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:804: Warning: + E-ACSL construct + `logic functions or predicates with no definition nor reads clause' + is not yet supported. + Ignoring annotation. [e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle index ee68e8606cdbd0d90a5f6ca011b556bb39421112..4dc9a20ea6aabb658451aaacf8020393e60b10cf 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle @@ -2,25 +2,25 @@ [e-acsl] Warning: annotating undefined function `posix_memalign': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:700: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:701: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:710: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:711: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:717: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:718: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:700: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:701: Warning: Some assumes clauses could not be translated. Ignoring complete and disjoint behaviors annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:700: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:701: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:714: Warning: - E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:715: Warning: + E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:716: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle index 4cd231d4748e3c00c565b704f2f4ecfa77f46068..e608985d5a008400c7eaec279bd9bf175a8d87d2 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle @@ -14,7 +14,7 @@ [eva] memsize.c:25: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:26: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva] FRAMAC_SHARE/libc/stdlib.h:452: Warning: +[eva] FRAMAC_SHARE/libc/stdlib.h:453: Warning: no 'assigns \result \from ...' clause specified for function realloc [eva] memsize.c:29: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:29: Warning: @@ -42,7 +42,7 @@ function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] memsize.c:52: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva] FRAMAC_SHARE/libc/stdlib.h:385: Warning: +[eva] FRAMAC_SHARE/libc/stdlib.h:386: Warning: no 'assigns \result \from ...' clause specified for function calloc [eva] memsize.c:55: Warning: ignoring unsupported allocates clause [eva:alarm] memsize.c:56: Warning: diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c index acadb73bba26a21210b64d9504f1754320a20677..ede92c3c70c3c7822255a83be2ea29009cc1d2cf 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c +++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c @@ -1,4 +1,5 @@ /* Generated by Frama-C */ +#include "errno.h" #include "pthread.h" #include "sched.h" #include "signal.h" @@ -10,21 +11,36 @@ char *__gen_e_acsl_literal_string; extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict; -/*@ requires valid_file_name: valid_read_string(file_name); +/*@ requires + valid_file_name_or_null: + file_name == \null || valid_read_string(file_name); requires resolved_name_null_or_allocated: resolved_name == \null || \valid(resolved_name + (0 .. 4096 - 1)); - assigns __fc_heap_status, \result, *(resolved_name + (0 .. 4096 - 1)); + assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)), + *(resolved_name + (0 .. 4096 - 1)), __fc_errno; assigns __fc_heap_status \from (indirect: resolved_name), __fc_heap_status; - assigns \result + assigns *(\result + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); + assigns __fc_errno + \from (indirect: file_name), (indirect: *(file_name + (0 ..))), + (indirect: resolved_name), (indirect: __fc_heap_status); + + behavior null_file_name: + assumes null_file_name: file_name == \null; + ensures null_result: \result == \null; + ensures errno_set: __fc_errno == 22; + assigns \result, __fc_errno; + assigns \result \from (indirect: file_name); + assigns __fc_errno \from (indirect: file_name); behavior allocate_resolved_name: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; assumes can_allocate: is_allocable(4096); ensures allocation: \fresh{Old, Here}(\result,4096); @@ -33,42 +49,73 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict; assigns \result \from (indirect: __fc_heap_status); behavior not_enough_memory: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; + assumes cannot_allocate: !is_allocable(4096); ensures null_result: \result == \null; + ensures errno_set: __fc_errno == 12; assigns \result; assigns \result \from \nothing; allocates \nothing; behavior resolved_name_buffer: + assumes valid_file_name: valid_read_string(file_name); assumes allocated_resolved_name_or_fail: \valid(resolved_name + (0 .. 4096 - 1)); - ensures valid_string_resolved_name: valid_string(\old(resolved_name)); + ensures + valid_string_resolved_name: + valid_string(\old(resolved_name)) && + strlen(\old(resolved_name)) < 4096; ensures resolved_result: \result == \old(resolved_name); assigns \result, *(resolved_name + (0 .. 4096 - 1)); - assigns \result \from \nothing; + assigns \result \from resolved_name; assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: *(file_name + (0 ..))); allocates \nothing; + + behavior filesystem_error: + assumes valid_file_name: valid_read_string(file_name); + ensures null_result: \result == \null; + ensures errno_set: __fc_errno \in {13, 5, 40, 36, 2, 20}; + assigns \result, __fc_errno; + assigns \result \from (indirect: *(file_name + (0 ..))); + assigns __fc_errno \from (indirect: *(file_name + (0 ..))); + allocates \nothing; */ char *__gen_e_acsl_realpath(char const * restrict file_name, char * restrict resolved_name); -/*@ requires valid_file_name: valid_read_string(file_name); +/*@ requires + valid_file_name_or_null: + file_name == \null || valid_read_string(file_name); requires resolved_name_null_or_allocated: resolved_name == \null || \valid(resolved_name + (0 .. 4096 - 1)); - assigns __fc_heap_status, \result, *(resolved_name + (0 .. 4096 - 1)); + assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)), + *(resolved_name + (0 .. 4096 - 1)), __fc_errno; assigns __fc_heap_status \from (indirect: resolved_name), __fc_heap_status; - assigns \result + assigns *(\result + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); + assigns __fc_errno + \from (indirect: file_name), (indirect: *(file_name + (0 ..))), + (indirect: resolved_name), (indirect: __fc_heap_status); + + behavior null_file_name: + assumes null_file_name: file_name == \null; + ensures null_result: \result == \null; + ensures errno_set: __fc_errno == 22; + assigns \result, __fc_errno; + assigns \result \from (indirect: file_name); + assigns __fc_errno \from (indirect: file_name); behavior allocate_resolved_name: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; assumes can_allocate: is_allocable(4096); ensures allocation: \fresh{Old, Here}(\result,4096); @@ -77,23 +124,39 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, assigns \result \from (indirect: __fc_heap_status); behavior not_enough_memory: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name == \null; + assumes cannot_allocate: !is_allocable(4096); ensures null_result: \result == \null; + ensures errno_set: __fc_errno == 12; assigns \result; assigns \result \from \nothing; allocates \nothing; behavior resolved_name_buffer: + assumes valid_file_name: valid_read_string(file_name); assumes allocated_resolved_name_or_fail: \valid(resolved_name + (0 .. 4096 - 1)); - ensures valid_string_resolved_name: valid_string(\old(resolved_name)); + ensures + valid_string_resolved_name: + valid_string(\old(resolved_name)) && + strlen(\old(resolved_name)) < 4096; ensures resolved_result: \result == \old(resolved_name); assigns \result, *(resolved_name + (0 .. 4096 - 1)); - assigns \result \from \nothing; + assigns \result \from resolved_name; assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: *(file_name + (0 ..))); allocates \nothing; + + behavior filesystem_error: + assumes valid_file_name: valid_read_string(file_name); + ensures null_result: \result == \null; + ensures errno_set: __fc_errno \in {13, 5, 40, 36, 2, 20}; + assigns \result, __fc_errno; + assigns \result \from (indirect: *(file_name + (0 ..))); + assigns __fc_errno \from (indirect: *(file_name + (0 ..))); + allocates \nothing; */ char *__gen_e_acsl_realpath(char const * restrict file_name, char * restrict resolved_name) @@ -104,13 +167,10 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, __e_acsl_store_block((void *)(& __retres),8UL); { int __gen_e_acsl_or; - int __gen_e_acsl_size_2; - int __gen_e_acsl_if_2; - int __gen_e_acsl_valid_2; __e_acsl_store_block((void *)(& resolved_name),8UL); __e_acsl_temporal_pull_parameter((void *)(& resolved_name),1U,8UL); __gen_e_acsl_at = resolved_name; - __gen_e_acsl_contract = __e_acsl_contract_init(3UL); + __gen_e_acsl_contract = __e_acsl_contract_init(5UL); __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 = {.values = (void *)0}; __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2, @@ -147,21 +207,12 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, __gen_e_acsl_assert_data_2.pred_txt = "resolved_name == \\null || \\valid(resolved_name + (0 .. 4096 - 1))"; __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_2.fct = "realpath"; - __gen_e_acsl_assert_data_2.line = 757; + __gen_e_acsl_assert_data_2.line = 759; __gen_e_acsl_assert_data_2.name = "resolved_name_null_or_allocated"; __e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2); - __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,1UL, - resolved_name == (char *)0); - __gen_e_acsl_size_2 = 1 * (((4096 - 1) - 0) + 1); - if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0; - else __gen_e_acsl_if_2 = __gen_e_acsl_size_2; - __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(resolved_name + 1 * 0), - (size_t)__gen_e_acsl_if_2, - (void *)resolved_name, - (void *)(& resolved_name)); - __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,2UL, - __gen_e_acsl_valid_2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,0UL, + file_name == (char const *)0); __e_acsl_temporal_reset_parameters(); __e_acsl_temporal_reset_return(); __e_acsl_temporal_save_nreferent_parameter((void *)(& resolved_name),1U); @@ -172,21 +223,34 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, int __gen_e_acsl_assumes_value; __e_acsl_temporal_save_return((void *)(& __retres)); __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes - ((__e_acsl_contract_t const *)__gen_e_acsl_contract,1UL); + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,0UL); if (__gen_e_acsl_assumes_value) { - __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 = + __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 = {.values = (void *)0}; - __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"\\result", + __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"\\result", (void *)__retres); + __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 = + {.values = (void *)0}; + __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"__fc_errno", + 0,errno); __gen_e_acsl_assert_data_4.blocking = 1; __gen_e_acsl_assert_data_4.kind = "Postcondition"; - __gen_e_acsl_assert_data_4.pred_txt = "\\result == \\null"; + __gen_e_acsl_assert_data_4.pred_txt = "__fc_errno == 22"; __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_4.fct = "realpath"; - __gen_e_acsl_assert_data_4.line = 771; - __gen_e_acsl_assert_data_4.name = "not_enough_memory/null_result"; - __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_4); + __gen_e_acsl_assert_data_4.line = 770; + __gen_e_acsl_assert_data_4.name = "null_file_name/errno_set"; + __e_acsl_assert(errno == 22,& __gen_e_acsl_assert_data_4); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4); + __gen_e_acsl_assert_data_3.blocking = 1; + __gen_e_acsl_assert_data_3.kind = "Postcondition"; + __gen_e_acsl_assert_data_3.pred_txt = "\\result == \\null"; + __gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/stdlib.h"; + __gen_e_acsl_assert_data_3.fct = "realpath"; + __gen_e_acsl_assert_data_3.line = 769; + __gen_e_acsl_assert_data_3.name = "null_file_name/null_result"; + __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_3); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3); } __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes ((__e_acsl_contract_t const *)__gen_e_acsl_contract,2UL); @@ -195,20 +259,67 @@ char *__gen_e_acsl_realpath(char const * restrict file_name, {.values = (void *)0}; __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\result", (void *)__retres); - __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6, - "\\old(resolved_name)", - (void *)__gen_e_acsl_at); + __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 = + {.values = (void *)0}; + __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"__fc_errno", + 0,errno); + __gen_e_acsl_assert_data_7.blocking = 1; + __gen_e_acsl_assert_data_7.kind = "Postcondition"; + __gen_e_acsl_assert_data_7.pred_txt = "__fc_errno == 12"; + __gen_e_acsl_assert_data_7.file = "FRAMAC_SHARE/libc/stdlib.h"; + __gen_e_acsl_assert_data_7.fct = "realpath"; + __gen_e_acsl_assert_data_7.line = 785; + __gen_e_acsl_assert_data_7.name = "not_enough_memory/errno_set"; + __e_acsl_assert(errno == 12,& __gen_e_acsl_assert_data_7); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7); __gen_e_acsl_assert_data_6.blocking = 1; __gen_e_acsl_assert_data_6.kind = "Postcondition"; - __gen_e_acsl_assert_data_6.pred_txt = "\\result == \\old(resolved_name)"; + __gen_e_acsl_assert_data_6.pred_txt = "\\result == \\null"; __gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_6.fct = "realpath"; - __gen_e_acsl_assert_data_6.line = 780; - __gen_e_acsl_assert_data_6.name = "resolved_name_buffer/resolved_result"; - __e_acsl_assert(__retres == __gen_e_acsl_at, - & __gen_e_acsl_assert_data_6); + __gen_e_acsl_assert_data_6.line = 784; + __gen_e_acsl_assert_data_6.name = "not_enough_memory/null_result"; + __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_6); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6); } + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,3UL); + if (__gen_e_acsl_assumes_value) { + __e_acsl_assert_data_t __gen_e_acsl_assert_data_9 = + {.values = (void *)0}; + __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9,"\\result", + (void *)__retres); + __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_9, + "\\old(resolved_name)", + (void *)__gen_e_acsl_at); + __gen_e_acsl_assert_data_9.blocking = 1; + __gen_e_acsl_assert_data_9.kind = "Postcondition"; + __gen_e_acsl_assert_data_9.pred_txt = "\\result == \\old(resolved_name)"; + __gen_e_acsl_assert_data_9.file = "FRAMAC_SHARE/libc/stdlib.h"; + __gen_e_acsl_assert_data_9.fct = "realpath"; + __gen_e_acsl_assert_data_9.line = 796; + __gen_e_acsl_assert_data_9.name = "resolved_name_buffer/resolved_result"; + __e_acsl_assert(__retres == __gen_e_acsl_at, + & __gen_e_acsl_assert_data_9); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data_9); + } + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,4UL); + if (__gen_e_acsl_assumes_value) { + __e_acsl_assert_data_t __gen_e_acsl_assert_data_10 = + {.values = (void *)0}; + __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_10,"\\result", + (void *)__retres); + __gen_e_acsl_assert_data_10.blocking = 1; + __gen_e_acsl_assert_data_10.kind = "Postcondition"; + __gen_e_acsl_assert_data_10.pred_txt = "\\result == \\null"; + __gen_e_acsl_assert_data_10.file = "FRAMAC_SHARE/libc/stdlib.h"; + __gen_e_acsl_assert_data_10.fct = "realpath"; + __gen_e_acsl_assert_data_10.line = 802; + __gen_e_acsl_assert_data_10.name = "filesystem_error/null_result"; + __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_10); + __e_acsl_assert_clean(& __gen_e_acsl_assert_data_10); + } __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& resolved_name)); __e_acsl_delete_block((void *)(& __retres)); diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c index 443d067b6350173cf948f99e755e8a72f3d50244..a95cdb0ed93f608bc404277e283b3411d1d8b3db 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c +++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c @@ -57,7 +57,7 @@ char *__gen_e_acsl_getenv(char const *name) __gen_e_acsl_assert_data_2.pred_txt = "\\result == \\null || \\valid(\\result)"; __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h"; __gen_e_acsl_assert_data_2.fct = "getenv"; - __gen_e_acsl_assert_data_2.line = 523; + __gen_e_acsl_assert_data_2.line = 524; __gen_e_acsl_assert_data_2.name = "null_or_valid_result"; __e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2); __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2); diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle index fec515bf84577c12e67a8a715429edcf18ae53e9..014073a4bba894b34d813b8db4b56715fbb9f203 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle @@ -2,38 +2,61 @@ [e-acsl] Warning: annotating undefined function `realpath': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning: - E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:755: Warning: + E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:757: Warning: no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported [e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:763: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:772: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:779: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:787: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:799: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:755: Warning: Some assumes clauses could not be translated. Ignoring complete and disjoint behaviors annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:755: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:770: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:766: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:777: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:766: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:777: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:771: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:785: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:777: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:792: Warning: no assigns clause generated for function valid_string because pointers as arguments is not yet supported [e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:796: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:804: Warning: + E-ACSL construct + `logic functions or predicates with no definition nor reads clause' + is not yet supported. + Ignoring annotation. [e-acsl] translation done in project "e-acsl". [eva:alarm] t_fun_lib.c:15: Warning: function __e_acsl_assert_register_ulong: precondition data->values == \null || diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle index 1c9dd482c25fd5d5c7013fb3714d6bc6e97cca56..512e712c13d305d6a7a8a8d3aa316915f3246491 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle @@ -2,28 +2,28 @@ [e-acsl] Warning: annotating undefined function `getenv': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:521: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:522: Warning: no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported [e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: E-ACSL construct `logic functions or predicates performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:520: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:521: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:524: Warning: function __e_acsl_assert_register_ptr: precondition data->values == \null || \valid(data->values) got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:524: Warning: function __e_acsl_assert_register_ulong: precondition data->values == \null || \valid(data->values) got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:524: Warning: function __e_acsl_assert_register_int: precondition data->values == \null || \valid(data->values) got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:524: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:523: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:524: Warning: function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown. [eva:alarm] t_getenv.c:13: Warning: function __e_acsl_assert_register_ptr: precondition data->values == \null || diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle index b58973f347f3f02d2cc4ed7318a0cf053462a6cb..aa120142ee298c93689ee34a53c6b4b52052b9b4 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle @@ -2,6 +2,7 @@ [instantiate] calloc.c:24: Warning: calloc instantiator cannot replace call [instantiate] calloc.c:25: Warning: calloc instantiator cannot replace call /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct X { int x ; @@ -316,6 +317,7 @@ int main(void) [kernel] Parsing ocode_calloc.c (with preprocessing) /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct X { int x ; diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle index 59f9e2b69776a0f7d70ea782149f214b64b420c1..01bdb24dbef3c573e554bea6efd032b0133fc8b4 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle @@ -1,6 +1,7 @@ [kernel] Parsing free.c (with preprocessing) [instantiate] free.c:13: Warning: free instantiator cannot replace call /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct incomplete; /*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr); @@ -140,6 +141,7 @@ void with_incomplete(struct incomplete *t) [kernel] Parsing ocode_free.c (with preprocessing) /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct incomplete; /*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr); diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle index e5d86f16bdbba2458bff1b57ac6f3c99c5c34019..86dc9d7413f9207e05a238bbcc452cb69155b027 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle @@ -2,6 +2,7 @@ [instantiate] malloc.c:23: Warning: malloc instantiator cannot replace call [instantiate] malloc.c:24: Warning: malloc instantiator cannot replace call /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct X { int x ; @@ -218,6 +219,7 @@ int main(void) [kernel] Parsing ocode_malloc.c (with preprocessing) /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct X { int x ; 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 c09cffbaa62838196db4cbd474d3908ac11046bc..a27314ede4be1426fc5be86f8a50f6f819a44706 100644 --- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif +++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif @@ -4442,9 +4442,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 516, + "startLine": 517, "startColumn": 12, - "endLine": 516, + "endLine": 517, "endColumn": 17, "byteLength": 5 } @@ -4465,9 +4465,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 514, + "startLine": 515, "startColumn": 28, - "endLine": 514, + "endLine": 515, "endColumn": 34, "byteLength": 6 } @@ -4488,9 +4488,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 516, + "startLine": 517, "startColumn": 12, - "endLine": 516, + "endLine": 517, "endColumn": 17, "byteLength": 5 } @@ -4511,9 +4511,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 497, + "startLine": 498, "startColumn": 12, - "endLine": 497, + "endLine": 498, "endColumn": 17, "byteLength": 5 } @@ -4534,9 +4534,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 494, + "startLine": 495, "startColumn": 16, - "endLine": 494, + "endLine": 495, "endColumn": 33, "byteLength": 17 } @@ -4557,9 +4557,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 495, + "startLine": 496, "startColumn": 28, - "endLine": 495, + "endLine": 496, "endColumn": 34, "byteLength": 6 } @@ -4580,9 +4580,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 493, + "startLine": 494, "startColumn": 10, - "endLine": 493, + "endLine": 494, "endColumn": 22, "byteLength": 12 } @@ -4605,9 +4605,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 493, + "startLine": 494, "startColumn": 10, - "endLine": 493, + "endLine": 494, "endColumn": 22, "byteLength": 12 } @@ -4628,9 +4628,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 610, + "startLine": 611, "startColumn": 11, - "endLine": 610, + "endLine": 611, "endColumn": 14, "byteLength": 3 } @@ -4651,9 +4651,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 610, + "startLine": 611, "startColumn": 11, - "endLine": 610, + "endLine": 611, "endColumn": 14, "byteLength": 3 } @@ -4674,9 +4674,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 610, + "startLine": 611, "startColumn": 11, - "endLine": 610, + "endLine": 611, "endColumn": 14, "byteLength": 3 } @@ -4697,9 +4697,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 599, + "startLine": 600, "startColumn": 30, - "endLine": 599, + "endLine": 600, "endColumn": 51, "byteLength": 21 } @@ -4720,9 +4720,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 602, + "startLine": 603, "startColumn": 22, - "endLine": 602, + "endLine": 603, "endColumn": 27, "byteLength": 5 } @@ -4743,9 +4743,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 605, + "startLine": 606, "startColumn": 25, - "endLine": 605, + "endLine": 606, "endColumn": 31, "byteLength": 6 } @@ -4766,9 +4766,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 603, + "startLine": 604, "startColumn": 29, - "endLine": 603, + "endLine": 604, "endColumn": 42, "byteLength": 13 } @@ -4789,9 +4789,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 606, + "startLine": 607, "startColumn": 25, - "endLine": 606, + "endLine": 607, "endColumn": 37, "byteLength": 12 } @@ -4812,9 +4812,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 610, + "startLine": 611, "startColumn": 11, - "endLine": 610, + "endLine": 611, "endColumn": 14, "byteLength": 3 } @@ -4837,9 +4837,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 600, + "startLine": 601, "startColumn": 10, - "endLine": 600, + "endLine": 601, "endColumn": 17, "byteLength": 7 } @@ -4860,9 +4860,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 610, + "startLine": 611, "startColumn": 11, - "endLine": 610, + "endLine": 611, "endColumn": 14, "byteLength": 3 } @@ -4883,9 +4883,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 610, + "startLine": 611, "startColumn": 11, - "endLine": 610, + "endLine": 611, "endColumn": 14, "byteLength": 3 } @@ -4908,9 +4908,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 503, + "startLine": 504, "startColumn": 11, - "endLine": 503, + "endLine": 504, "endColumn": 24, "byteLength": 13 } @@ -4931,9 +4931,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 503, + "startLine": 504, "startColumn": 11, - "endLine": 503, + "endLine": 504, "endColumn": 24, "byteLength": 13 } @@ -4956,9 +4956,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 502, + "startLine": 503, "startColumn": 12, - "endLine": 502, + "endLine": 503, "endColumn": 19, "byteLength": 7 } @@ -4979,9 +4979,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 500, + "startLine": 501, "startColumn": 11, - "endLine": 500, + "endLine": 501, "endColumn": 17, "byteLength": 6 } @@ -5002,9 +5002,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 500, + "startLine": 501, "startColumn": 11, - "endLine": 500, + "endLine": 501, "endColumn": 17, "byteLength": 6 } @@ -5027,9 +5027,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 499, + "startLine": 500, "startColumn": 12, - "endLine": 499, + "endLine": 500, "endColumn": 19, "byteLength": 7 } @@ -5050,9 +5050,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 75, + "startLine": 76, "startColumn": 14, - "endLine": 75, + "endLine": 76, "endColumn": 18, "byteLength": 4 } @@ -5073,9 +5073,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 72, + "startLine": 73, "startColumn": 23, - "endLine": 72, + "endLine": 73, "endColumn": 40, "byteLength": 17 } @@ -5096,9 +5096,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 75, + "startLine": 76, "startColumn": 14, - "endLine": 75, + "endLine": 76, "endColumn": 18, "byteLength": 4 } @@ -5121,9 +5121,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 73, + "startLine": 74, "startColumn": 10, - "endLine": 73, + "endLine": 74, "endColumn": 17, "byteLength": 7 } @@ -5144,9 +5144,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 81, + "startLine": 82, "startColumn": 11, - "endLine": 81, + "endLine": 82, "endColumn": 15, "byteLength": 4 } @@ -5167,9 +5167,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 78, + "startLine": 79, "startColumn": 23, - "endLine": 78, + "endLine": 79, "endColumn": 40, "byteLength": 17 } @@ -5190,9 +5190,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 81, + "startLine": 82, "startColumn": 11, - "endLine": 81, + "endLine": 82, "endColumn": 15, "byteLength": 4 } @@ -5215,9 +5215,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 79, + "startLine": 80, "startColumn": 10, - "endLine": 79, + "endLine": 80, "endColumn": 17, "byteLength": 7 } @@ -5238,9 +5238,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 87, + "startLine": 88, "startColumn": 16, - "endLine": 87, + "endLine": 88, "endColumn": 20, "byteLength": 4 } @@ -5261,9 +5261,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 84, + "startLine": 85, "startColumn": 23, - "endLine": 84, + "endLine": 85, "endColumn": 40, "byteLength": 17 } @@ -5284,9 +5284,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 87, + "startLine": 88, "startColumn": 16, - "endLine": 87, + "endLine": 88, "endColumn": 20, "byteLength": 4 } @@ -5309,9 +5309,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 85, + "startLine": 86, "startColumn": 10, - "endLine": 85, + "endLine": 86, "endColumn": 17, "byteLength": 7 } @@ -5332,9 +5332,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 93, + "startLine": 94, "startColumn": 21, - "endLine": 93, + "endLine": 94, "endColumn": 26, "byteLength": 5 } @@ -5355,9 +5355,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 90, + "startLine": 91, "startColumn": 23, - "endLine": 90, + "endLine": 91, "endColumn": 40, "byteLength": 17 } @@ -5378,9 +5378,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 93, + "startLine": 94, "startColumn": 21, - "endLine": 93, + "endLine": 94, "endColumn": 26, "byteLength": 5 } @@ -5403,9 +5403,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 91, + "startLine": 92, "startColumn": 10, - "endLine": 91, + "endLine": 92, "endColumn": 17, "byteLength": 7 } @@ -5426,9 +5426,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 582, + "startLine": 583, "startColumn": 12, - "endLine": 582, + "endLine": 583, "endColumn": 13, "byteLength": 1 } @@ -5449,9 +5449,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 575, + "startLine": 576, "startColumn": 34, - "endLine": 575, + "endLine": 576, "endColumn": 57, "byteLength": 23 } @@ -5472,9 +5472,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 579, + "startLine": 580, "startColumn": 34, - "endLine": 580, + "endLine": 581, "endColumn": 76, "byteLength": 96 } @@ -5495,9 +5495,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 582, + "startLine": 583, "startColumn": 12, - "endLine": 582, + "endLine": 583, "endColumn": 13, "byteLength": 1 } @@ -5520,9 +5520,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 576, + "startLine": 577, "startColumn": 10, - "endLine": 576, + "endLine": 577, "endColumn": 17, "byteLength": 7 } @@ -5683,9 +5683,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 386, "startColumn": 12, - "endLine": 385, + "endLine": 386, "endColumn": 13, "byteLength": 1 } @@ -5706,9 +5706,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 386, "startColumn": 12, - "endLine": 385, + "endLine": 386, "endColumn": 13, "byteLength": 1 } @@ -5729,9 +5729,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 386, "startColumn": 12, - "endLine": 385, + "endLine": 386, "endColumn": 13, "byteLength": 1 } @@ -5752,9 +5752,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 372, + "startLine": 373, "startColumn": 26, - "endLine": 372, + "endLine": 373, "endColumn": 52, "byteLength": 26 } @@ -5775,9 +5775,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 378, + "startLine": 379, "startColumn": 29, - "endLine": 378, + "endLine": 379, "endColumn": 56, "byteLength": 27 } @@ -5798,9 +5798,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 373, + "startLine": 374, "startColumn": 24, - "endLine": 373, + "endLine": 374, "endColumn": 53, "byteLength": 29 } @@ -5821,9 +5821,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 374, + "startLine": 375, "startColumn": 28, - "endLine": 374, + "endLine": 375, "endColumn": 77, "byteLength": 49 } @@ -5844,9 +5844,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 375, + "startLine": 376, "startColumn": 33, - "endLine": 375, + "endLine": 376, "endColumn": 81, "byteLength": 48 } @@ -5867,9 +5867,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 381, + "startLine": 382, "startColumn": 25, - "endLine": 381, + "endLine": 382, "endColumn": 41, "byteLength": 16 } @@ -5890,9 +5890,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 367, + "startLine": 368, "startColumn": 10, - "endLine": 367, + "endLine": 368, "endColumn": 26, "byteLength": 16 } @@ -5913,9 +5913,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 386, "startColumn": 12, - "endLine": 385, + "endLine": 386, "endColumn": 13, "byteLength": 1 } @@ -5938,9 +5938,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 367, + "startLine": 368, "startColumn": 10, - "endLine": 367, + "endLine": 368, "endColumn": 26, "byteLength": 16 } @@ -5963,9 +5963,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 368, + "startLine": 369, "startColumn": 10, - "endLine": 368, + "endLine": 369, "endColumn": 17, "byteLength": 7 } @@ -5988,9 +5988,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 379, + "startLine": 380, "startColumn": 12, - "endLine": 379, + "endLine": 380, "endColumn": 19, "byteLength": 7 } @@ -6011,9 +6011,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 366, + "startLine": 367, "startColumn": 12, - "endLine": 366, + "endLine": 367, "endColumn": 19, "byteLength": 7 } @@ -6034,9 +6034,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 386, "startColumn": 12, - "endLine": 385, + "endLine": 386, "endColumn": 13, "byteLength": 1 } @@ -6057,9 +6057,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 386, "startColumn": 12, - "endLine": 385, + "endLine": 386, "endColumn": 13, "byteLength": 1 } @@ -6080,9 +6080,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 385, + "startLine": 386, "startColumn": 12, - "endLine": 385, + "endLine": 386, "endColumn": 13, "byteLength": 1 } @@ -6103,9 +6103,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 641, + "startLine": 642, "startColumn": 13, - "endLine": 641, + "endLine": 642, "endColumn": 16, "byteLength": 3 } @@ -6126,9 +6126,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 641, + "startLine": 642, "startColumn": 13, - "endLine": 641, + "endLine": 642, "endColumn": 16, "byteLength": 3 } @@ -6151,9 +6151,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 640, + "startLine": 641, "startColumn": 12, - "endLine": 640, + "endLine": 641, "endColumn": 19, "byteLength": 7 } @@ -6174,9 +6174,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 322, + "startLine": 323, "startColumn": 14, - "endLine": 322, + "endLine": 323, "endColumn": 21, "byteLength": 7 } @@ -6197,9 +6197,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 317, + "startLine": 318, "startColumn": 33, - "endLine": 317, + "endLine": 318, "endColumn": 56, "byteLength": 23 } @@ -6220,9 +6220,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 320, + "startLine": 321, "startColumn": 24, - "endLine": 320, + "endLine": 321, "endColumn": 67, "byteLength": 43 } @@ -6243,9 +6243,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 318, + "startLine": 319, "startColumn": 10, - "endLine": 318, + "endLine": 319, "endColumn": 37, "byteLength": 27 } @@ -6268,9 +6268,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 318, + "startLine": 319, "startColumn": 10, - "endLine": 318, + "endLine": 319, "endColumn": 37, "byteLength": 27 } @@ -6293,9 +6293,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 319, + "startLine": 320, "startColumn": 10, - "endLine": 319, + "endLine": 320, "endColumn": 17, "byteLength": 7 } @@ -6316,9 +6316,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 330, + "startLine": 331, "startColumn": 14, - "endLine": 330, + "endLine": 331, "endColumn": 21, "byteLength": 7 } @@ -6339,9 +6339,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 325, + "startLine": 326, "startColumn": 45, - "endLine": 325, + "endLine": 326, "endColumn": 71, "byteLength": 26 } @@ -6362,9 +6362,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 328, + "startLine": 329, "startColumn": 24, - "endLine": 328, + "endLine": 329, "endColumn": 67, "byteLength": 43 } @@ -6385,9 +6385,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 326, + "startLine": 327, "startColumn": 10, - "endLine": 326, + "endLine": 327, "endColumn": 37, "byteLength": 27 } @@ -6410,9 +6410,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 326, + "startLine": 327, "startColumn": 10, - "endLine": 326, + "endLine": 327, "endColumn": 37, "byteLength": 27 } @@ -6435,9 +6435,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 327, + "startLine": 328, "startColumn": 10, - "endLine": 327, + "endLine": 328, "endColumn": 17, "byteLength": 7 } @@ -6458,9 +6458,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 510, + "startLine": 511, "startColumn": 12, - "endLine": 510, + "endLine": 511, "endColumn": 16, "byteLength": 4 } @@ -6481,9 +6481,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 507, + "startLine": 508, "startColumn": 16, - "endLine": 507, + "endLine": 508, "endColumn": 38, "byteLength": 22 } @@ -6504,9 +6504,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 508, + "startLine": 509, "startColumn": 28, - "endLine": 508, + "endLine": 509, "endColumn": 34, "byteLength": 6 } @@ -6527,9 +6527,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 506, + "startLine": 507, "startColumn": 10, - "endLine": 506, + "endLine": 507, "endColumn": 22, "byteLength": 12 } @@ -6552,9 +6552,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 506, + "startLine": 507, "startColumn": 10, - "endLine": 506, + "endLine": 507, "endColumn": 22, "byteLength": 12 } @@ -6575,9 +6575,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 419, + "startLine": 420, "startColumn": 12, - "endLine": 419, + "endLine": 420, "endColumn": 16, "byteLength": 4 } @@ -6598,9 +6598,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 419, + "startLine": 420, "startColumn": 12, - "endLine": 419, + "endLine": 420, "endColumn": 16, "byteLength": 4 } @@ -6621,9 +6621,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 419, + "startLine": 420, "startColumn": 12, - "endLine": 419, + "endLine": 420, "endColumn": 16, "byteLength": 4 } @@ -6644,9 +6644,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 405, + "startLine": 406, "startColumn": 23, - "endLine": 405, + "endLine": 406, "endColumn": 47, "byteLength": 24 } @@ -6667,9 +6667,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 409, + "startLine": 410, "startColumn": 23, - "endLine": 409, + "endLine": 410, "endColumn": 31, "byteLength": 8 } @@ -6690,9 +6690,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 413, + "startLine": 414, "startColumn": 20, - "endLine": 413, + "endLine": 414, "endColumn": 28, "byteLength": 8 } @@ -6713,9 +6713,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 411, + "startLine": 412, "startColumn": 19, - "endLine": 411, + "endLine": 412, "endColumn": 32, "byteLength": 13 } @@ -6736,9 +6736,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 410, + "startLine": 411, "startColumn": 12, - "endLine": 410, + "endLine": 411, "endColumn": 28, "byteLength": 16 } @@ -6759,9 +6759,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 407, + "startLine": 408, "startColumn": 12, - "endLine": 407, + "endLine": 408, "endColumn": 28, "byteLength": 16 } @@ -6782,9 +6782,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 419, + "startLine": 420, "startColumn": 12, - "endLine": 419, + "endLine": 420, "endColumn": 16, "byteLength": 4 } @@ -6807,9 +6807,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 410, + "startLine": 411, "startColumn": 12, - "endLine": 410, + "endLine": 411, "endColumn": 28, "byteLength": 16 } @@ -6832,9 +6832,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 407, + "startLine": 408, "startColumn": 12, - "endLine": 407, + "endLine": 408, "endColumn": 28, "byteLength": 16 } @@ -6855,9 +6855,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 406, + "startLine": 407, "startColumn": 10, - "endLine": 406, + "endLine": 407, "endColumn": 11, "byteLength": 1 } @@ -6878,9 +6878,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 419, + "startLine": 420, "startColumn": 12, - "endLine": 419, + "endLine": 420, "endColumn": 16, "byteLength": 4 } @@ -6901,9 +6901,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 419, + "startLine": 420, "startColumn": 12, - "endLine": 419, + "endLine": 420, "endColumn": 16, "byteLength": 4 } @@ -6924,9 +6924,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 419, + "startLine": 420, "startColumn": 12, - "endLine": 419, + "endLine": 420, "endColumn": 16, "byteLength": 4 } @@ -6947,9 +6947,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 525, + "startLine": 526, "startColumn": 12, - "endLine": 525, + "endLine": 526, "endColumn": 13, "byteLength": 1 } @@ -6970,9 +6970,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 521, + "startLine": 522, "startColumn": 23, - "endLine": 521, + "endLine": 522, "endColumn": 46, "byteLength": 23 } @@ -6993,9 +6993,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 523, + "startLine": 524, "startColumn": 32, - "endLine": 523, + "endLine": 524, "endColumn": 67, "byteLength": 35 } @@ -7016,9 +7016,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 525, + "startLine": 526, "startColumn": 12, - "endLine": 525, + "endLine": 526, "endColumn": 13, "byteLength": 1 } @@ -7041,9 +7041,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 522, + "startLine": 523, "startColumn": 10, - "endLine": 522, + "endLine": 523, "endColumn": 17, "byteLength": 7 } @@ -7064,9 +7064,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 362, + "startLine": 363, "startColumn": 16, - "endLine": 362, + "endLine": 363, "endColumn": 23, "byteLength": 7 } @@ -7087,9 +7087,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 357, + "startLine": 358, "startColumn": 45, - "endLine": 357, + "endLine": 358, "endColumn": 71, "byteLength": 26 } @@ -7110,9 +7110,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 360, + "startLine": 361, "startColumn": 24, - "endLine": 360, + "endLine": 361, "endColumn": 59, "byteLength": 35 } @@ -7133,9 +7133,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 358, + "startLine": 359, "startColumn": 10, - "endLine": 358, + "endLine": 359, "endColumn": 37, "byteLength": 27 } @@ -7158,9 +7158,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 358, + "startLine": 359, "startColumn": 10, - "endLine": 358, + "endLine": 359, "endColumn": 37, "byteLength": 27 } @@ -7183,9 +7183,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 359, + "startLine": 360, "startColumn": 10, - "endLine": 359, + "endLine": 360, "endColumn": 17, "byteLength": 7 } @@ -7206,9 +7206,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 624, + "startLine": 625, "startColumn": 16, - "endLine": 624, + "endLine": 625, "endColumn": 20, "byteLength": 4 } @@ -7229,9 +7229,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 624, + "startLine": 625, "startColumn": 16, - "endLine": 624, + "endLine": 625, "endColumn": 20, "byteLength": 4 } @@ -7252,9 +7252,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 624, + "startLine": 625, "startColumn": 16, - "endLine": 624, + "endLine": 625, "endColumn": 20, "byteLength": 4 } @@ -7275,9 +7275,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 613, + "startLine": 614, "startColumn": 30, - "endLine": 613, + "endLine": 614, "endColumn": 62, "byteLength": 32 } @@ -7298,9 +7298,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 616, + "startLine": 617, "startColumn": 22, - "endLine": 616, + "endLine": 617, "endColumn": 27, "byteLength": 5 } @@ -7321,9 +7321,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 619, + "startLine": 620, "startColumn": 25, - "endLine": 619, + "endLine": 620, "endColumn": 31, "byteLength": 6 } @@ -7344,9 +7344,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 617, + "startLine": 618, "startColumn": 29, - "endLine": 617, + "endLine": 618, "endColumn": 42, "byteLength": 13 } @@ -7367,9 +7367,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 620, + "startLine": 621, "startColumn": 25, - "endLine": 620, + "endLine": 621, "endColumn": 37, "byteLength": 12 } @@ -7390,9 +7390,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 624, + "startLine": 625, "startColumn": 16, - "endLine": 624, + "endLine": 625, "endColumn": 20, "byteLength": 4 } @@ -7415,9 +7415,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 614, + "startLine": 615, "startColumn": 10, - "endLine": 614, + "endLine": 615, "endColumn": 17, "byteLength": 7 } @@ -7438,9 +7438,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 624, + "startLine": 625, "startColumn": 16, - "endLine": 624, + "endLine": 625, "endColumn": 20, "byteLength": 4 } @@ -7461,9 +7461,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 624, + "startLine": 625, "startColumn": 16, - "endLine": 624, + "endLine": 625, "endColumn": 20, "byteLength": 4 } @@ -7484,9 +7484,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 314, + "startLine": 315, "startColumn": 12, - "endLine": 314, + "endLine": 315, "endColumn": 19, "byteLength": 7 } @@ -7507,9 +7507,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 312, + "startLine": 313, "startColumn": 32, - "endLine": 312, + "endLine": 313, "endColumn": 55, "byteLength": 23 } @@ -7530,9 +7530,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 310, + "startLine": 311, "startColumn": 10, - "endLine": 310, + "endLine": 311, "endColumn": 37, "byteLength": 27 } @@ -7555,9 +7555,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 310, + "startLine": 311, "startColumn": 10, - "endLine": 310, + "endLine": 311, "endColumn": 37, "byteLength": 27 } @@ -7580,9 +7580,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 311, + "startLine": 312, "startColumn": 10, - "endLine": 311, + "endLine": 312, "endColumn": 28, "byteLength": 18 } @@ -7603,9 +7603,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 643, + "startLine": 644, "startColumn": 14, - "endLine": 643, + "endLine": 644, "endColumn": 18, "byteLength": 4 } @@ -7626,9 +7626,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 643, + "startLine": 644, "startColumn": 14, - "endLine": 643, + "endLine": 644, "endColumn": 18, "byteLength": 4 } @@ -7651,9 +7651,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 642, + "startLine": 643, "startColumn": 12, - "endLine": 642, + "endLine": 643, "endColumn": 19, "byteLength": 7 } @@ -7674,9 +7674,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 638, + "startLine": 639, "startColumn": 21, - "endLine": 638, + "endLine": 639, "endColumn": 26, "byteLength": 5 } @@ -7697,9 +7697,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 638, + "startLine": 639, "startColumn": 21, - "endLine": 638, + "endLine": 639, "endColumn": 26, "byteLength": 5 } @@ -7720,9 +7720,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 638, + "startLine": 639, "startColumn": 21, - "endLine": 638, + "endLine": 639, "endColumn": 26, "byteLength": 5 } @@ -7743,9 +7743,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 627, + "startLine": 628, "startColumn": 30, - "endLine": 627, + "endLine": 628, "endColumn": 64, "byteLength": 34 } @@ -7766,9 +7766,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 630, + "startLine": 631, "startColumn": 22, - "endLine": 630, + "endLine": 631, "endColumn": 27, "byteLength": 5 } @@ -7789,9 +7789,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 633, + "startLine": 634, "startColumn": 25, - "endLine": 633, + "endLine": 634, "endColumn": 31, "byteLength": 6 } @@ -7812,9 +7812,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 631, + "startLine": 632, "startColumn": 29, - "endLine": 631, + "endLine": 632, "endColumn": 42, "byteLength": 13 } @@ -7835,9 +7835,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 634, + "startLine": 635, "startColumn": 25, - "endLine": 634, + "endLine": 635, "endColumn": 37, "byteLength": 12 } @@ -7858,9 +7858,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 638, + "startLine": 639, "startColumn": 21, - "endLine": 638, + "endLine": 639, "endColumn": 26, "byteLength": 5 } @@ -7883,9 +7883,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 628, + "startLine": 629, "startColumn": 10, - "endLine": 628, + "endLine": 629, "endColumn": 17, "byteLength": 7 } @@ -7906,9 +7906,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 638, + "startLine": 639, "startColumn": 21, - "endLine": 638, + "endLine": 639, "endColumn": 26, "byteLength": 5 } @@ -7929,9 +7929,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 638, + "startLine": 639, "startColumn": 21, - "endLine": 638, + "endLine": 639, "endColumn": 26, "byteLength": 5 } @@ -7952,9 +7952,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 645, + "startLine": 646, "startColumn": 15, - "endLine": 645, + "endLine": 646, "endColumn": 20, "byteLength": 5 } @@ -7975,9 +7975,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 645, + "startLine": 646, "startColumn": 15, - "endLine": 645, + "endLine": 646, "endColumn": 20, "byteLength": 5 } @@ -8000,9 +8000,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 644, + "startLine": 645, "startColumn": 12, - "endLine": 644, + "endLine": 645, "endColumn": 19, "byteLength": 7 } @@ -8023,9 +8023,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 338, + "startLine": 339, "startColumn": 16, - "endLine": 338, + "endLine": 339, "endColumn": 23, "byteLength": 7 } @@ -8046,9 +8046,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 333, + "startLine": 334, "startColumn": 33, - "endLine": 333, + "endLine": 334, "endColumn": 56, "byteLength": 23 } @@ -8069,9 +8069,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 336, + "startLine": 337, "startColumn": 24, - "endLine": 336, + "endLine": 337, "endColumn": 49, "byteLength": 25 } @@ -8092,9 +8092,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 334, + "startLine": 335, "startColumn": 10, - "endLine": 334, + "endLine": 335, "endColumn": 37, "byteLength": 27 } @@ -8117,9 +8117,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 334, + "startLine": 335, "startColumn": 10, - "endLine": 334, + "endLine": 335, "endColumn": 37, "byteLength": 27 } @@ -8142,9 +8142,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 335, + "startLine": 336, "startColumn": 10, - "endLine": 335, + "endLine": 336, "endColumn": 17, "byteLength": 7 } @@ -8165,9 +8165,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 404, "startColumn": 12, - "endLine": 403, + "endLine": 404, "endColumn": 13, "byteLength": 1 } @@ -8188,9 +8188,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 404, "startColumn": 12, - "endLine": 403, + "endLine": 404, "endColumn": 13, "byteLength": 1 } @@ -8211,9 +8211,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 404, "startColumn": 12, - "endLine": 403, + "endLine": 404, "endColumn": 13, "byteLength": 1 } @@ -8234,9 +8234,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 391, + "startLine": 392, "startColumn": 26, - "endLine": 391, + "endLine": 392, "endColumn": 44, "byteLength": 18 } @@ -8257,9 +8257,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 396, + "startLine": 397, "startColumn": 29, - "endLine": 396, + "endLine": 397, "endColumn": 48, "byteLength": 19 } @@ -8280,9 +8280,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 394, + "startLine": 395, "startColumn": 24, - "endLine": 394, + "endLine": 395, "endColumn": 44, "byteLength": 20 } @@ -8303,9 +8303,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 399, + "startLine": 400, "startColumn": 25, - "endLine": 399, + "endLine": 400, "endColumn": 39, "byteLength": 14 } @@ -8326,9 +8326,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 392, + "startLine": 393, "startColumn": 12, - "endLine": 392, + "endLine": 393, "endColumn": 28, "byteLength": 16 } @@ -8349,9 +8349,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 388, + "startLine": 389, "startColumn": 12, - "endLine": 388, + "endLine": 389, "endColumn": 28, "byteLength": 16 } @@ -8372,9 +8372,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 404, "startColumn": 12, - "endLine": 403, + "endLine": 404, "endColumn": 13, "byteLength": 1 } @@ -8397,9 +8397,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 392, + "startLine": 393, "startColumn": 12, - "endLine": 392, + "endLine": 393, "endColumn": 28, "byteLength": 16 } @@ -8422,9 +8422,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 393, + "startLine": 394, "startColumn": 12, - "endLine": 393, + "endLine": 394, "endColumn": 19, "byteLength": 7 } @@ -8447,9 +8447,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 388, + "startLine": 389, "startColumn": 12, - "endLine": 388, + "endLine": 389, "endColumn": 28, "byteLength": 16 } @@ -8472,9 +8472,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 389, + "startLine": 390, "startColumn": 12, - "endLine": 389, + "endLine": 390, "endColumn": 19, "byteLength": 7 } @@ -8497,9 +8497,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 397, + "startLine": 398, "startColumn": 12, - "endLine": 397, + "endLine": 398, "endColumn": 19, "byteLength": 7 } @@ -8520,9 +8520,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 387, + "startLine": 388, "startColumn": 14, - "endLine": 387, + "endLine": 388, "endColumn": 21, "byteLength": 7 } @@ -8543,9 +8543,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 404, "startColumn": 12, - "endLine": 403, + "endLine": 404, "endColumn": 13, "byteLength": 1 } @@ -8566,9 +8566,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 404, "startColumn": 12, - "endLine": 403, + "endLine": 404, "endColumn": 13, "byteLength": 1 } @@ -8589,9 +8589,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 403, + "startLine": 404, "startColumn": 12, - "endLine": 403, + "endLine": 404, "endColumn": 13, "byteLength": 1 } @@ -8612,9 +8612,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 653, + "startLine": 654, "startColumn": 11, - "endLine": 653, + "endLine": 654, "endColumn": 16, "byteLength": 5 } @@ -8635,9 +8635,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 651, + "startLine": 652, "startColumn": 12, - "endLine": 651, + "endLine": 652, "endColumn": 19, "byteLength": 7 } @@ -8660,9 +8660,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 651, + "startLine": 652, "startColumn": 12, - "endLine": 651, + "endLine": 652, "endColumn": 19, "byteLength": 7 } @@ -8685,9 +8685,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 651, + "startLine": 652, "startColumn": 21, - "endLine": 651, + "endLine": 652, "endColumn": 37, "byteLength": 16 } @@ -8708,9 +8708,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 685, + "startLine": 686, "startColumn": 14, - "endLine": 685, + "endLine": 686, "endColumn": 22, "byteLength": 8 } @@ -8731,9 +8731,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 681, + "startLine": 682, "startColumn": 23, - "endLine": 681, + "endLine": 682, "endColumn": 42, "byteLength": 19 } @@ -8754,9 +8754,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 682, + "startLine": 683, "startColumn": 10, - "endLine": 682, + "endLine": 683, "endColumn": 17, "byteLength": 7 } @@ -8779,9 +8779,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 682, + "startLine": 683, "startColumn": 10, - "endLine": 682, + "endLine": 683, "endColumn": 17, "byteLength": 7 } @@ -8804,9 +8804,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 683, + "startLine": 684, "startColumn": 10, - "endLine": 683, + "endLine": 684, "endColumn": 24, "byteLength": 14 } @@ -8827,9 +8827,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 665, + "startLine": 666, "startColumn": 11, - "endLine": 665, + "endLine": 666, "endColumn": 17, "byteLength": 6 } @@ -8850,9 +8850,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 658, + "startLine": 659, "startColumn": 23, - "endLine": 658, + "endLine": 659, "endColumn": 41, "byteLength": 18 } @@ -8873,9 +8873,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 663, + "startLine": 664, "startColumn": 26, - "endLine": 663, + "endLine": 664, "endColumn": 38, "byteLength": 12 } @@ -8896,9 +8896,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 659, + "startLine": 660, "startColumn": 10, - "endLine": 659, + "endLine": 660, "endColumn": 17, "byteLength": 7 } @@ -8921,9 +8921,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 659, + "startLine": 660, "startColumn": 10, - "endLine": 659, + "endLine": 660, "endColumn": 17, "byteLength": 7 } @@ -8946,9 +8946,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 661, + "startLine": 662, "startColumn": 10, - "endLine": 661, + "endLine": 662, "endColumn": 29, "byteLength": 19 } @@ -8971,9 +8971,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 661, + "startLine": 662, "startColumn": 31, - "endLine": 661, + "endLine": 662, "endColumn": 48, "byteLength": 17 } @@ -11301,9 +11301,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 736, + "startLine": 737, "startColumn": 11, - "endLine": 736, + "endLine": 737, "endColumn": 18, "byteLength": 7 } @@ -11324,9 +11324,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 729, + "startLine": 730, "startColumn": 27, - "endLine": 729, + "endLine": 730, "endColumn": 48, "byteLength": 21 } @@ -11347,9 +11347,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 730, + "startLine": 731, "startColumn": 25, - "endLine": 730, + "endLine": 731, "endColumn": 45, "byteLength": 20 } @@ -11370,9 +11370,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 733, + "startLine": 734, "startColumn": 36, - "endLine": 734, + "endLine": 735, "endColumn": 53, "byteLength": 70 } @@ -11393,9 +11393,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 731, + "startLine": 732, "startColumn": 10, - "endLine": 731, + "endLine": 732, "endColumn": 22, "byteLength": 12 } @@ -11418,9 +11418,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 731, + "startLine": 732, "startColumn": 10, - "endLine": 731, + "endLine": 732, "endColumn": 22, "byteLength": 12 } @@ -11443,9 +11443,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 732, + "startLine": 733, "startColumn": 10, - "endLine": 732, + "endLine": 733, "endColumn": 17, "byteLength": 7 } @@ -11466,9 +11466,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 749, + "startLine": 750, "startColumn": 11, - "endLine": 749, + "endLine": 750, "endColumn": 19, "byteLength": 8 } @@ -11489,9 +11489,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 741, + "startLine": 742, "startColumn": 27, - "endLine": 741, + "endLine": 742, "endColumn": 48, "byteLength": 21 } @@ -11512,9 +11512,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 742, + "startLine": 743, "startColumn": 25, - "endLine": 742, + "endLine": 743, "endColumn": 57, "byteLength": 32 } @@ -11535,9 +11535,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 743, + "startLine": 744, "startColumn": 35, - "endLine": 743, + "endLine": 744, "endColumn": 49, "byteLength": 14 } @@ -11558,9 +11558,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 746, + "startLine": 747, "startColumn": 36, - "endLine": 747, + "endLine": 748, "endColumn": 53, "byteLength": 70 } @@ -11581,9 +11581,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 744, + "startLine": 745, "startColumn": 10, - "endLine": 744, + "endLine": 745, "endColumn": 22, "byteLength": 12 } @@ -11606,9 +11606,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 744, + "startLine": 745, "startColumn": 10, - "endLine": 744, + "endLine": 745, "endColumn": 22, "byteLength": 12 } @@ -11631,9 +11631,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 745, + "startLine": 746, "startColumn": 10, - "endLine": 745, + "endLine": 746, "endColumn": 17, "byteLength": 7 } @@ -11654,9 +11654,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 354, + "startLine": 355, "startColumn": 16, - "endLine": 354, + "endLine": 355, "endColumn": 23, "byteLength": 7 } @@ -11677,9 +11677,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 349, + "startLine": 350, "startColumn": 33, - "endLine": 349, + "endLine": 350, "endColumn": 56, "byteLength": 23 } @@ -11700,9 +11700,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 352, + "startLine": 353, "startColumn": 24, - "endLine": 352, + "endLine": 353, "endColumn": 59, "byteLength": 35 } @@ -11723,9 +11723,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 350, + "startLine": 351, "startColumn": 10, - "endLine": 350, + "endLine": 351, "endColumn": 37, "byteLength": 27 } @@ -11748,9 +11748,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 350, + "startLine": 351, "startColumn": 10, - "endLine": 350, + "endLine": 351, "endColumn": 37, "byteLength": 27 } @@ -11773,9 +11773,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 351, + "startLine": 352, "startColumn": 10, - "endLine": 351, + "endLine": 352, "endColumn": 17, "byteLength": 7 } @@ -11796,9 +11796,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 346, + "startLine": 347, "startColumn": 16, - "endLine": 346, + "endLine": 347, "endColumn": 23, "byteLength": 7 } @@ -11819,9 +11819,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 341, + "startLine": 342, "startColumn": 45, - "endLine": 341, + "endLine": 342, "endColumn": 71, "byteLength": 26 } @@ -11842,9 +11842,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 344, + "startLine": 345, "startColumn": 24, - "endLine": 344, + "endLine": 345, "endColumn": 49, "byteLength": 25 } @@ -11865,9 +11865,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 342, + "startLine": 343, "startColumn": 10, - "endLine": 342, + "endLine": 343, "endColumn": 37, "byteLength": 27 } @@ -11890,9 +11890,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 342, + "startLine": 343, "startColumn": 10, - "endLine": 342, + "endLine": 343, "endColumn": 37, "byteLength": 27 } @@ -11915,9 +11915,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 343, + "startLine": 344, "startColumn": 10, - "endLine": 343, + "endLine": 344, "endColumn": 17, "byteLength": 7 } @@ -11940,9 +11940,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 724, + "startLine": 725, "startColumn": 11, - "endLine": 724, + "endLine": 725, "endColumn": 25, "byteLength": 14 } @@ -11965,9 +11965,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 724, + "startLine": 725, "startColumn": 11, - "endLine": 724, + "endLine": 725, "endColumn": 25, "byteLength": 14 } @@ -11990,9 +11990,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 724, + "startLine": 725, "startColumn": 11, - "endLine": 724, + "endLine": 725, "endColumn": 25, "byteLength": 14 } @@ -12013,9 +12013,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 701, + "startLine": 702, "startColumn": 25, - "endLine": 701, + "endLine": 702, "endColumn": 39, "byteLength": 14 } @@ -12036,9 +12036,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 703, + "startLine": 704, "startColumn": 4, - "endLine": 704, + "endLine": 705, "endColumn": 54, "byteLength": 84 } @@ -12059,9 +12059,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 710, + "startLine": 711, "startColumn": 26, - "endLine": 710, + "endLine": 711, "endColumn": 44, "byteLength": 18 } @@ -12082,9 +12082,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 717, + "startLine": 718, "startColumn": 29, - "endLine": 717, + "endLine": 718, "endColumn": 48, "byteLength": 19 } @@ -12105,9 +12105,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 714, + "startLine": 715, "startColumn": 24, - "endLine": 714, + "endLine": 715, "endColumn": 44, "byteLength": 20 } @@ -12128,9 +12128,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 715, + "startLine": 716, "startColumn": 25, - "endLine": 715, + "endLine": 716, "endColumn": 37, "byteLength": 12 } @@ -12151,9 +12151,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 720, + "startLine": 721, "startColumn": 29, - "endLine": 720, + "endLine": 721, "endColumn": 55, "byteLength": 26 } @@ -12174,9 +12174,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 711, + "startLine": 712, "startColumn": 12, - "endLine": 711, + "endLine": 712, "endColumn": 28, "byteLength": 16 } @@ -12197,9 +12197,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 706, + "startLine": 707, "startColumn": 10, - "endLine": 706, + "endLine": 707, "endColumn": 26, "byteLength": 16 } @@ -12220,9 +12220,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 724, + "startLine": 725, "startColumn": 11, - "endLine": 724, + "endLine": 725, "endColumn": 25, "byteLength": 14 } @@ -12245,9 +12245,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 711, + "startLine": 712, "startColumn": 12, - "endLine": 711, + "endLine": 712, "endColumn": 28, "byteLength": 16 } @@ -12270,9 +12270,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 712, + "startLine": 713, "startColumn": 12, - "endLine": 712, + "endLine": 713, "endColumn": 19, "byteLength": 7 } @@ -12295,9 +12295,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 706, + "startLine": 707, "startColumn": 10, - "endLine": 706, + "endLine": 707, "endColumn": 26, "byteLength": 16 } @@ -12320,9 +12320,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 707, + "startLine": 708, "startColumn": 10, - "endLine": 707, + "endLine": 708, "endColumn": 17, "byteLength": 7 } @@ -12345,9 +12345,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 718, + "startLine": 719, "startColumn": 12, - "endLine": 718, + "endLine": 719, "endColumn": 19, "byteLength": 7 } @@ -12370,9 +12370,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 705, + "startLine": 706, "startColumn": 12, - "endLine": 705, + "endLine": 706, "endColumn": 19, "byteLength": 7 } @@ -12395,9 +12395,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 724, + "startLine": 725, "startColumn": 11, - "endLine": 724, + "endLine": 725, "endColumn": 25, "byteLength": 14 } @@ -12420,9 +12420,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 724, + "startLine": 725, "startColumn": 11, - "endLine": 724, + "endLine": 725, "endColumn": 25, "byteLength": 14 } @@ -12445,9 +12445,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 724, + "startLine": 725, "startColumn": 11, - "endLine": 724, + "endLine": 725, "endColumn": 25, "byteLength": 14 } @@ -12468,9 +12468,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 532, + "startLine": 533, "startColumn": 11, - "endLine": 532, + "endLine": 533, "endColumn": 17, "byteLength": 6 } @@ -12491,9 +12491,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 528, + "startLine": 529, "startColumn": 25, - "endLine": 528, + "endLine": 529, "endColumn": 50, "byteLength": 25 } @@ -12514,9 +12514,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 529, + "startLine": 530, "startColumn": 10, - "endLine": 529, + "endLine": 530, "endColumn": 23, "byteLength": 13 } @@ -12539,9 +12539,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 529, + "startLine": 530, "startColumn": 10, - "endLine": 529, + "endLine": 530, "endColumn": 23, "byteLength": 13 } @@ -12564,9 +12564,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 530, + "startLine": 531, "startColumn": 10, - "endLine": 530, + "endLine": 531, "endColumn": 17, "byteLength": 7 } @@ -12587,9 +12587,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 593, + "startLine": 594, "startColumn": 12, - "endLine": 593, + "endLine": 594, "endColumn": 17, "byteLength": 5 } @@ -12610,9 +12610,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 588, + "startLine": 589, "startColumn": 34, - "endLine": 588, + "endLine": 589, "endColumn": 57, "byteLength": 23 } @@ -12633,9 +12633,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 589, + "startLine": 590, "startColumn": 10, - "endLine": 589, + "endLine": 590, "endColumn": 29, "byteLength": 19 } @@ -12658,9 +12658,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 589, + "startLine": 590, "startColumn": 10, - "endLine": 589, + "endLine": 590, "endColumn": 29, "byteLength": 19 } @@ -12681,9 +12681,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 556, + "startLine": 557, "startColumn": 12, - "endLine": 556, + "endLine": 557, "endColumn": 22, "byteLength": 10 } @@ -12704,9 +12704,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 554, + "startLine": 555, "startColumn": 28, - "endLine": 554, + "endLine": 555, "endColumn": 34, "byteLength": 6 } @@ -12727,9 +12727,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 556, + "startLine": 557, "startColumn": 12, - "endLine": 556, + "endLine": 557, "endColumn": 22, "byteLength": 10 } @@ -12750,9 +12750,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 272, + "startLine": 273, "startColumn": 11, - "endLine": 272, + "endLine": 273, "endColumn": 15, "byteLength": 4 } @@ -12773,9 +12773,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 270, + "startLine": 271, "startColumn": 26, - "endLine": 270, + "endLine": 271, "endColumn": 55, "byteLength": 29 } @@ -12796,9 +12796,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 268, + "startLine": 269, "startColumn": 12, - "endLine": 268, + "endLine": 269, "endColumn": 19, "byteLength": 7 } @@ -12821,9 +12821,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 268, + "startLine": 269, "startColumn": 12, - "endLine": 268, + "endLine": 269, "endColumn": 19, "byteLength": 7 } @@ -12846,9 +12846,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 269, + "startLine": 270, "startColumn": 12, - "endLine": 269, + "endLine": 270, "endColumn": 31, "byteLength": 19 } @@ -12869,9 +12869,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 281, + "startLine": 282, "startColumn": 16, - "endLine": 281, + "endLine": 282, "endColumn": 22, "byteLength": 6 } @@ -12892,9 +12892,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 279, + "startLine": 280, "startColumn": 24, - "endLine": 279, + "endLine": 280, "endColumn": 53, "byteLength": 29 } @@ -12915,9 +12915,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 281, + "startLine": 282, "startColumn": 16, - "endLine": 281, + "endLine": 282, "endColumn": 22, "byteLength": 6 } @@ -12940,9 +12940,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 278, + "startLine": 279, "startColumn": 10, - "endLine": 278, + "endLine": 279, "endColumn": 17, "byteLength": 7 } @@ -12963,9 +12963,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -12986,9 +12986,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13009,9 +13009,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13032,9 +13032,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13055,9 +13055,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 422, + "startLine": 423, "startColumn": 22, - "endLine": 422, + "endLine": 423, "endColumn": 52, "byteLength": 30 } @@ -13078,9 +13078,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 429, + "startLine": 430, "startColumn": 27, - "endLine": 429, + "endLine": 430, "endColumn": 45, "byteLength": 18 } @@ -13101,9 +13101,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 435, + "startLine": 436, "startColumn": 26, - "endLine": 435, + "endLine": 436, "endColumn": 38, "byteLength": 12 } @@ -13124,9 +13124,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 436, + "startLine": 437, "startColumn": 27, - "endLine": 436, + "endLine": 437, "endColumn": 45, "byteLength": 18 } @@ -13147,9 +13147,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 442, + "startLine": 443, "startColumn": 30, - "endLine": 442, + "endLine": 443, "endColumn": 49, "byteLength": 19 } @@ -13170,9 +13170,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 432, + "startLine": 433, "startColumn": 25, - "endLine": 432, + "endLine": 433, "endColumn": 45, "byteLength": 20 } @@ -13193,9 +13193,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 438, + "startLine": 439, "startColumn": 20, - "endLine": 438, + "endLine": 439, "endColumn": 35, "byteLength": 15 } @@ -13216,9 +13216,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 439, + "startLine": 440, "startColumn": 23, - "endLine": 439, + "endLine": 440, "endColumn": 61, "byteLength": 38 } @@ -13239,9 +13239,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 446, + "startLine": 447, "startColumn": 26, - "endLine": 446, + "endLine": 447, "endColumn": 42, "byteLength": 16 } @@ -13262,9 +13262,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13285,9 +13285,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 425, + "startLine": 426, "startColumn": 11, - "endLine": 425, + "endLine": 426, "endColumn": 27, "byteLength": 16 } @@ -13308,9 +13308,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13333,9 +13333,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 431, + "startLine": 432, "startColumn": 13, - "endLine": 431, + "endLine": 432, "endColumn": 20, "byteLength": 7 } @@ -13358,9 +13358,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 425, + "startLine": 426, "startColumn": 11, - "endLine": 425, + "endLine": 426, "endColumn": 27, "byteLength": 16 } @@ -13383,9 +13383,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 426, + "startLine": 427, "startColumn": 11, - "endLine": 426, + "endLine": 427, "endColumn": 18, "byteLength": 7 } @@ -13408,9 +13408,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 445, + "startLine": 446, "startColumn": 13, - "endLine": 445, + "endLine": 446, "endColumn": 20, "byteLength": 7 } @@ -13433,9 +13433,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 430, + "startLine": 431, "startColumn": 15, - "endLine": 430, + "endLine": 431, "endColumn": 22, "byteLength": 7 } @@ -13458,9 +13458,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 437, + "startLine": 438, "startColumn": 11, - "endLine": 437, + "endLine": 438, "endColumn": 14, "byteLength": 3 } @@ -13483,9 +13483,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 424, + "startLine": 425, "startColumn": 9, - "endLine": 424, + "endLine": 425, "endColumn": 12, "byteLength": 3 } @@ -13508,9 +13508,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13531,9 +13531,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13554,9 +13554,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13577,9 +13577,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 452, + "startLine": 453, "startColumn": 12, - "endLine": 452, + "endLine": 453, "endColumn": 13, "byteLength": 1 } @@ -13602,9 +13602,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -13627,9 +13627,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -13652,9 +13652,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -13675,9 +13675,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -13698,9 +13698,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 456, + "startLine": 457, "startColumn": 22, - "endLine": 456, + "endLine": 457, "endColumn": 52, "byteLength": 30 } @@ -13721,9 +13721,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 465, + "startLine": 466, "startColumn": 27, - "endLine": 465, + "endLine": 466, "endColumn": 53, "byteLength": 26 } @@ -13744,9 +13744,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 470, + "startLine": 471, "startColumn": 26, - "endLine": 470, + "endLine": 471, "endColumn": 38, "byteLength": 12 } @@ -13767,9 +13767,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 471, + "startLine": 472, "startColumn": 27, - "endLine": 471, + "endLine": 472, "endColumn": 53, "byteLength": 26 } @@ -13790,9 +13790,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 477, + "startLine": 478, "startColumn": 30, - "endLine": 477, + "endLine": 478, "endColumn": 57, "byteLength": 27 } @@ -13813,9 +13813,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 467, + "startLine": 468, "startColumn": 25, - "endLine": 467, + "endLine": 468, "endColumn": 54, "byteLength": 29 } @@ -13836,9 +13836,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 473, + "startLine": 474, "startColumn": 20, - "endLine": 473, + "endLine": 474, "endColumn": 35, "byteLength": 15 } @@ -13859,9 +13859,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 474, + "startLine": 475, "startColumn": 23, - "endLine": 474, + "endLine": 475, "endColumn": 61, "byteLength": 38 } @@ -13882,9 +13882,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 482, + "startLine": 483, "startColumn": 26, - "endLine": 482, + "endLine": 483, "endColumn": 42, "byteLength": 16 } @@ -13905,9 +13905,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 459, + "startLine": 460, "startColumn": 11, - "endLine": 459, + "endLine": 460, "endColumn": 27, "byteLength": 16 } @@ -13928,9 +13928,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -13953,9 +13953,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 459, + "startLine": 460, "startColumn": 11, - "endLine": 459, + "endLine": 460, "endColumn": 27, "byteLength": 16 } @@ -13978,9 +13978,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 461, + "startLine": 462, "startColumn": 11, - "endLine": 461, + "endLine": 462, "endColumn": 18, "byteLength": 7 } @@ -14003,9 +14003,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 480, + "startLine": 481, "startColumn": 13, - "endLine": 480, + "endLine": 481, "endColumn": 20, "byteLength": 7 } @@ -14028,9 +14028,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 466, + "startLine": 467, "startColumn": 15, - "endLine": 466, + "endLine": 467, "endColumn": 22, "byteLength": 7 } @@ -14053,9 +14053,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 472, + "startLine": 473, "startColumn": 11, - "endLine": 472, + "endLine": 473, "endColumn": 14, "byteLength": 3 } @@ -14078,9 +14078,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 458, + "startLine": 459, "startColumn": 9, - "endLine": 458, + "endLine": 459, "endColumn": 12, "byteLength": 3 } @@ -14103,9 +14103,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -14126,9 +14126,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -14149,9 +14149,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -14172,9 +14172,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 488, + "startLine": 489, "startColumn": 12, - "endLine": 488, + "endLine": 489, "endColumn": 13, "byteLength": 1 } @@ -14197,9 +14197,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 783, + "startLine": 807, "startColumn": 12, - "endLine": 783, + "endLine": 807, "endColumn": 13, "byteLength": 1 } @@ -14220,9 +14220,34 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 783, + "startLine": 807, + "startColumn": 12, + "endLine": 807, + "endColumn": 13, + "byteLength": 1 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { + "text": "behavior filesystem_error in function realpath." + }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 807, "startColumn": 12, - "endLine": 783, + "endLine": 807, "endColumn": 13, "byteLength": 1 } @@ -14245,9 +14270,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 783, + "startLine": 807, "startColumn": 12, - "endLine": 783, + "endLine": 807, "endColumn": 13, "byteLength": 1 } @@ -14260,7 +14285,7 @@ "kind": "pass", "level": "none", "message": { - "text": "behavior resolved_name_buffer in function realpath." + "text": "behavior null_file_name in function realpath." }, "locations": [ { @@ -14270,9 +14295,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 783, + "startLine": 807, "startColumn": 12, - "endLine": 783, + "endLine": 807, "endColumn": 13, "byteLength": 1 } @@ -14284,7 +14309,9 @@ "ruleId": "user-spec", "kind": "pass", "level": "none", - "message": { "text": "valid_file_name." }, + "message": { + "text": "behavior resolved_name_buffer in function realpath." + }, "locations": [ { "physicalLocation": { @@ -14293,11 +14320,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 755, - "startColumn": 28, - "endLine": 755, - "endColumn": 56, - "byteLength": 28 + "startLine": 807, + "startColumn": 12, + "endLine": 807, + "endColumn": 13, + "byteLength": 1 } } } @@ -14307,7 +14334,7 @@ "ruleId": "user-spec", "kind": "pass", "level": "none", - "message": { "text": "resolved_name_null_or_allocated." }, + "message": { "text": "valid_file_name_or_null." }, "locations": [ { "physicalLocation": { @@ -14319,6 +14346,29 @@ "startLine": 757, "startColumn": 4, "endLine": 757, + "endColumn": 54, + "byteLength": 50 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "resolved_name_null_or_allocated." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 759, + "startColumn": 4, + "endLine": 759, "endColumn": 66, "byteLength": 62 } @@ -14326,6 +14376,52 @@ } ] }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "null_file_name." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 767, + "startColumn": 28, + "endLine": 767, + "endColumn": 46, + "byteLength": 18 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "valid_file_name." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 772, + "startColumn": 29, + "endLine": 772, + "endColumn": 57, + "byteLength": 28 + } + } + } + ] + }, { "ruleId": "user-spec", "kind": "pass", @@ -14339,9 +14435,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 762, + "startLine": 773, "startColumn": 32, - "endLine": 762, + "endLine": 773, "endColumn": 54, "byteLength": 22 } @@ -14362,9 +14458,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 763, + "startLine": 774, "startColumn": 26, - "endLine": 763, + "endLine": 774, "endColumn": 44, "byteLength": 18 } @@ -14372,6 +14468,29 @@ } ] }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "valid_file_name." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 779, + "startColumn": 29, + "endLine": 779, + "endColumn": 57, + "byteLength": 28 + } + } + } + ] + }, { "ruleId": "user-spec", "kind": "pass", @@ -14385,9 +14504,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 768, + "startLine": 780, "startColumn": 32, - "endLine": 768, + "endLine": 780, "endColumn": 54, "byteLength": 22 } @@ -14395,6 +14514,52 @@ } ] }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "cannot_allocate." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 781, + "startColumn": 29, + "endLine": 781, + "endColumn": 48, + "byteLength": 19 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "valid_file_name." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 787, + "startColumn": 29, + "endLine": 787, + "endColumn": 57, + "byteLength": 28 + } + } + } + ] + }, { "ruleId": "user-spec", "kind": "pass", @@ -14408,9 +14573,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 774, + "startLine": 789, "startColumn": 6, - "endLine": 774, + "endLine": 789, "endColumn": 42, "byteLength": 36 } @@ -14418,6 +14583,75 @@ } ] }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "valid_file_name." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 799, + "startColumn": 29, + "endLine": 799, + "endColumn": 57, + "byteLength": 28 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "null_result." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 769, + "startColumn": 25, + "endLine": 769, + "endColumn": 41, + "byteLength": 16 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "errno_set." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 770, + "startColumn": 23, + "endLine": 770, + "endColumn": 39, + "byteLength": 16 + } + } + } + ] + }, { "ruleId": "user-spec", "kind": "pass", @@ -14431,9 +14665,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 766, + "startLine": 777, "startColumn": 24, - "endLine": 766, + "endLine": 777, "endColumn": 44, "byteLength": 20 } @@ -14454,9 +14688,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 771, + "startLine": 784, "startColumn": 25, - "endLine": 771, + "endLine": 784, "endColumn": 41, "byteLength": 16 } @@ -14464,6 +14698,29 @@ } ] }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "errno_set." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 785, + "startColumn": 23, + "endLine": 785, + "endColumn": 39, + "byteLength": 16 + } + } + } + ] + }, { "ruleId": "user-spec", "kind": "pass", @@ -14477,11 +14734,243 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 777, + "startLine": 792, "startColumn": 40, - "endLine": 777, - "endColumn": 67, - "byteLength": 27 + "endLine": 793, + "endColumn": 71, + "byteLength": 99 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "resolved_result." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 796, + "startColumn": 29, + "endLine": 796, + "endColumn": 53, + "byteLength": 24 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "null_result." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 802, + "startColumn": 25, + "endLine": 802, + "endColumn": 41, + "byteLength": 16 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "errno_set." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 804, + "startColumn": 6, + "endLine": 804, + "endColumn": 43, + "byteLength": 37 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "assigns clause in function realpath." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 775, + "startColumn": 12, + "endLine": 775, + "endColumn": 28, + "byteLength": 16 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "assigns clause in function realpath." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 760, + "startColumn": 10, + "endLine": 760, + "endColumn": 26, + "byteLength": 16 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "assigns clause in function realpath." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 800, + "startColumn": 12, + "endLine": 800, + "endColumn": 19, + "byteLength": 7 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "assigns clause in function realpath." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 807, + "startColumn": 12, + "endLine": 807, + "endColumn": 13, + "byteLength": 1 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "assigns clause in function realpath." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 768, + "startColumn": 12, + "endLine": 768, + "endColumn": 19, + "byteLength": 7 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { "text": "assigns clause in function realpath." }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 790, + "startColumn": 12, + "endLine": 790, + "endColumn": 19, + "byteLength": 7 + } + } + } + ] + }, + { + "ruleId": "user-spec", + "kind": "pass", + "level": "none", + "message": { + "text": "from clause of term __fc_heap_status in function realpath." + }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "libc/stdlib.h", + "uriBaseId": "FRAMAC_SHARE" + }, + "region": { + "startLine": 775, + "startColumn": 12, + "endLine": 775, + "endColumn": 28, + "byteLength": 16 } } } @@ -14491,7 +14980,9 @@ "ruleId": "user-spec", "kind": "pass", "level": "none", - "message": { "text": "resolved_result." }, + "message": { + "text": "from clause of term \\result in function realpath." + }, "locations": [ { "physicalLocation": { @@ -14500,11 +14991,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 780, - "startColumn": 29, - "endLine": 780, - "endColumn": 53, - "byteLength": 24 + "startLine": 776, + "startColumn": 12, + "endLine": 776, + "endColumn": 19, + "byteLength": 7 } } } @@ -14514,7 +15005,9 @@ "ruleId": "user-spec", "kind": "pass", "level": "none", - "message": { "text": "assigns clause in function realpath." }, + "message": { + "text": "from clause of term __fc_heap_status in function realpath." + }, "locations": [ { "physicalLocation": { @@ -14523,10 +15016,10 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 764, - "startColumn": 12, - "endLine": 764, - "endColumn": 28, + "startLine": 760, + "startColumn": 10, + "endLine": 760, + "endColumn": 26, "byteLength": 16 } } @@ -14537,7 +15030,9 @@ "ruleId": "user-spec", "kind": "pass", "level": "none", - "message": { "text": "assigns clause in function realpath." }, + "message": { + "text": "from clause of term *(\\result + (0 .. 4096 - 1)) in function realpath." + }, "locations": [ { "physicalLocation": { @@ -14546,11 +15041,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 758, + "startLine": 761, "startColumn": 10, - "endLine": 758, - "endColumn": 26, - "byteLength": 16 + "endLine": 761, + "endColumn": 31, + "byteLength": 21 } } } @@ -14560,7 +15055,9 @@ "ruleId": "user-spec", "kind": "pass", "level": "none", - "message": { "text": "assigns clause in function realpath." }, + "message": { + "text": "from clause of term *(resolved_name + (0 .. 4096 - 1)) in function realpath." + }, "locations": [ { "physicalLocation": { @@ -14569,11 +15066,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 783, - "startColumn": 12, - "endLine": 783, - "endColumn": 13, - "byteLength": 1 + "startLine": 761, + "startColumn": 33, + "endLine": 761, + "endColumn": 60, + "byteLength": 27 } } } @@ -14583,7 +15080,9 @@ "ruleId": "user-spec", "kind": "pass", "level": "none", - "message": { "text": "assigns clause in function realpath." }, + "message": { + "text": "from clause of term __fc_errno in function realpath." + }, "locations": [ { "physicalLocation": { @@ -14592,11 +15091,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 775, - "startColumn": 12, - "endLine": 775, - "endColumn": 19, - "byteLength": 7 + "startLine": 763, + "startColumn": 10, + "endLine": 763, + "endColumn": 20, + "byteLength": 10 } } } @@ -14607,7 +15106,7 @@ "kind": "pass", "level": "none", "message": { - "text": "from clause of term __fc_heap_status in function realpath." + "text": "from clause of term \\result in function realpath." }, "locations": [ { @@ -14617,11 +15116,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 764, + "startLine": 800, "startColumn": 12, - "endLine": 764, - "endColumn": 28, - "byteLength": 16 + "endLine": 800, + "endColumn": 19, + "byteLength": 7 } } } @@ -14632,7 +15131,7 @@ "kind": "pass", "level": "none", "message": { - "text": "from clause of term \\result in function realpath." + "text": "from clause of term __fc_errno in function realpath." }, "locations": [ { @@ -14642,11 +15141,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 765, - "startColumn": 12, - "endLine": 765, - "endColumn": 19, - "byteLength": 7 + "startLine": 800, + "startColumn": 21, + "endLine": 800, + "endColumn": 31, + "byteLength": 10 } } } @@ -14657,7 +15156,7 @@ "kind": "pass", "level": "none", "message": { - "text": "from clause of term __fc_heap_status in function realpath." + "text": "from clause of term \\result in function realpath." }, "locations": [ { @@ -14667,11 +15166,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 758, - "startColumn": 10, - "endLine": 758, - "endColumn": 26, - "byteLength": 16 + "startLine": 782, + "startColumn": 12, + "endLine": 782, + "endColumn": 19, + "byteLength": 7 } } } @@ -14692,10 +15191,10 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 759, - "startColumn": 10, - "endLine": 759, - "endColumn": 17, + "startLine": 768, + "startColumn": 12, + "endLine": 768, + "endColumn": 19, "byteLength": 7 } } @@ -14707,7 +15206,7 @@ "kind": "pass", "level": "none", "message": { - "text": "from clause of term *(resolved_name + (0 .. 4096 - 1)) in function realpath." + "text": "from clause of term __fc_errno in function realpath." }, "locations": [ { @@ -14717,11 +15216,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 759, - "startColumn": 19, - "endLine": 759, - "endColumn": 46, - "byteLength": 27 + "startLine": 768, + "startColumn": 21, + "endLine": 768, + "endColumn": 31, + "byteLength": 10 } } } @@ -14742,9 +15241,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 769, + "startLine": 790, "startColumn": 12, - "endLine": 769, + "endLine": 790, "endColumn": 19, "byteLength": 7 } @@ -14757,7 +15256,7 @@ "kind": "pass", "level": "none", "message": { - "text": "from clause of term \\result in function realpath." + "text": "from clause of term *(resolved_name + (0 .. 4096 - 1)) in function realpath." }, "locations": [ { @@ -14767,11 +15266,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 775, + "startLine": 791, "startColumn": 12, - "endLine": 775, - "endColumn": 19, - "byteLength": 7 + "endLine": 791, + "endColumn": 39, + "byteLength": 27 } } } @@ -14782,7 +15281,7 @@ "kind": "pass", "level": "none", "message": { - "text": "from clause of term *(resolved_name + (0 .. 4096 - 1)) in function realpath." + "text": "allocates/frees clause in function realpath." }, "locations": [ { @@ -14792,11 +15291,11 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 776, + "startLine": 807, "startColumn": 12, - "endLine": 776, - "endColumn": 39, - "byteLength": 27 + "endLine": 807, + "endColumn": 13, + "byteLength": 1 } } } @@ -14817,9 +15316,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 783, + "startLine": 807, "startColumn": 12, - "endLine": 783, + "endLine": 807, "endColumn": 13, "byteLength": 1 } @@ -14842,9 +15341,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 783, + "startLine": 807, "startColumn": 12, - "endLine": 783, + "endLine": 807, "endColumn": 13, "byteLength": 1 } @@ -14865,9 +15364,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 307, + "startLine": 308, "startColumn": 22, - "endLine": 307, + "endLine": 308, "endColumn": 23, "byteLength": 1 } @@ -14888,9 +15387,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 300, + "startLine": 301, "startColumn": 47, - "endLine": 300, + "endLine": 301, "endColumn": 75, "byteLength": 28 } @@ -14911,9 +15410,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 304, + "startLine": 305, "startColumn": 32, - "endLine": 304, + "endLine": 305, "endColumn": 55, "byteLength": 23 } @@ -14934,9 +15433,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 305, + "startLine": 306, "startColumn": 26, - "endLine": 305, + "endLine": 306, "endColumn": 60, "byteLength": 34 } @@ -14957,9 +15456,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 301, + "startLine": 302, "startColumn": 10, - "endLine": 301, + "endLine": 302, "endColumn": 37, "byteLength": 27 } @@ -14982,9 +15481,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 301, + "startLine": 302, "startColumn": 10, - "endLine": 301, + "endLine": 302, "endColumn": 37, "byteLength": 27 } @@ -15007,9 +15506,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 302, + "startLine": 303, "startColumn": 10, - "endLine": 302, + "endLine": 303, "endColumn": 28, "byteLength": 18 } @@ -15032,9 +15531,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 303, + "startLine": 304, "startColumn": 10, - "endLine": 303, + "endLine": 304, "endColumn": 17, "byteLength": 7 } @@ -15055,9 +15554,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 542, + "startLine": 543, "startColumn": 11, - "endLine": 542, + "endLine": 543, "endColumn": 17, "byteLength": 6 } @@ -15078,9 +15577,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 535, + "startLine": 536, "startColumn": 23, - "endLine": 535, + "endLine": 536, "endColumn": 46, "byteLength": 23 } @@ -15101,9 +15600,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 536, + "startLine": 537, "startColumn": 24, - "endLine": 536, + "endLine": 537, "endColumn": 48, "byteLength": 24 } @@ -15124,9 +15623,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 540, + "startLine": 541, "startColumn": 30, - "endLine": 540, + "endLine": 541, "endColumn": 59, "byteLength": 29 } @@ -15147,9 +15646,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 537, + "startLine": 538, "startColumn": 10, - "endLine": 537, + "endLine": 538, "endColumn": 17, "byteLength": 7 } @@ -15172,9 +15671,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 537, + "startLine": 538, "startColumn": 10, - "endLine": 537, + "endLine": 538, "endColumn": 17, "byteLength": 7 } @@ -15197,9 +15696,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 537, + "startLine": 538, "startColumn": 19, - "endLine": 537, + "endLine": 538, "endColumn": 32, "byteLength": 13 } @@ -15220,9 +15719,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 275, + "startLine": 276, "startColumn": 12, - "endLine": 275, + "endLine": 276, "endColumn": 17, "byteLength": 5 } @@ -15243,9 +15742,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 274, + "startLine": 275, "startColumn": 12, - "endLine": 274, + "endLine": 275, "endColumn": 31, "byteLength": 19 } @@ -15268,9 +15767,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 274, + "startLine": 275, "startColumn": 12, - "endLine": 274, + "endLine": 275, "endColumn": 31, "byteLength": 19 } @@ -15291,9 +15790,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 297, + "startLine": 298, "startColumn": 12, - "endLine": 297, + "endLine": 298, "endColumn": 19, "byteLength": 7 } @@ -15314,9 +15813,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 295, + "startLine": 296, "startColumn": 32, - "endLine": 295, + "endLine": 296, "endColumn": 55, "byteLength": 23 } @@ -15337,9 +15836,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 293, + "startLine": 294, "startColumn": 10, - "endLine": 293, + "endLine": 294, "endColumn": 37, "byteLength": 27 } @@ -15362,9 +15861,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 293, + "startLine": 294, "startColumn": 10, - "endLine": 293, + "endLine": 294, "endColumn": 37, "byteLength": 27 } @@ -15387,9 +15886,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 294, + "startLine": 295, "startColumn": 10, - "endLine": 294, + "endLine": 295, "endColumn": 28, "byteLength": 18 } @@ -15410,9 +15909,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 284, + "startLine": 285, "startColumn": 12, - "endLine": 284, + "endLine": 285, "endColumn": 19, "byteLength": 7 } @@ -15433,9 +15932,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 284, "startColumn": 12, - "endLine": 283, + "endLine": 284, "endColumn": 31, "byteLength": 19 } @@ -15458,9 +15957,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 283, + "startLine": 284, "startColumn": 12, - "endLine": 283, + "endLine": 284, "endColumn": 31, "byteLength": 19 } @@ -21548,9 +22047,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 117, "startColumn": 14, - "endLine": 116, + "endLine": 117, "endColumn": 20, "byteLength": 6 } @@ -21571,9 +22070,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 117, "startColumn": 14, - "endLine": 116, + "endLine": 117, "endColumn": 20, "byteLength": 6 } @@ -21596,9 +22095,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 117, "startColumn": 14, - "endLine": 116, + "endLine": 117, "endColumn": 20, "byteLength": 6 } @@ -21619,9 +22118,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 98, + "startLine": 99, "startColumn": 30, - "endLine": 98, + "endLine": 99, "endColumn": 53, "byteLength": 23 } @@ -21642,9 +22141,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 99, + "startLine": 100, "startColumn": 23, - "endLine": 99, + "endLine": 100, "endColumn": 47, "byteLength": 24 } @@ -21665,9 +22164,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 107, + "startLine": 108, "startColumn": 27, - "endLine": 107, + "endLine": 108, "endColumn": 41, "byteLength": 14 } @@ -21688,9 +22187,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 103, + "startLine": 104, "startColumn": 25, - "endLine": 103, + "endLine": 104, "endColumn": 40, "byteLength": 15 } @@ -21711,9 +22210,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 106, + "startLine": 107, "startColumn": 28, - "endLine": 106, + "endLine": 107, "endColumn": 43, "byteLength": 15 } @@ -21734,9 +22233,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 110, + "startLine": 111, "startColumn": 28, - "endLine": 110, + "endLine": 111, "endColumn": 48, "byteLength": 20 } @@ -21757,9 +22256,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 111, + "startLine": 112, "startColumn": 34, - "endLine": 111, + "endLine": 112, "endColumn": 54, "byteLength": 20 } @@ -21780,9 +22279,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 112, + "startLine": 113, "startColumn": 29, - "endLine": 112, + "endLine": 113, "endColumn": 60, "byteLength": 31 } @@ -21803,9 +22302,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 100, + "startLine": 101, "startColumn": 10, - "endLine": 100, + "endLine": 101, "endColumn": 17, "byteLength": 7 } @@ -21826,9 +22325,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 117, "startColumn": 14, - "endLine": 116, + "endLine": 117, "endColumn": 20, "byteLength": 6 } @@ -21849,9 +22348,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 108, + "startLine": 109, "startColumn": 12, - "endLine": 108, + "endLine": 109, "endColumn": 19, "byteLength": 7 } @@ -21874,9 +22373,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 100, + "startLine": 101, "startColumn": 10, - "endLine": 100, + "endLine": 101, "endColumn": 17, "byteLength": 7 } @@ -21899,9 +22398,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 101, + "startLine": 102, "startColumn": 10, - "endLine": 101, + "endLine": 102, "endColumn": 17, "byteLength": 7 } @@ -21924,9 +22423,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 104, + "startLine": 105, "startColumn": 12, - "endLine": 104, + "endLine": 105, "endColumn": 19, "byteLength": 7 } @@ -21949,9 +22448,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 108, + "startLine": 109, "startColumn": 12, - "endLine": 108, + "endLine": 109, "endColumn": 19, "byteLength": 7 } @@ -21974,9 +22473,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 109, + "startLine": 110, "startColumn": 12, - "endLine": 109, + "endLine": 110, "endColumn": 19, "byteLength": 7 } @@ -21997,9 +22496,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 117, "startColumn": 14, - "endLine": 116, + "endLine": 117, "endColumn": 20, "byteLength": 6 } @@ -22020,9 +22519,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 116, + "startLine": 117, "startColumn": 14, - "endLine": 116, + "endLine": 117, "endColumn": 20, "byteLength": 6 } @@ -22043,9 +22542,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 138, + "startLine": 139, "startColumn": 13, - "endLine": 138, + "endLine": 139, "endColumn": 19, "byteLength": 6 } @@ -22066,9 +22565,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 138, + "startLine": 139, "startColumn": 13, - "endLine": 138, + "endLine": 139, "endColumn": 19, "byteLength": 6 } @@ -22091,9 +22590,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 138, + "startLine": 139, "startColumn": 13, - "endLine": 138, + "endLine": 139, "endColumn": 19, "byteLength": 6 } @@ -22114,9 +22613,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 120, + "startLine": 121, "startColumn": 30, - "endLine": 120, + "endLine": 121, "endColumn": 53, "byteLength": 23 } @@ -22137,9 +22636,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 121, + "startLine": 122, "startColumn": 23, - "endLine": 121, + "endLine": 122, "endColumn": 47, "byteLength": 24 } @@ -22160,9 +22659,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 129, + "startLine": 130, "startColumn": 27, - "endLine": 129, + "endLine": 130, "endColumn": 41, "byteLength": 14 } @@ -22183,9 +22682,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 125, + "startLine": 126, "startColumn": 25, - "endLine": 125, + "endLine": 126, "endColumn": 40, "byteLength": 15 } @@ -22206,9 +22705,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 128, + "startLine": 129, "startColumn": 28, - "endLine": 128, + "endLine": 129, "endColumn": 43, "byteLength": 15 } @@ -22229,9 +22728,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 132, + "startLine": 133, "startColumn": 28, - "endLine": 132, + "endLine": 133, "endColumn": 48, "byteLength": 20 } @@ -22252,9 +22751,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 133, + "startLine": 134, "startColumn": 34, - "endLine": 133, + "endLine": 134, "endColumn": 54, "byteLength": 20 } @@ -22275,9 +22774,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 134, + "startLine": 135, "startColumn": 29, - "endLine": 134, + "endLine": 135, "endColumn": 60, "byteLength": 31 } @@ -22298,9 +22797,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 122, + "startLine": 123, "startColumn": 10, - "endLine": 122, + "endLine": 123, "endColumn": 17, "byteLength": 7 } @@ -22321,9 +22820,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 138, + "startLine": 139, "startColumn": 13, - "endLine": 138, + "endLine": 139, "endColumn": 19, "byteLength": 6 } @@ -22344,9 +22843,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 130, + "startLine": 131, "startColumn": 12, - "endLine": 130, + "endLine": 131, "endColumn": 19, "byteLength": 7 } @@ -22369,9 +22868,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 122, + "startLine": 123, "startColumn": 10, - "endLine": 122, + "endLine": 123, "endColumn": 17, "byteLength": 7 } @@ -22394,9 +22893,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 123, + "startLine": 124, "startColumn": 10, - "endLine": 123, + "endLine": 124, "endColumn": 17, "byteLength": 7 } @@ -22419,9 +22918,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 126, + "startLine": 127, "startColumn": 12, - "endLine": 126, + "endLine": 127, "endColumn": 19, "byteLength": 7 } @@ -22444,9 +22943,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 130, + "startLine": 131, "startColumn": 12, - "endLine": 130, + "endLine": 131, "endColumn": 19, "byteLength": 7 } @@ -22469,9 +22968,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 131, + "startLine": 132, "startColumn": 12, - "endLine": 131, + "endLine": 132, "endColumn": 19, "byteLength": 7 } @@ -22492,9 +22991,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 138, + "startLine": 139, "startColumn": 13, - "endLine": 138, + "endLine": 139, "endColumn": 19, "byteLength": 6 } @@ -22515,9 +23014,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 138, + "startLine": 139, "startColumn": 13, - "endLine": 138, + "endLine": 139, "endColumn": 19, "byteLength": 6 } @@ -23889,9 +24388,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 184, + "startLine": 185, "startColumn": 16, - "endLine": 184, + "endLine": 185, "endColumn": 22, "byteLength": 6 } @@ -23912,9 +24411,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 184, + "startLine": 185, "startColumn": 16, - "endLine": 184, + "endLine": 185, "endColumn": 22, "byteLength": 6 } @@ -23937,9 +24436,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 184, + "startLine": 185, "startColumn": 16, - "endLine": 184, + "endLine": 185, "endColumn": 22, "byteLength": 6 } @@ -23960,9 +24459,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 165, + "startLine": 166, "startColumn": 30, - "endLine": 165, + "endLine": 166, "endColumn": 53, "byteLength": 23 } @@ -23983,9 +24482,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 166, + "startLine": 167, "startColumn": 23, - "endLine": 166, + "endLine": 167, "endColumn": 47, "byteLength": 24 } @@ -24006,9 +24505,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 167, + "startLine": 168, "startColumn": 23, - "endLine": 167, + "endLine": 168, "endColumn": 51, "byteLength": 28 } @@ -24029,9 +24528,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 175, + "startLine": 176, "startColumn": 27, - "endLine": 175, + "endLine": 176, "endColumn": 41, "byteLength": 14 } @@ -24052,9 +24551,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 171, + "startLine": 172, "startColumn": 25, - "endLine": 171, + "endLine": 172, "endColumn": 40, "byteLength": 15 } @@ -24075,9 +24574,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 174, + "startLine": 175, "startColumn": 28, - "endLine": 174, + "endLine": 175, "endColumn": 43, "byteLength": 15 } @@ -24098,9 +24597,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 178, + "startLine": 179, "startColumn": 28, - "endLine": 178, + "endLine": 179, "endColumn": 48, "byteLength": 20 } @@ -24121,9 +24620,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 179, + "startLine": 180, "startColumn": 34, - "endLine": 179, + "endLine": 180, "endColumn": 54, "byteLength": 20 } @@ -24144,9 +24643,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 180, + "startLine": 181, "startColumn": 29, - "endLine": 180, + "endLine": 181, "endColumn": 60, "byteLength": 31 } @@ -24167,9 +24666,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 168, + "startLine": 169, "startColumn": 10, - "endLine": 168, + "endLine": 169, "endColumn": 17, "byteLength": 7 } @@ -24190,9 +24689,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 184, + "startLine": 185, "startColumn": 16, - "endLine": 184, + "endLine": 185, "endColumn": 22, "byteLength": 6 } @@ -24213,9 +24712,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 176, + "startLine": 177, "startColumn": 12, - "endLine": 176, + "endLine": 177, "endColumn": 19, "byteLength": 7 } @@ -24238,9 +24737,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 168, + "startLine": 169, "startColumn": 10, - "endLine": 168, + "endLine": 169, "endColumn": 17, "byteLength": 7 } @@ -24263,9 +24762,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 169, + "startLine": 170, "startColumn": 10, - "endLine": 169, + "endLine": 170, "endColumn": 17, "byteLength": 7 } @@ -24288,9 +24787,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 172, + "startLine": 173, "startColumn": 12, - "endLine": 172, + "endLine": 173, "endColumn": 19, "byteLength": 7 } @@ -24313,9 +24812,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 176, + "startLine": 177, "startColumn": 12, - "endLine": 176, + "endLine": 177, "endColumn": 19, "byteLength": 7 } @@ -24338,9 +24837,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 177, + "startLine": 178, "startColumn": 12, - "endLine": 177, + "endLine": 178, "endColumn": 19, "byteLength": 7 } @@ -24361,9 +24860,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 184, + "startLine": 185, "startColumn": 16, - "endLine": 184, + "endLine": 185, "endColumn": 22, "byteLength": 6 } @@ -24384,9 +24883,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 184, + "startLine": 185, "startColumn": 16, - "endLine": 184, + "endLine": 185, "endColumn": 22, "byteLength": 6 } @@ -24407,9 +24906,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 160, + "startLine": 161, "startColumn": 19, - "endLine": 160, + "endLine": 161, "endColumn": 26, "byteLength": 7 } @@ -24430,9 +24929,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 160, + "startLine": 161, "startColumn": 19, - "endLine": 160, + "endLine": 161, "endColumn": 26, "byteLength": 7 } @@ -24455,9 +24954,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 160, + "startLine": 161, "startColumn": 19, - "endLine": 160, + "endLine": 161, "endColumn": 26, "byteLength": 7 } @@ -24478,9 +24977,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 142, + "startLine": 143, "startColumn": 30, - "endLine": 142, + "endLine": 143, "endColumn": 53, "byteLength": 23 } @@ -24501,9 +25000,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 143, + "startLine": 144, "startColumn": 23, - "endLine": 143, + "endLine": 144, "endColumn": 47, "byteLength": 24 } @@ -24524,9 +25023,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 151, + "startLine": 152, "startColumn": 27, - "endLine": 151, + "endLine": 152, "endColumn": 41, "byteLength": 14 } @@ -24547,9 +25046,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 147, + "startLine": 148, "startColumn": 25, - "endLine": 147, + "endLine": 148, "endColumn": 40, "byteLength": 15 } @@ -24570,9 +25069,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 150, + "startLine": 151, "startColumn": 28, - "endLine": 150, + "endLine": 151, "endColumn": 43, "byteLength": 15 } @@ -24593,9 +25092,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 154, + "startLine": 155, "startColumn": 28, - "endLine": 154, + "endLine": 155, "endColumn": 48, "byteLength": 20 } @@ -24616,9 +25115,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 155, + "startLine": 156, "startColumn": 34, - "endLine": 155, + "endLine": 156, "endColumn": 54, "byteLength": 20 } @@ -24639,9 +25138,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 156, + "startLine": 157, "startColumn": 29, - "endLine": 156, + "endLine": 157, "endColumn": 60, "byteLength": 31 } @@ -24662,9 +25161,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 144, + "startLine": 145, "startColumn": 10, - "endLine": 144, + "endLine": 145, "endColumn": 17, "byteLength": 7 } @@ -24685,9 +25184,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 160, + "startLine": 161, "startColumn": 19, - "endLine": 160, + "endLine": 161, "endColumn": 26, "byteLength": 7 } @@ -24708,9 +25207,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 152, + "startLine": 153, "startColumn": 12, - "endLine": 152, + "endLine": 153, "endColumn": 19, "byteLength": 7 } @@ -24733,9 +25232,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 144, + "startLine": 145, "startColumn": 10, - "endLine": 144, + "endLine": 145, "endColumn": 17, "byteLength": 7 } @@ -24758,9 +25257,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 145, + "startLine": 146, "startColumn": 10, - "endLine": 145, + "endLine": 146, "endColumn": 17, "byteLength": 7 } @@ -24783,9 +25282,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 148, + "startLine": 149, "startColumn": 12, - "endLine": 148, + "endLine": 149, "endColumn": 19, "byteLength": 7 } @@ -24808,9 +25307,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 152, + "startLine": 153, "startColumn": 12, - "endLine": 152, + "endLine": 153, "endColumn": 19, "byteLength": 7 } @@ -24833,9 +25332,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 153, + "startLine": 154, "startColumn": 12, - "endLine": 153, + "endLine": 154, "endColumn": 19, "byteLength": 7 } @@ -24856,9 +25355,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 160, + "startLine": 161, "startColumn": 19, - "endLine": 160, + "endLine": 161, "endColumn": 26, "byteLength": 7 } @@ -24879,9 +25378,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 160, + "startLine": 161, "startColumn": 19, - "endLine": 160, + "endLine": 161, "endColumn": 26, "byteLength": 7 } @@ -24902,9 +25401,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 209, + "startLine": 210, "startColumn": 21, - "endLine": 209, + "endLine": 210, "endColumn": 28, "byteLength": 7 } @@ -24925,9 +25424,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 209, + "startLine": 210, "startColumn": 21, - "endLine": 209, + "endLine": 210, "endColumn": 28, "byteLength": 7 } @@ -24950,9 +25449,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 209, + "startLine": 210, "startColumn": 21, - "endLine": 209, + "endLine": 210, "endColumn": 28, "byteLength": 7 } @@ -24973,9 +25472,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 190, + "startLine": 191, "startColumn": 30, - "endLine": 190, + "endLine": 191, "endColumn": 53, "byteLength": 23 } @@ -24996,9 +25495,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 191, + "startLine": 192, "startColumn": 23, - "endLine": 191, + "endLine": 192, "endColumn": 47, "byteLength": 24 } @@ -25019,9 +25518,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 192, + "startLine": 193, "startColumn": 23, - "endLine": 192, + "endLine": 193, "endColumn": 51, "byteLength": 28 } @@ -25042,9 +25541,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 200, + "startLine": 201, "startColumn": 27, - "endLine": 200, + "endLine": 201, "endColumn": 41, "byteLength": 14 } @@ -25065,9 +25564,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 196, + "startLine": 197, "startColumn": 25, - "endLine": 196, + "endLine": 197, "endColumn": 40, "byteLength": 15 } @@ -25088,9 +25587,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 199, + "startLine": 200, "startColumn": 28, - "endLine": 199, + "endLine": 200, "endColumn": 43, "byteLength": 15 } @@ -25111,9 +25610,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 203, + "startLine": 204, "startColumn": 28, - "endLine": 203, + "endLine": 204, "endColumn": 48, "byteLength": 20 } @@ -25134,9 +25633,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 204, + "startLine": 205, "startColumn": 34, - "endLine": 204, + "endLine": 205, "endColumn": 54, "byteLength": 20 } @@ -25157,9 +25656,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 205, + "startLine": 206, "startColumn": 29, - "endLine": 205, + "endLine": 206, "endColumn": 60, "byteLength": 31 } @@ -25180,9 +25679,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 193, + "startLine": 194, "startColumn": 10, - "endLine": 193, + "endLine": 194, "endColumn": 17, "byteLength": 7 } @@ -25203,9 +25702,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 209, + "startLine": 210, "startColumn": 21, - "endLine": 209, + "endLine": 210, "endColumn": 28, "byteLength": 7 } @@ -25226,9 +25725,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 201, + "startLine": 202, "startColumn": 12, - "endLine": 201, + "endLine": 202, "endColumn": 19, "byteLength": 7 } @@ -25251,9 +25750,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 193, + "startLine": 194, "startColumn": 10, - "endLine": 193, + "endLine": 194, "endColumn": 17, "byteLength": 7 } @@ -25276,9 +25775,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 194, + "startLine": 195, "startColumn": 10, - "endLine": 194, + "endLine": 195, "endColumn": 17, "byteLength": 7 } @@ -25301,9 +25800,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 197, + "startLine": 198, "startColumn": 12, - "endLine": 197, + "endLine": 198, "endColumn": 19, "byteLength": 7 } @@ -25326,9 +25825,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 201, + "startLine": 202, "startColumn": 12, - "endLine": 201, + "endLine": 202, "endColumn": 19, "byteLength": 7 } @@ -25351,9 +25850,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 202, + "startLine": 203, "startColumn": 12, - "endLine": 202, + "endLine": 203, "endColumn": 19, "byteLength": 7 } @@ -25374,9 +25873,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 209, + "startLine": 210, "startColumn": 21, - "endLine": 209, + "endLine": 210, "endColumn": 28, "byteLength": 7 } @@ -25397,9 +25896,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 209, + "startLine": 210, "startColumn": 21, - "endLine": 209, + "endLine": 210, "endColumn": 28, "byteLength": 7 } @@ -25420,9 +25919,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 234, + "startLine": 235, "startColumn": 25, - "endLine": 234, + "endLine": 235, "endColumn": 32, "byteLength": 7 } @@ -25443,9 +25942,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 234, + "startLine": 235, "startColumn": 25, - "endLine": 234, + "endLine": 235, "endColumn": 32, "byteLength": 7 } @@ -25468,9 +25967,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 234, + "startLine": 235, "startColumn": 25, - "endLine": 234, + "endLine": 235, "endColumn": 32, "byteLength": 7 } @@ -25491,9 +25990,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 215, + "startLine": 216, "startColumn": 30, - "endLine": 215, + "endLine": 216, "endColumn": 53, "byteLength": 23 } @@ -25514,9 +26013,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 216, + "startLine": 217, "startColumn": 23, - "endLine": 216, + "endLine": 217, "endColumn": 47, "byteLength": 24 } @@ -25537,9 +26036,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 217, + "startLine": 218, "startColumn": 23, - "endLine": 217, + "endLine": 218, "endColumn": 51, "byteLength": 28 } @@ -25560,9 +26059,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 225, + "startLine": 226, "startColumn": 27, - "endLine": 225, + "endLine": 226, "endColumn": 41, "byteLength": 14 } @@ -25583,9 +26082,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 221, + "startLine": 222, "startColumn": 25, - "endLine": 221, + "endLine": 222, "endColumn": 40, "byteLength": 15 } @@ -25606,9 +26105,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 224, + "startLine": 225, "startColumn": 28, - "endLine": 224, + "endLine": 225, "endColumn": 43, "byteLength": 15 } @@ -25629,9 +26128,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 228, + "startLine": 229, "startColumn": 28, - "endLine": 228, + "endLine": 229, "endColumn": 48, "byteLength": 20 } @@ -25652,9 +26151,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 229, + "startLine": 230, "startColumn": 34, - "endLine": 229, + "endLine": 230, "endColumn": 54, "byteLength": 20 } @@ -25675,9 +26174,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 230, + "startLine": 231, "startColumn": 29, - "endLine": 230, + "endLine": 231, "endColumn": 60, "byteLength": 31 } @@ -25698,9 +26197,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 218, + "startLine": 219, "startColumn": 10, - "endLine": 218, + "endLine": 219, "endColumn": 17, "byteLength": 7 } @@ -25721,9 +26220,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 234, + "startLine": 235, "startColumn": 25, - "endLine": 234, + "endLine": 235, "endColumn": 32, "byteLength": 7 } @@ -25744,9 +26243,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 226, + "startLine": 227, "startColumn": 12, - "endLine": 226, + "endLine": 227, "endColumn": 19, "byteLength": 7 } @@ -25769,9 +26268,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 218, + "startLine": 219, "startColumn": 10, - "endLine": 218, + "endLine": 219, "endColumn": 17, "byteLength": 7 } @@ -25794,9 +26293,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 219, + "startLine": 220, "startColumn": 10, - "endLine": 219, + "endLine": 220, "endColumn": 17, "byteLength": 7 } @@ -25819,9 +26318,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 222, + "startLine": 223, "startColumn": 12, - "endLine": 222, + "endLine": 223, "endColumn": 19, "byteLength": 7 } @@ -25844,9 +26343,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 226, + "startLine": 227, "startColumn": 12, - "endLine": 226, + "endLine": 227, "endColumn": 19, "byteLength": 7 } @@ -25869,9 +26368,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 227, + "startLine": 228, "startColumn": 12, - "endLine": 227, + "endLine": 228, "endColumn": 19, "byteLength": 7 } @@ -25892,9 +26391,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 234, + "startLine": 235, "startColumn": 25, - "endLine": 234, + "endLine": 235, "endColumn": 32, "byteLength": 7 } @@ -25915,9 +26414,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 234, + "startLine": 235, "startColumn": 25, - "endLine": 234, + "endLine": 235, "endColumn": 32, "byteLength": 7 } @@ -25938,9 +26437,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 259, + "startLine": 260, "startColumn": 30, - "endLine": 259, + "endLine": 260, "endColumn": 38, "byteLength": 8 } @@ -25961,9 +26460,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 259, + "startLine": 260, "startColumn": 30, - "endLine": 259, + "endLine": 260, "endColumn": 38, "byteLength": 8 } @@ -25986,9 +26485,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 259, + "startLine": 260, "startColumn": 30, - "endLine": 259, + "endLine": 260, "endColumn": 38, "byteLength": 8 } @@ -26009,9 +26508,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 240, + "startLine": 241, "startColumn": 30, - "endLine": 240, + "endLine": 241, "endColumn": 53, "byteLength": 23 } @@ -26032,9 +26531,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 241, + "startLine": 242, "startColumn": 23, - "endLine": 241, + "endLine": 242, "endColumn": 47, "byteLength": 24 } @@ -26055,9 +26554,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 242, + "startLine": 243, "startColumn": 23, - "endLine": 242, + "endLine": 243, "endColumn": 51, "byteLength": 28 } @@ -26078,9 +26577,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 250, + "startLine": 251, "startColumn": 27, - "endLine": 250, + "endLine": 251, "endColumn": 41, "byteLength": 14 } @@ -26101,9 +26600,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 246, + "startLine": 247, "startColumn": 25, - "endLine": 246, + "endLine": 247, "endColumn": 40, "byteLength": 15 } @@ -26124,9 +26623,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 249, + "startLine": 250, "startColumn": 28, - "endLine": 249, + "endLine": 250, "endColumn": 43, "byteLength": 15 } @@ -26147,9 +26646,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 253, + "startLine": 254, "startColumn": 28, - "endLine": 253, + "endLine": 254, "endColumn": 48, "byteLength": 20 } @@ -26170,9 +26669,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 254, + "startLine": 255, "startColumn": 34, - "endLine": 254, + "endLine": 255, "endColumn": 54, "byteLength": 20 } @@ -26193,9 +26692,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 255, + "startLine": 256, "startColumn": 29, - "endLine": 255, + "endLine": 256, "endColumn": 60, "byteLength": 31 } @@ -26216,9 +26715,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 243, + "startLine": 244, "startColumn": 10, - "endLine": 243, + "endLine": 244, "endColumn": 17, "byteLength": 7 } @@ -26239,9 +26738,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 259, + "startLine": 260, "startColumn": 30, - "endLine": 259, + "endLine": 260, "endColumn": 38, "byteLength": 8 } @@ -26262,9 +26761,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 251, + "startLine": 252, "startColumn": 12, - "endLine": 251, + "endLine": 252, "endColumn": 19, "byteLength": 7 } @@ -26287,9 +26786,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 243, + "startLine": 244, "startColumn": 10, - "endLine": 243, + "endLine": 244, "endColumn": 17, "byteLength": 7 } @@ -26312,9 +26811,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 244, + "startLine": 245, "startColumn": 10, - "endLine": 244, + "endLine": 245, "endColumn": 17, "byteLength": 7 } @@ -26337,9 +26836,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 247, + "startLine": 248, "startColumn": 12, - "endLine": 247, + "endLine": 248, "endColumn": 19, "byteLength": 7 } @@ -26362,9 +26861,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 251, + "startLine": 252, "startColumn": 12, - "endLine": 251, + "endLine": 252, "endColumn": 19, "byteLength": 7 } @@ -26387,9 +26886,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 252, + "startLine": 253, "startColumn": 12, - "endLine": 252, + "endLine": 253, "endColumn": 19, "byteLength": 7 } @@ -26410,9 +26909,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 259, + "startLine": 260, "startColumn": 30, - "endLine": 259, + "endLine": 260, "endColumn": 38, "byteLength": 8 } @@ -26433,9 +26932,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 259, + "startLine": 260, "startColumn": 30, - "endLine": 259, + "endLine": 260, "endColumn": 38, "byteLength": 8 } @@ -26598,9 +27097,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 563, + "startLine": 564, "startColumn": 11, - "endLine": 563, + "endLine": 564, "endColumn": 17, "byteLength": 6 } @@ -26621,9 +27120,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 560, + "startLine": 561, "startColumn": 5, - "endLine": 560, + "endLine": 561, "endColumn": 51, "byteLength": 46 } @@ -26644,9 +27143,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 563, + "startLine": 564, "startColumn": 11, - "endLine": 563, + "endLine": 564, "endColumn": 17, "byteLength": 6 } @@ -26669,9 +27168,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 561, + "startLine": 562, "startColumn": 10, - "endLine": 561, + "endLine": 562, "endColumn": 17, "byteLength": 7 } @@ -26692,9 +27191,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 550, + "startLine": 551, "startColumn": 11, - "endLine": 550, + "endLine": 551, "endColumn": 19, "byteLength": 8 } @@ -26715,9 +27214,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 545, + "startLine": 546, "startColumn": 23, - "endLine": 545, + "endLine": 546, "endColumn": 46, "byteLength": 23 } @@ -26738,9 +27237,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 548, + "startLine": 549, "startColumn": 30, - "endLine": 548, + "endLine": 549, "endColumn": 59, "byteLength": 29 } @@ -26761,9 +27260,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 546, + "startLine": 547, "startColumn": 10, - "endLine": 546, + "endLine": 547, "endColumn": 17, "byteLength": 7 } @@ -26786,9 +27285,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 546, + "startLine": 547, "startColumn": 10, - "endLine": 546, + "endLine": 547, "endColumn": 17, "byteLength": 7 } @@ -26811,9 +27310,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 546, + "startLine": 547, "startColumn": 19, - "endLine": 546, + "endLine": 547, "endColumn": 32, "byteLength": 13 } @@ -26834,9 +27333,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 694, + "startLine": 695, "startColumn": 14, - "endLine": 694, + "endLine": 695, "endColumn": 22, "byteLength": 8 } @@ -26857,9 +27356,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 690, + "startLine": 691, "startColumn": 23, - "endLine": 690, + "endLine": 691, "endColumn": 42, "byteLength": 19 } @@ -26880,9 +27379,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 691, + "startLine": 692, "startColumn": 10, - "endLine": 691, + "endLine": 692, "endColumn": 17, "byteLength": 7 } @@ -26905,9 +27404,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 691, + "startLine": 692, "startColumn": 10, - "endLine": 691, + "endLine": 692, "endColumn": 17, "byteLength": 7 } @@ -26930,9 +27429,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 692, + "startLine": 693, "startColumn": 10, - "endLine": 692, + "endLine": 693, "endColumn": 21, "byteLength": 11 } @@ -26953,9 +27452,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 676, + "startLine": 677, "startColumn": 11, - "endLine": 676, + "endLine": 677, "endColumn": 17, "byteLength": 6 } @@ -26976,9 +27475,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 673, + "startLine": 674, "startColumn": 10, - "endLine": 673, + "endLine": 674, "endColumn": 17, "byteLength": 7 } @@ -27001,9 +27500,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 673, + "startLine": 674, "startColumn": 10, - "endLine": 673, + "endLine": 674, "endColumn": 17, "byteLength": 7 } @@ -27026,9 +27525,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 674, + "startLine": 675, "startColumn": 10, - "endLine": 674, + "endLine": 675, "endColumn": 17, "byteLength": 7 } @@ -27051,9 +27550,9 @@ "uriBaseId": "FRAMAC_SHARE" }, "region": { - "startLine": 674, + "startLine": 675, "startColumn": 19, - "endLine": 674, + "endLine": 675, "endColumn": 36, "byteLength": 17 } diff --git a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle index b2712cff667ac3c6ab0c9bf6ff7ba44d740aca7d..25efd1adf49148194cafd20f8e537c4a6edf7899 100644 --- a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle @@ -31,6 +31,7 @@ __malloc_pack_l20[0..5] ∈ {42} [6] ∈ {0} /* Generated by Frama-C */ +#include "errno.h" #include "stdarg.h" #include "stdlib.h" int *pack(int first, void * const *__va_params) diff --git a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle index c5eaf34085b23ce96653ca65b5e9ae340727b0d2..2092b713a5790e49bf7d2c478ff41f0dcd0f8580 100644 --- a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle +++ b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle @@ -31,6 +31,7 @@ __malloc_pack_l21[0..5] ∈ {42} [6] ∈ {0} /* Generated by Frama-C */ +#include "errno.h" #include "stdarg.h" #include "stdlib.h" int *pack(int first, void * const *__va_params) diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle index 5917ee76650ab412cc1d5db21f025f7352a6fbc6..0c0e75bda644384e9c87aad58541a0f8a1c7b8bb 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle @@ -1,10 +1,10 @@ # frama-c -wp [...] [kernel] Parsing terminates_call_options.c (with preprocessing) [wp] Running WP plugin... -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:510: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:511: Warning: Neither code nor explicit terminates for function exit, generating default clauses. See -generated-spec-* options for more info -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:641: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:642: Warning: Neither code nor explicit exits and terminates for function div, generating default clauses. See -generated-spec-* options for more info [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle index cd868c1ddd7a100294d87c9fa4536638552e99ae..907d765fcb069c60eb99c128520a688baadd064f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle @@ -4,10 +4,10 @@ [kernel:annot:missing-spec] terminates_call_options.c:17: Warning: Neither code nor explicit exits and terminates for function declaration, generating default clauses. See -generated-spec-* options for more info -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:510: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:511: Warning: Neither code nor explicit terminates for function exit, generating default clauses. See -generated-spec-* options for more info -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:641: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:642: Warning: Neither code nor explicit exits and terminates for function div, generating default clauses. See -generated-spec-* options for more info [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle index 7f72267fc093e8af037eae5998e193ca9af16160..be2f82c65143796f81fa17eb5d906dd11203ebdd 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle @@ -1,10 +1,10 @@ # frama-c -wp [...] [kernel] Parsing terminates_call_options.c (with preprocessing) [wp] Running WP plugin... -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:510: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:511: Warning: Neither code nor explicit terminates for function exit, generating default clauses. See -generated-spec-* options for more info -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:641: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:642: Warning: Neither code nor explicit exits and terminates for function div, generating default clauses. See -generated-spec-* options for more info [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle index 637741c47d24a498b1369bc7ba364e73029e475a..c0b8e8f68afae083a33b1559023f7ae97d111f5c 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle @@ -4,10 +4,10 @@ [kernel:annot:missing-spec] terminates_call_options.c:17: Warning: Neither code nor explicit exits and terminates for function declaration, generating default clauses. See -generated-spec-* options for more info -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:510: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:511: Warning: Neither code nor explicit terminates for function exit, generating default clauses. See -generated-spec-* options for more info -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:641: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:642: Warning: Neither code nor explicit exits and terminates for function div, generating default clauses. See -generated-spec-* options for more info [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle index e0dd37332643a2304b8c6f1d2dc73dda92693044..3ffda2bbd573ca3eacf2c0cac5653c23459e01b5 100644 --- a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle @@ -1,7 +1,7 @@ # frama-c -wp [...] [kernel] Parsing issue-684-exit.c (with preprocessing) [wp] Running WP plugin... -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:510: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:511: Warning: Neither code nor explicit terminates for function exit, generating default clauses. See -generated-spec-* options for more info [wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle index 1709f08e56244ff4a53a20f3863bed602753fd27..298c37684c6d07ccbcef188616124cb1b7e72528 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle @@ -1,7 +1,7 @@ # frama-c -wp [...] [kernel] Parsing issue-684-exit.c (with preprocessing) [wp] Running WP plugin... -[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:510: Warning: +[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:511: Warning: Neither code nor explicit terminates for function exit, generating default clauses. See -generated-spec-* options for more info [wp] Warning: Missing RTE guards diff --git a/tests/builtins/oracle/free.res.oracle b/tests/builtins/oracle/free.res.oracle index c8b839ed69f75b41023e2da4b9148bc1b628e109..36697aa13a32d1dfdd32eec38ddf20b09ecdb3aa 100644 --- a/tests/builtins/oracle/free.res.oracle +++ b/tests/builtins/oracle/free.res.oracle @@ -14,6 +14,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} diff --git a/tests/builtins/oracle/linked_list.0.res.oracle b/tests/builtins/oracle/linked_list.0.res.oracle index 4477e26a27e40b3b07003538f1959d3e85d1f751..45987fd11dcf676e5b53cafd650180b2d135d280 100644 --- a/tests/builtins/oracle/linked_list.0.res.oracle +++ b/tests/builtins/oracle/linked_list.0.res.oracle @@ -44,7 +44,7 @@ ==END OF DUMP== [eva] computing for function malloc <- main. Called from linked_list.c:41. -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:394: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:395: Warning: function malloc, behavior allocation: postcondition 'allocation' got status unknown. [eva] Recording results for malloc [eva] Done for function malloc diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle index c97ebeb2a70161b6c360d6cb8bf94962bf92fb3f..488273ab10d70800ebcb23b96d034502714116f9 100644 --- a/tests/builtins/oracle/linked_list.1.res.oracle +++ b/tests/builtins/oracle/linked_list.1.res.oracle @@ -44,7 +44,7 @@ ==END OF DUMP== [eva] computing for function malloc <- main. Called from linked_list.c:41. -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:394: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:395: Warning: function malloc, behavior allocation: postcondition 'allocation' got status unknown. [eva] Recording results for malloc [eva] Done for function malloc diff --git a/tests/builtins/oracle/linked_list.2.res.oracle b/tests/builtins/oracle/linked_list.2.res.oracle index c5cd47271ad912fdd4c58c84be6df348d2359148..ae7d0058ec1f75eec94c984ff2ce8a5d06214dc6 100644 --- a/tests/builtins/oracle/linked_list.2.res.oracle +++ b/tests/builtins/oracle/linked_list.2.res.oracle @@ -44,7 +44,7 @@ ==END OF DUMP== [eva] computing for function malloc <- main. Called from linked_list.c:41. -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:394: Warning: +[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:395: Warning: function malloc, behavior allocation: postcondition 'allocation' got status unknown. [eva] Recording results for malloc [eva] Done for function malloc diff --git a/tests/builtins/oracle/malloc-size-zero.0.res.oracle b/tests/builtins/oracle/malloc-size-zero.0.res.oracle index 75f6a2b0f5fce129ae4368c77f998a5d9a82f817..6fac8f66d523b1a1c715bea58f484fc70f929acb 100644 --- a/tests/builtins/oracle/malloc-size-zero.0.res.oracle +++ b/tests/builtins/oracle/malloc-size-zero.0.res.oracle @@ -49,6 +49,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} diff --git a/tests/builtins/oracle/malloc-size-zero.1.res.oracle b/tests/builtins/oracle/malloc-size-zero.1.res.oracle index 1b40f39f17564e2c61cf01007a6adbc299bed28d..bb9cb15cfb4330ef2102509314f2f684c5e619a9 100644 --- a/tests/builtins/oracle/malloc-size-zero.1.res.oracle +++ b/tests/builtins/oracle/malloc-size-zero.1.res.oracle @@ -31,6 +31,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} diff --git a/tests/builtins/oracle/realloc.res.oracle b/tests/builtins/oracle/realloc.res.oracle index 0b8621e9f5f51c69c0798c416f1e32a45a2f812d..cedab8abdd07ec2d95dbfa3c0e4a34dcdfc84c3f 100644 --- a/tests/builtins/oracle/realloc.res.oracle +++ b/tests/builtins/oracle/realloc.res.oracle @@ -12,6 +12,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -41,6 +42,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -87,6 +89,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -129,6 +132,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -162,6 +166,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -227,6 +232,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -283,6 +289,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -345,6 +352,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -375,6 +383,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -440,6 +449,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -467,6 +477,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -505,6 +516,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -542,6 +554,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -580,6 +593,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -610,6 +624,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} diff --git a/tests/builtins/oracle/realloc_multiple.0.res.oracle b/tests/builtins/oracle/realloc_multiple.0.res.oracle index 6413ab4bdc624d8087dc489754719c3a080a95bd..fb44822b047b19a0d570d183cd3f921fa2db2a0c 100644 --- a/tests/builtins/oracle/realloc_multiple.0.res.oracle +++ b/tests/builtins/oracle/realloc_multiple.0.res.oracle @@ -20,6 +20,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -56,6 +57,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -105,6 +107,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -143,6 +146,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -197,6 +201,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -239,6 +244,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -281,6 +287,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} diff --git a/tests/builtins/oracle/realloc_multiple.1.res.oracle b/tests/builtins/oracle/realloc_multiple.1.res.oracle index 7a06abde7f246fa1d1ac646d47857991cd28a32e..c076efb3a39138ab0e7e59070fbf2c4885bea4cd 100644 --- a/tests/builtins/oracle/realloc_multiple.1.res.oracle +++ b/tests/builtins/oracle/realloc_multiple.1.res.oracle @@ -28,6 +28,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -64,6 +65,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -95,6 +97,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -150,6 +153,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -188,6 +192,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -223,6 +228,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -281,6 +287,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -327,6 +334,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -369,6 +377,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} diff --git a/tests/builtins/oracle/strnlen.res.oracle b/tests/builtins/oracle/strnlen.res.oracle index 009fb074190f6d18180ff27c9de5819dd9d5b0f9..5d22fb90327d86dbb7309bb4794a47c8e2588664 100644 --- a/tests/builtins/oracle/strnlen.res.oracle +++ b/tests/builtins/oracle/strnlen.res.oracle @@ -36,6 +36,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} diff --git a/tests/builtins/oracle_gauges/realloc.res.oracle b/tests/builtins/oracle_gauges/realloc.res.oracle index 317aba47d1df8261a94c9a7e59085491fc885220..b61ec8f618bcc743656c990a8338abba067675e6 100644 --- a/tests/builtins/oracle_gauges/realloc.res.oracle +++ b/tests/builtins/oracle_gauges/realloc.res.oracle @@ -1,4 +1,4 @@ -632a633,969 +647a648,996 > [eva] realloc.c:152: Call to builtin realloc > [eva:malloc] bases_to_realloc: {__realloc_w_main10_l152} > [eva:malloc] realloc.c:152: weak free on bases: {__realloc_w_main10_l152} @@ -7,6 +7,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -35,6 +36,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -63,6 +65,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -91,6 +94,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -119,6 +123,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -147,6 +152,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -175,6 +181,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -203,6 +210,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -231,6 +239,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -260,6 +269,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -288,6 +298,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -316,6 +327,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -336,7 +348,7 @@ > __realloc_w_main10_l152[0] ∈ {4} > [1] ∈ UNINITIALIZED > ==END OF DUMP== -699a1037,1101 +714a1064,1128 > [eva] realloc.c:167: Call to builtin reallocarray > [eva] realloc.c:167: Call to builtin reallocarray > [eva] computing for function Frama_C_interval <- main11 <- main. @@ -402,7 +414,7 @@ > [eva:malloc] bases_to_realloc: {} > [eva:malloc] realloc.c:171: strong free on bases: {} > [eva] realloc.c:172: Frama_C_show_each_p: {{ NULL ; &__realloc_w_main11_l171 }} -767,768c1169,1171 +782,783c1196,1198 < p ∈ {{ NULL ; &__malloc_main11_l160 ; (int *)&__realloc_main11_l171 }} < q ∈ {0} or UNINITIALIZED or ESCAPINGADDR --- diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index d08401adb21799fa5128e980cb7a661e5dd98443..db5aac49397b7662d77d97b276db56dac4a039e9 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -7194,21 +7194,36 @@ int posix_memalign(void **memptr, size_t alignment, size_t size) return_label: return __retres; } -/*@ requires valid_file_name: valid_read_string(file_name); +/*@ requires + valid_file_name_or_null: + file_name ≡ \null ∨ valid_read_string(file_name); requires resolved_name_null_or_allocated: resolved_name ≡ \null ∨ \valid(resolved_name + (0 .. 4096 - 1)); - assigns __fc_heap_status, \result, *(resolved_name + (0 .. 4096 - 1)); + assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)), + *(resolved_name + (0 .. 4096 - 1)), __fc_errno; assigns __fc_heap_status \from (indirect: resolved_name), __fc_heap_status; - assigns \result + assigns *(\result + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: __fc_heap_status), (indirect: resolved_name), (indirect: *(file_name + (0 ..))); + assigns __fc_errno + \from (indirect: file_name), (indirect: *(file_name + (0 ..))), + (indirect: resolved_name), (indirect: __fc_heap_status); + + behavior null_file_name: + assumes null_file_name: file_name ≡ \null; + ensures null_result: \result ≡ \null; + ensures errno_set: __fc_errno ≡ 22; + assigns \result, __fc_errno; + assigns \result \from (indirect: file_name); + assigns __fc_errno \from (indirect: file_name); behavior allocate_resolved_name: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name ≡ \null; assumes can_allocate: is_allocable(4096); ensures allocation: \fresh{Old, Here}(\result,4096); @@ -7217,23 +7232,39 @@ int posix_memalign(void **memptr, size_t alignment, size_t size) assigns \result \from (indirect: __fc_heap_status); behavior not_enough_memory: + assumes valid_file_name: valid_read_string(file_name); assumes resolved_name_null: resolved_name ≡ \null; + assumes cannot_allocate: ¬is_allocable(4096); ensures null_result: \result ≡ \null; + ensures errno_set: __fc_errno ≡ 12; assigns \result; assigns \result \from \nothing; allocates \nothing; behavior resolved_name_buffer: + assumes valid_file_name: valid_read_string(file_name); assumes allocated_resolved_name_or_fail: \valid(resolved_name + (0 .. 4096 - 1)); - ensures valid_string_resolved_name: valid_string(\old(resolved_name)); + ensures + valid_string_resolved_name: + valid_string(\old(resolved_name)) ∧ + strlen(\old(resolved_name)) < 4096; ensures resolved_result: \result ≡ \old(resolved_name); assigns \result, *(resolved_name + (0 .. 4096 - 1)); - assigns \result \from \nothing; + assigns \result \from resolved_name; assigns *(resolved_name + (0 .. 4096 - 1)) \from (indirect: *(file_name + (0 ..))); allocates \nothing; + + behavior filesystem_error: + assumes valid_file_name: valid_read_string(file_name); + ensures null_result: \result ≡ \null; + ensures errno_set: __fc_errno ∈ {13, 5, 40, 36, 2, 20}; + assigns \result, __fc_errno; + assigns \result \from (indirect: *(file_name + (0 ..))); + assigns __fc_errno \from (indirect: *(file_name + (0 ..))); + allocates \nothing; */ char *realpath(char const * restrict file_name, char * restrict resolved_name) { diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle index b690ae421776ff0d02c2d2880b6660d6d1d7a495..71ff8f9d0dd26170d780b01a42df3071ef8bc615 100644 --- a/tests/libc/oracle/stdio_c.res.oracle +++ b/tests/libc/oracle/stdio_c.res.oracle @@ -355,19 +355,19 @@ [eva] Done for function main [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function fgetc: - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] __retres ∈ [-1..255] [eva:final-states] Values at end of function fgets: - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] i ∈ [0..9] or UNINITIALIZED buf[0..8] ∈ [--..--] or UNINITIALIZED [9] ∈ {0} or UNINITIALIZED __retres ∈ {{ NULL ; &buf[0] }} [eva:final-states] Values at end of function getchar: - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] [eva:final-states] Values at end of function is_valid_mode: __retres ∈ {1} [eva:final-states] Values at end of function asprintf: @@ -381,14 +381,14 @@ [255] ∈ {0} or UNINITIALIZED [eva:final-states] Values at end of function fmemopen: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] buf ∈ {{ NULL ; (void *)&__malloc_fmemopen_l224 }} __retres ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }} [eva:final-states] Values at end of function getline: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] cur ∈ [0..2147483647] or UNINITIALIZED line ∈ {{ NULL ; &__malloc_w_getline_l73[0] ; &__realloc_w_getline_l104[0] }} @@ -399,8 +399,8 @@ [2147483646] ∈ {0} or UNINITIALIZED [eva:final-states] Values at end of function main: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] __fc_fopen[0..15] ∈ [--..--] __fc_initial_stdout.__fc_FILE_id ∈ {1} .__fc_FILE_data ∈ [--..--] diff --git a/tests/libc/oracle/stdlib_c.0.res.oracle b/tests/libc/oracle/stdlib_c.0.res.oracle index 9ff599dc085c9f48b9fa14583ac7546e0445be75..311025d26fd3425b42362fd4c546daeeab9dacc2 100644 --- a/tests/libc/oracle/stdlib_c.0.res.oracle +++ b/tests/libc/oracle/stdlib_c.0.res.oracle @@ -251,8 +251,8 @@ __retres ∈ {0; 12} [eva:final-states] Values at end of function realpath: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ; &__malloc_realpath_l224_0[0] }} @@ -267,14 +267,14 @@ [1..4095] ∈ [--..--] or UNINITIALIZED [eva:final-states] Values at end of function canonicalize_file_name: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] __malloc_realpath_l224_0[0] ∈ [--..--] [1..4095] ∈ [--..--] or UNINITIALIZED [eva:final-states] Values at end of function main: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] p ∈ {{ NULL ; &__calloc_main_l15 }} nmemb ∈ [1..4294967295] q ∈ {{ NULL ; &__calloc_main_l22[0] }} diff --git a/tests/libc/oracle/stdlib_c.1.res.oracle b/tests/libc/oracle/stdlib_c.1.res.oracle index a51658203071296339038439ba80c95d791b3a35..2dd89afee8614a150420fa948b006bd6257deeea 100644 --- a/tests/libc/oracle/stdlib_c.1.res.oracle +++ b/tests/libc/oracle/stdlib_c.1.res.oracle @@ -269,8 +269,8 @@ __retres ∈ {0} [eva:final-states] Values at end of function realpath: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ; &__malloc_realpath_l224_0[0] }} @@ -285,14 +285,14 @@ [1..4095] ∈ [--..--] or UNINITIALIZED [eva:final-states] Values at end of function canonicalize_file_name: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] __malloc_realpath_l224_0[0] ∈ [--..--] [1..4095] ∈ [--..--] or UNINITIALIZED [eva:final-states] Values at end of function main: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] p ∈ {{ &__calloc_main_l15 }} nmemb ∈ [1..4294967295] q ∈ {{ NULL ; &__calloc_main_l22[0] }} diff --git a/tests/libc/oracle/stdlib_c.2.res.oracle b/tests/libc/oracle/stdlib_c.2.res.oracle index a3e6c332dff595f880267430de635863197786ba..92a26b0f48e0b8e75ef495fdd9375ea676193e2a 100644 --- a/tests/libc/oracle/stdlib_c.2.res.oracle +++ b/tests/libc/oracle/stdlib_c.2.res.oracle @@ -223,8 +223,8 @@ __retres ∈ {0; 12} [eva:final-states] Values at end of function realpath: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] resolved_name ∈ {{ NULL ; &__malloc_main_l44[0] ; &__malloc_realpath_l224[0] ; &__malloc_realpath_l224_0[0] }} @@ -237,13 +237,13 @@ __malloc_realpath_l224_0[0..4095] ∈ [--..--] or UNINITIALIZED [eva:final-states] Values at end of function canonicalize_file_name: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] __malloc_realpath_l224_0[0..4095] ∈ [--..--] or UNINITIALIZED [eva:final-states] Values at end of function main: __fc_heap_status ∈ [--..--] - Frama_C_entropy_source ∈ [--..--] __fc_errno ∈ [--..--] + Frama_C_entropy_source ∈ [--..--] p ∈ {{ NULL ; (int *)&__malloc_calloc_l72 }} nmemb ∈ [1..4294967295] q ∈ {{ NULL ; (int *)&__malloc_calloc_l72_0 }} diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml index 7872b93e4ddd025199dbcedd0a868d908bc8909a..b7c9a0b07c9959a69a91f1bfb8a09b8decea31c6 100644 --- a/tests/misc/custom_machdep.yaml +++ b/tests/misc/custom_machdep.yaml @@ -58,6 +58,11 @@ sig_atomic_t: int time_t: long nsig: '' errno: + eacces: "13" + eloop: "5" + enametoolong: "11" + enoent: "2" + enotdir: "20" edom: "33" eilseq: "84" erange: "34" diff --git a/tests/misc/oracle/widen_hints2.1.res.oracle b/tests/misc/oracle/widen_hints2.1.res.oracle index d336955d5f6ef33760a1ce681c38acb78aacf0c6..12277beb5c43454428ed30d2fa9c81ae5e1049d8 100644 --- a/tests/misc/oracle/widen_hints2.1.res.oracle +++ b/tests/misc/oracle/widen_hints2.1.res.oracle @@ -1,5 +1,6 @@ [kernel] Parsing widen_hints2.c (with preprocessing) /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" int t[100]; int const x = 9; diff --git a/tests/rte/oracle/gnu_zero_length.res.oracle b/tests/rte/oracle/gnu_zero_length.res.oracle index 29ec3ac3638a2a2d2a18c44147143adca28f3e5a..a77759d8145613c42a073ef259dde9c7864c6c13 100644 --- a/tests/rte/oracle/gnu_zero_length.res.oracle +++ b/tests/rte/oracle/gnu_zero_length.res.oracle @@ -1,6 +1,7 @@ [kernel] Parsing gnu_zero_length.c (with preprocessing) [rte:annot] annotating function main /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct S { unsigned int length ; diff --git a/tests/spec/oracle/acsl_basic_allocator.res.oracle b/tests/spec/oracle/acsl_basic_allocator.res.oracle index 210a19385d1f4cde81b259ccbafc0a45e170ce20..e105feda9d20c0d5a70e0254b4fc37f3b2610d9f 100644 --- a/tests/spec/oracle/acsl_basic_allocator.res.oracle +++ b/tests/spec/oracle/acsl_basic_allocator.res.oracle @@ -1,5 +1,6 @@ [kernel] Parsing acsl_basic_allocator.c (with preprocessing) /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" enum _bool { false = 0, diff --git a/tests/spec/oracle/purse.res.oracle b/tests/spec/oracle/purse.res.oracle index 002f073dcb12c237a0e04ad38453d5fa063a34aa..e8c2819090a433333d50bf11eb350a14ee61cbc4 100644 --- a/tests/spec/oracle/purse.res.oracle +++ b/tests/spec/oracle/purse.res.oracle @@ -1,5 +1,6 @@ [kernel] Parsing purse.c (with preprocessing) /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct purse { int balance ; diff --git a/tests/syntax/oracle/exit.res.oracle b/tests/syntax/oracle/exit.res.oracle index 447a683f20bce22ffe923aca587a3cb43f43bb91..497136c44c5477f9adf7df0bf6afe5f6c2300dba 100644 --- a/tests/syntax/oracle/exit.res.oracle +++ b/tests/syntax/oracle/exit.res.oracle @@ -2,6 +2,7 @@ [kernel:CERT:MSC:37] exit.c:16: Warning: Body of function g falls-through. Adding a return statement /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" int volatile c; int f(void) diff --git a/tests/syntax/oracle/field-offsets.res.oracle b/tests/syntax/oracle/field-offsets.res.oracle index 6e37cb9d680c6945e9f63a5136185063840f491d..e0b50d77ac73d2667129a5085c0b96550aa8648f 100644 --- a/tests/syntax/oracle/field-offsets.res.oracle +++ b/tests/syntax/oracle/field-offsets.res.oracle @@ -1,5 +1,6 @@ [kernel] Parsing field-offsets.c (with preprocessing) /* Generated by Frama-C */ +#include "errno.h" #include "stdlib.h" struct st { int a ; /* bits 0 .. 31 */ diff --git a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle index 49e36a7bc9637e4de1698ba1149b6d9ff51b5f64..18dcb7d1e98d6f720629c92a70f5ca2cd640c702 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle @@ -4,6 +4,7 @@ [kernel] multiple_decls_contracts.c:10: Warning: dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 /* Generated by Frama-C */ +#include "errno.h" #include "stddef.h" #include "stdlib.h" #include "string.h" diff --git a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle index 50638f1cb54fb1518b7f2c83c791765c3baa4be6..ac9847f5831c67c3b5f6b3736a20adaeb2d167b5 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle @@ -4,6 +4,7 @@ [kernel] multiple_decls_contracts.c:10: Warning: dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 /* Generated by Frama-C */ +#include "errno.h" #include "stddef.h" #include "stdlib.h" #include "string.h" diff --git a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle index 364dd1fa5a6fd84939e45f8e31186c0869868d77..9f8c64afd7c2f00000e441724eb1050302ea192e 100644 --- a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle +++ b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle @@ -4,6 +4,7 @@ [kernel] multiple_decls_contracts.c:10: Warning: dropping duplicate def'n of func strdup at multiple_decls_contracts.c:10 in favor of that at multiple_decls_contracts.c:10 /* Generated by Frama-C */ +#include "errno.h" #include "stddef.h" #include "stdlib.h" #include "string.h" diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle index 4b7f0372dd0bb9eb70ae5e95a7ad3d083f33c162..71ec205b2f39796fa24f19f480c7b8a685727be1 100644 --- a/tests/value/oracle/gauges.res.oracle +++ b/tests/value/oracle/gauges.res.oracle @@ -338,6 +338,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -398,6 +399,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -457,6 +459,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -516,6 +519,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -581,6 +585,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} @@ -642,6 +647,7 @@ Frama_C_dump_each: # cvalue: __fc_heap_status ∈ [--..--] + __fc_errno ∈ [--..--] __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {2147483647} __fc_random48_init ∈ {0} diff --git a/tests/value/oracle_apron/gauges.res.oracle b/tests/value/oracle_apron/gauges.res.oracle index e39bbda029892bd78f7dccf1f133ee3e51428468..fd4e06736e9b52c1034bcc0c5c67a5abef42fe89 100644 --- a/tests/value/oracle_apron/gauges.res.oracle +++ b/tests/value/oracle_apron/gauges.res.oracle @@ -50,15 +50,15 @@ < Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647] --- > Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..598] -778c765 +784c771 < n ∈ [-2147483648..99] --- > n ∈ [-2147483547..99] -781c768 +787c774 < i ∈ [0..2147483647] --- > i ∈ [10..2147483647] -817c804 +823c810 < i ∈ [0..2147483647] --- > i ∈ [0..21] diff --git a/tests/value/oracle_equality/gauges.res.oracle b/tests/value/oracle_equality/gauges.res.oracle index 1375772daf32d94c39da70a45a329a0af7e75df1..e5c21b0c6810b8e5a50ea0dfc412e8a08fef0766 100644 --- a/tests/value/oracle_equality/gauges.res.oracle +++ b/tests/value/oracle_equality/gauges.res.oracle @@ -1,4 +1,4 @@ -716c716 +722c722 < (read 14 times, propagated 12 times) garbled mix of &{x; y} --- > (read 20 times, propagated 12 times) garbled mix of &{x; y} diff --git a/tests/value/oracle_gauges/gauges.res.oracle b/tests/value/oracle_gauges/gauges.res.oracle index 9d4462e029b227ddad11d18dc38dee160fab8cff..ded703ccb200de2e23ff4878b4831319fce4b033 100644 --- a/tests/value/oracle_gauges/gauges.res.oracle +++ b/tests/value/oracle_gauges/gauges.res.oracle @@ -97,43 +97,44 @@ < Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [0..2147483647] --- > Frama_C_show_each: {-593; -592; -591; -590; -589; -588}, [99..119] -394a359,362 +395a360,363 > # gauges: > V: [{[ p -> {{ &x }} > i -> {1} ]}] > s398: λ(0) -454a423,426 +456a425,428 > # gauges: > V: [{[ i -> {1} ]}] > s398: λ([0 .. 1]) > {[ i -> {1} ]} -513a486,489 +516a489,492 > # gauges: > V: [{[ i -> {1} ]}] > s398: λ([0 .. 2]) > {[ i -> {1} ]} -572a549,552 +576a553,556 > # gauges: > V: [{[ i -> {1} ]}] > s398: λ([0 .. 10]) > {[ i -> {1} ]} -637a618,622 +642a623,627 > # gauges: > V: [{[ p -> {{ &a }} > i -> {2} ]}] > s412: λ(0) > s411: λ(0) -698a684,688 +704a690,694 > # gauges: > V: [{[ i -> {2} ]}] > s412: λ(0) > s411: λ([0 .. 1]) > {[ i -> {0} ]} -700a691,818 +706a697,826 > [eva] gauges.c:325: > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -198,6 +199,7 @@ > Frama_C_dump_each: > # cvalue: > __fc_heap_status ∈ [--..--] +> __fc_errno ∈ [--..--] > __fc_random_counter ∈ [--..--] > __fc_rand_max ∈ {2147483647} > __fc_random48_init ∈ {0} @@ -258,55 +260,55 @@ > s411: λ([0 .. +oo]) > {[ i -> {0} ]} > ==END OF DUMP== -708a827,828 +714a835,836 > [eva] gauges.c:343: Call to builtin malloc > [eva] gauges.c:343: Call to builtin malloc -716c836 +722c844 < (read 14 times, propagated 12 times) garbled mix of &{x; y} --- > (read 12 times, propagated 11 times) garbled mix of &{x; y} -765,766c885,886 +771,772c893,894 < A ∈ {{ &A + [0..--],0%4 }} < B ∈ {{ &B + [0..--],0%4 }} --- > A ∈ {{ &A + [0..36],0%4 }} > B ∈ {{ &B + [0..36],0%4 }} -778c898 +784c906 < n ∈ [-2147483648..99] --- > n ∈ [-2147483547..99] -784c904 +790c912 < i ∈ {45; 46; 47; 48; 49; 50; 51} --- > i ∈ {45; 46; 47; 48} -790c910 +796c918 < i ∈ {-59; -58; -57; -56; -55; -54; -53} --- > i ∈ {-58; -57; -56; -55; -54; -53} -810c930 +816c938 < p ∈ {{ &u + [0..--],0%4 }} --- > p ∈ {{ &u + [0..400],0%4 }} -812c932 +818c940 < k ∈ [0..2147483647] --- > k ∈ [0..390] -817c937 +823c945 < i ∈ [0..2147483647] --- > i ∈ [0..21] -828,829c948,950 +834,835c956,958 < [1..9] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED < p ∈ {{ &y + [4..40],0%4 }} --- > [1..6] ∈ {4; 5; 6; 7; 8; 9} or UNINITIALIZED > [7..9] ∈ UNINITIALIZED > p ∈ {{ &y[7] }} -840c961 +846c969 < p ∈ {{ &T + [--..396],0%4 }} --- > p ∈ {{ &T + [-4..396],0%4 }} -845,849c966 +851,855c974 < n ∈ {0} < arr[0] ∈ {0} < [1] ∈ {-1} @@ -314,19 +316,19 @@ < p ∈ {{ &arr + [12..--],0%4 }} --- > NON TERMINATING FUNCTION -952a1070 +958a1078 > [from] Non-terminating function main8_aux (no dependencies) -975,976c1093,1094 +981,982c1101,1102 < p FROM p; A; B; n; p; A[0..9]; B[0..9] (and SELF) < \result FROM p; A; B; n; p; A[0..9]; B[0..9] --- > p FROM p; A; B; n; p; A[0..8]; B[0..8] (and SELF) > \result FROM p; A; B; n; p; A[0..8]; B[0..8] -1020c1138 +1026c1146 < NO EFFECTS --- > NON TERMINATING - NO EFFECTS -1054c1172 +1060c1180 < p; A[0..9]; B[0..9] --- > p; A[0..8]; B[0..8] diff --git a/tests/value/oracle_octagon/gauges.res.oracle b/tests/value/oracle_octagon/gauges.res.oracle index 1b2c6b235548585fb2d4218526d8c76fbed82258..acb804905135c794b100d1f8ccc6e91305a36faa 100644 --- a/tests/value/oracle_octagon/gauges.res.oracle +++ b/tests/value/oracle_octagon/gauges.res.oracle @@ -7,11 +7,11 @@ < [eva] gauges.c:218: Frama_C_show_each: < [eva:alarm] gauges.c:220: Warning: < signed overflow. assert -2147483648 ≤ n - 1; -767c760 +773c766 < numNonZero ∈ [-2147483648..8] --- > numNonZero ∈ {-1} -778c771 +784c777 < n ∈ [-2147483648..99] --- > n ∈ {-1}