diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index 15aeb15a7e15df807434d277080da0f9f506d694..f6304d722fd813a62af1879555e4b5c8b1af2bae 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -39,6 +39,14 @@ module Translate: sig
a single expression. *)
end
+module Functions: sig
+ module RTL: sig
+ val is_generated_name: string -> bool
+ (** @return [true] if the prefix of the given name indicates that it has been
+ generated by E-ACSL instrumentation (see [mk_gen_name] function). *)
+ end
+end
+
(** No function is directly exported: they are dynamically registered. *)
(*
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
index 02dcc62330216104b4a830f0aac14181c43ae900..a33b19b9e42be188eaabb80ce398cd9370323f9b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
@@ -4,8 +4,36 @@
char *__gen_e_acsl_literal_string;
extern int __e_acsl_sound_verdict;
+/*@ requires valid_nptr: \valid_read(nptr);
+ assigns \result;
+ assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
+ */
+int __gen_e_acsl_atoi(char const *nptr);
+
int a;
char *n = (char *)"134";
+/*@ requires valid_nptr: \valid_read(nptr);
+ assigns \result;
+ assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
+ */
+int __gen_e_acsl_atoi(char const *nptr)
+{
+ int __retres;
+ {
+ int __gen_e_acsl_valid_read;
+ __e_acsl_store_block((void *)(& nptr),(size_t)8);
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)nptr,
+ sizeof(char const),
+ (void *)nptr,
+ (void *)(& nptr));
+ __e_acsl_assert(__gen_e_acsl_valid_read,"Precondition","atoi",
+ "\\valid_read(nptr)","FRAMAC_SHARE/libc/stdlib.h",78);
+ }
+ __retres = atoi(nptr);
+ __e_acsl_delete_block((void *)(& nptr));
+ return __retres;
+}
+
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
index 97a3f9b0d6c2ae37cd984948fdca68ac1e710137..c26e98c393743890253261c4c622d4a19a38c11a 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
@@ -38,10 +38,176 @@ char *__gen_e_acsl_literal_string_17;
char *__gen_e_acsl_literal_string_18;
extern int __e_acsl_sound_verdict;
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
+void __gen_e_acsl_exit(int status);
+
+/*@ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result \from __fc_p_fopen;
+ */
+FILE *__gen_e_acsl_tmpfile(void);
+
+/*@ requires valid_stream: \valid(stream);
+ ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result \from (indirect: stream), (indirect: *stream);
+ */
+int __gen_e_acsl_fclose(FILE *stream);
+
+/*@ ensures result_ok_or_error: \result ≡ -1 ∨ \result ≥ 0;
+ ensures
+ initialization: stat_loc_init_on_success:
+ \result ≥ 0 ∧ \old(stat_loc) ≢ \null ⇒
+ \initialized(\old(stat_loc));
+ assigns \result, *stat_loc;
+ assigns \result \from (indirect: options);
+ assigns *stat_loc \from (indirect: options);
+
+ behavior stat_loc_null:
+ assumes stat_loc_null: stat_loc ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+
+ behavior stat_loc_non_null:
+ assumes stat_loc_non_null: stat_loc ≢ \null;
+ requires valid_stat_loc: \valid(stat_loc);
+ */
+pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options);
+
/*@ assigns \result;
assigns \result \from \nothing; */
extern int ( /* missing proto */ fork)(void);
+/*@ ensures result_ok_or_error: \result ≡ -1 ∨ \result ≥ 0;
+ ensures
+ initialization: stat_loc_init_on_success:
+ \result ≥ 0 ∧ \old(stat_loc) ≢ \null ⇒
+ \initialized(\old(stat_loc));
+ assigns \result, *stat_loc;
+ assigns \result \from (indirect: options);
+ assigns *stat_loc \from (indirect: options);
+
+ behavior stat_loc_null:
+ assumes stat_loc_null: stat_loc ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+
+ behavior stat_loc_non_null:
+ assumes stat_loc_non_null: stat_loc ≢ \null;
+ requires valid_stat_loc: \valid(stat_loc);
+ */
+pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
+{
+ int *__gen_e_acsl_at_2;
+ int *__gen_e_acsl_at;
+ pid_t __retres;
+ {
+ int __gen_e_acsl_implies;
+ __e_acsl_store_block((void *)(& stat_loc),(size_t)8);
+ if (! (stat_loc != (int *)0)) __gen_e_acsl_implies = 1;
+ else {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)stat_loc,sizeof(int),
+ (void *)stat_loc,
+ (void *)(& stat_loc));
+ __gen_e_acsl_implies = __gen_e_acsl_valid;
+ }
+ __e_acsl_assert(__gen_e_acsl_implies,"Precondition","waitpid",
+ "stat_loc != \\null ==> \\valid(stat_loc)",
+ "FRAMAC_SHARE/libc/sys/wait.h",92);
+ }
+ __gen_e_acsl_at_2 = stat_loc;
+ __gen_e_acsl_at = stat_loc;
+ __retres = waitpid(pid,stat_loc,options);
+ {
+ int __gen_e_acsl_or;
+ int __gen_e_acsl_and;
+ int __gen_e_acsl_implies_2;
+ if (__retres == -1) __gen_e_acsl_or = 1;
+ else __gen_e_acsl_or = __retres >= 0;
+ __e_acsl_assert(__gen_e_acsl_or,"Postcondition","waitpid",
+ "\\result == -1 || \\result >= 0",
+ "FRAMAC_SHARE/libc/sys/wait.h",84);
+ if (__retres >= 0) __gen_e_acsl_and = __gen_e_acsl_at != (int *)0;
+ else __gen_e_acsl_and = 0;
+ if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1;
+ else {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2,
+ sizeof(int));
+ __gen_e_acsl_implies_2 = __gen_e_acsl_initialized;
+ }
+ __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","waitpid",
+ "\\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))",
+ "FRAMAC_SHARE/libc/sys/wait.h",86);
+ __e_acsl_delete_block((void *)(& stat_loc));
+ return __retres;
+ }
+}
+
+/*@ requires valid_stream: \valid(stream);
+ ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1;
+ assigns \result;
+ assigns \result \from (indirect: stream), (indirect: *stream);
+ */
+int __gen_e_acsl_fclose(FILE *stream)
+{
+ int __retres;
+ {
+ int __gen_e_acsl_valid;
+ __e_acsl_store_block((void *)(& stream),(size_t)8);
+ __gen_e_acsl_valid = __e_acsl_valid((void *)stream,sizeof(FILE),
+ (void *)stream,(void *)(& stream));
+ __e_acsl_assert(__gen_e_acsl_valid,"Precondition","fclose",
+ "\\valid(stream)","FRAMAC_SHARE/libc/stdio.h",120);
+ }
+ __retres = fclose(stream);
+ {
+ int __gen_e_acsl_or;
+ if (__retres == 0) __gen_e_acsl_or = 1;
+ else __gen_e_acsl_or = __retres == -1;
+ __e_acsl_assert(__gen_e_acsl_or,"Postcondition","fclose",
+ "\\result == 0 || \\result == -1",
+ "FRAMAC_SHARE/libc/stdio.h",122);
+ __e_acsl_delete_block((void *)(& stream));
+ return __retres;
+ }
+}
+
+/*@ ensures
+ result_null_or_valid_fd:
+ \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]);
+ assigns \result;
+ assigns \result \from __fc_p_fopen;
+ */
+FILE *__gen_e_acsl_tmpfile(void)
+{
+ FILE *__retres;
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __retres = tmpfile();
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
+void __gen_e_acsl_exit(int status)
+{
+ exit(status);
+ __e_acsl_assert(0,"Postcondition","exit","\\false",
+ "FRAMAC_SHARE/libc/stdlib.h",473);
+ return;
+}
+
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
index 416aa6f3ed6c6327c6fb3f1e66770a7b0f9b2adc..52d996bb0201a28fd51cfb82afb06d4714107121 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
@@ -4,6 +4,23 @@
#include "stdlib.h"
extern int __e_acsl_sound_verdict;
+/*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1;
+ assigns \result;
+ assigns \result \from c;
+
+ behavior definitely_match:
+ assumes c_upper: 'A' ≤ c ≤ 'Z';
+ ensures nonzero_result: \result < 0 ∨ \result > 0;
+
+ behavior definitely_not_match:
+ assumes
+ c_non_upper: c ≡ -1 ∨ (0 ≤ c < 'A') ∨ ('Z' < c ≤ 127);
+ ensures zero_result: \result ≡ 0;
+
+ disjoint behaviors definitely_not_match, definitely_match;
+ */
+int __gen_e_acsl_isupper(int c);
+
int main(int argc, char const **argv)
{
int __retres;
@@ -39,4 +56,79 @@ int main(int argc, char const **argv)
return __retres;
}
+/*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1;
+ assigns \result;
+ assigns \result \from c;
+
+ behavior definitely_match:
+ assumes c_upper: 'A' ≤ c ≤ 'Z';
+ ensures nonzero_result: \result < 0 ∨ \result > 0;
+
+ behavior definitely_not_match:
+ assumes
+ c_non_upper: c ≡ -1 ∨ (0 ≤ c < 'A') ∨ ('Z' < c ≤ 127);
+ ensures zero_result: \result ≡ 0;
+
+ disjoint behaviors definitely_not_match, definitely_match;
+ */
+int __gen_e_acsl_isupper(int c)
+{
+ int __gen_e_acsl_at_2;
+ int __gen_e_acsl_at;
+ int __retres;
+ {
+ int __gen_e_acsl_and;
+ int __gen_e_acsl_or;
+ if (0 <= c) __gen_e_acsl_and = c <= 255; else __gen_e_acsl_and = 0;
+ if (__gen_e_acsl_and) __gen_e_acsl_or = 1;
+ else __gen_e_acsl_or = c == -1;
+ __e_acsl_assert(__gen_e_acsl_or,"Precondition","isupper",
+ "(0 <= c <= 255) || c == -1","FRAMAC_SHARE/libc/ctype.h",
+ 174);
+ }
+ {
+ int __gen_e_acsl_or_3;
+ int __gen_e_acsl_or_4;
+ if (c == -1) __gen_e_acsl_or_3 = 1;
+ else {
+ int __gen_e_acsl_and_3;
+ if (0 <= c) __gen_e_acsl_and_3 = c < 65; else __gen_e_acsl_and_3 = 0;
+ __gen_e_acsl_or_3 = __gen_e_acsl_and_3;
+ }
+ if (__gen_e_acsl_or_3) __gen_e_acsl_or_4 = 1;
+ else {
+ int __gen_e_acsl_and_4;
+ if (90 < c) __gen_e_acsl_and_4 = c <= 127; else __gen_e_acsl_and_4 = 0;
+ __gen_e_acsl_or_4 = __gen_e_acsl_and_4;
+ }
+ __gen_e_acsl_at_2 = __gen_e_acsl_or_4;
+ }
+ {
+ int __gen_e_acsl_and_2;
+ if (65 <= c) __gen_e_acsl_and_2 = c <= 90; else __gen_e_acsl_and_2 = 0;
+ __gen_e_acsl_at = __gen_e_acsl_and_2;
+ }
+ __retres = isupper(c);
+ {
+ int __gen_e_acsl_implies;
+ int __gen_e_acsl_implies_2;
+ if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1;
+ else {
+ int __gen_e_acsl_or_2;
+ if (__retres < 0) __gen_e_acsl_or_2 = 1;
+ else __gen_e_acsl_or_2 = __retres > 0;
+ __gen_e_acsl_implies = __gen_e_acsl_or_2;
+ }
+ __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","isupper",
+ "\\old(\'A\' <= c <= \'Z\') ==> \\result < 0 || \\result > 0",
+ "FRAMAC_SHARE/libc/ctype.h",178);
+ if (! __gen_e_acsl_at_2) __gen_e_acsl_implies_2 = 1;
+ else __gen_e_acsl_implies_2 = __retres == 0;
+ __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","isupper",
+ "\\old(c == -1 || (0 <= c < \'A\') || (\'Z\' < c <= 127)) ==> \\result == 0",
+ "FRAMAC_SHARE/libc/ctype.h",181);
+ return __retres;
+ }
+}
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
index 8ec1fd43938696c97a69a574ac0324914fbac459..cd9cd223bf692bfcd3df82812937c41f4ebd306e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
@@ -4,6 +4,13 @@
#include "string.h"
extern int __e_acsl_sound_verdict;
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures acsl_c_equiv: \result ≡ strlen(\old(s));
+ assigns \result;
+ assigns \result \from (indirect: *(s + (0 ..)));
+ */
+size_t __gen_e_acsl_strlen(char const *s);
+
/*@ requires \valid(&argc);
requires \valid(&argv); */
int main(int argc, char **argv);
@@ -197,4 +204,18 @@ int main(int argc, char **argv)
return __retres;
}
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures acsl_c_equiv: \result ≡ strlen(\old(s));
+ assigns \result;
+ assigns \result \from (indirect: *(s + (0 ..)));
+ */
+size_t __gen_e_acsl_strlen(char const *s)
+{
+ size_t __retres;
+ __e_acsl_store_block((void *)(& s),(size_t)8);
+ __retres = strlen(s);
+ __e_acsl_delete_block((void *)(& s));
+ return __retres;
+}
+
diff --git a/src/plugins/e-acsl/tests/print.ml b/src/plugins/e-acsl/tests/print.ml
index da98696a1043b123459d356400232c803b028687..bcf83012c2cd7d578e01eaccc139afb346941c4c 100644
--- a/src/plugins/e-acsl/tests/print.ml
+++ b/src/plugins/e-acsl/tests/print.ml
@@ -20,6 +20,20 @@
(* *)
(**************************************************************************)
+(* return true if the global g has been generated by E-ACSL *)
+let is_generated (g: Cil_datatype.Global.t) =
+ let name =
+ match g with
+ | GType (ti, _) -> ti.tname
+ | GCompTagDecl (ci, _) | GCompTag(ci, _) -> ci.cname
+ | GEnumTagDecl (ei, _) | GEnumTag (ei, _) -> ei.ename
+ | GVarDecl (vi, _) | GVar(vi, _, _) -> vi.vname
+ | GFun (fundec, _) -> fundec.svar.vname
+ | GFunDecl (_, vi, _) -> vi.vname
+ | _ -> ""
+ in
+ E_ACSL.Functions.RTL.is_generated_name name
+
module Printer_extension(X: Printer.PrinterClass) = struct
class printer = object
@@ -29,7 +43,8 @@ module Printer_extension(X: Printer.PrinterClass) = struct
let loc, _ = Cil_datatype.Global.loc g in
let file = loc.Filepath.pos_path in
if file = Datatype.Filepath.dummy ||
- List.exists (fun s -> s = file) (Kernel.Files.get ())
+ List.exists (fun s -> s = file) (Kernel.Files.get ()) ||
+ is_generated g
then super#global fmt g
end
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
index 67f60841795ebbe9553887f4d8fb2afeb2445231..9c4df1533bf7feccab969de992f3c7692d8a77a2 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
@@ -5,6 +5,48 @@ char *__gen_e_acsl_literal_string_2;
char *__gen_e_acsl_literal_string;
extern int __e_acsl_sound_verdict;
+/*@ requires valid_name: valid_read_string(name);
+ ensures null_or_valid_result: \result ≡ \null ∨ \valid(\result);
+ assigns \result;
+ assigns \result \from __fc_env[0 ..], (indirect: name), *(name + (0 ..));
+ */
+char *__gen_e_acsl_getenv(char const *name);
+
+/*@ requires valid_name: valid_read_string(name);
+ ensures null_or_valid_result: \result ≡ \null ∨ \valid(\result);
+ assigns \result;
+ assigns \result \from __fc_env[0 ..], (indirect: name), *(name + (0 ..));
+ */
+char *__gen_e_acsl_getenv(char const *name)
+{
+ char *__retres;
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __e_acsl_temporal_reset_parameters();
+ __e_acsl_temporal_reset_return();
+ __retres = getenv(name);
+ __e_acsl_temporal_store_nblock((void *)(& __retres),(void *)*(& __retres));
+ {
+ int __gen_e_acsl_or;
+ __e_acsl_temporal_save_return((void *)(& __retres));
+ /*@ assert
+ Eva: ptr_comparison: \pointer_comparable((void *)__retres, (void *)0);
+ */
+ if (__retres == (char *)0) __gen_e_acsl_or = 1;
+ else {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)__retres,sizeof(char),
+ (void *)__retres,
+ (void *)(& __retres));
+ __gen_e_acsl_or = __gen_e_acsl_valid;
+ }
+ __e_acsl_assert(__gen_e_acsl_or,"Postcondition","getenv",
+ "\\result == \\null || \\valid(\\result)",
+ "FRAMAC_SHARE/libc/stdlib.h",488);
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
+ }
+}
+
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
index a6f4773e2ce84e8ac4a443f011c240549d1f0086..0f86c7371d4c879dc64808a673a75ca10dbe1a7a 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
@@ -4,6 +4,34 @@
#include "string.h"
extern int __e_acsl_sound_verdict;
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ requires
+ separation:
+ \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest;
+ */
+void *__gen_e_acsl_memcpy(void * __restrict dest,
+ void const * __restrict src, size_t n);
+
+/*@ requires valid_s: valid_or_empty(s, n);
+ ensures
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
+ ensures result_ptr: \result ≡ \old(s);
+ assigns *((char *)s + (0 .. n - 1)), \result;
+ assigns *((char *)s + (0 .. n - 1)) \from c;
+ assigns \result \from s;
+ */
+void *__gen_e_acsl_memset(void *s, int c, size_t n);
+
int main(void)
{
int __retres;
@@ -357,4 +385,64 @@ int main(void)
return __retres;
}
+/*@ requires valid_s: valid_or_empty(s, n);
+ ensures
+ acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true;
+ ensures result_ptr: \result ≡ \old(s);
+ assigns *((char *)s + (0 .. n - 1)), \result;
+ assigns *((char *)s + (0 .. n - 1)) \from c;
+ assigns \result \from s;
+ */
+void *__gen_e_acsl_memset(void *s, int c, size_t n)
+{
+ void *__gen_e_acsl_at;
+ void *__retres;
+ __e_acsl_store_block((void *)(& s),(size_t)8);
+ __e_acsl_temporal_pull_parameter((void *)(& s),0U,8UL);
+ __e_acsl_temporal_reset_parameters();
+ __e_acsl_temporal_reset_return();
+ __e_acsl_temporal_save_nreferent_parameter((void *)(& s),0U);
+ __e_acsl_temporal_memset(s,c,n);
+ __gen_e_acsl_at = s;
+ __retres = memset(s,c,n);
+ __e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","memset",
+ "\\result == \\old(s)","FRAMAC_SHARE/libc/string.h",119);
+ __e_acsl_delete_block((void *)(& s));
+ return __retres;
+}
+
+/*@ requires valid_dest: valid_or_empty(dest, n);
+ requires valid_src: valid_read_or_empty(src, n);
+ requires
+ separation:
+ \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1));
+ ensures
+ copied_contents:
+ memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡
+ 0;
+ ensures result_ptr: \result ≡ \old(dest);
+ assigns *((char *)dest + (0 .. n - 1)), \result;
+ assigns *((char *)dest + (0 .. n - 1))
+ \from *((char *)src + (0 .. n - 1));
+ assigns \result \from dest;
+ */
+void *__gen_e_acsl_memcpy(void * __restrict dest,
+ void const * __restrict src, size_t n)
+{
+ void *__gen_e_acsl_at;
+ void *__retres;
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
+ __e_acsl_temporal_pull_parameter((void *)(& dest),0U,8UL);
+ __e_acsl_temporal_reset_parameters();
+ __e_acsl_temporal_reset_return();
+ __e_acsl_temporal_save_nreferent_parameter((void *)(& dest),0U);
+ __e_acsl_temporal_memcpy(dest,(void *)src,n);
+ __gen_e_acsl_at = dest;
+ __retres = memcpy(dest,src,n);
+ __e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","memcpy",
+ "\\result == \\old(dest)","FRAMAC_SHARE/libc/string.h",99);
+ __e_acsl_delete_block((void *)(& dest));
+ return __retres;
+}
+