Commit 4e1f7dd3 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/andre/libc-rand48' into 'master'

sync with frama-c/frama-c!2148

See merge request frama-c/e-acsl!281
parents 5e135627 4ef4d409
......@@ -219,6 +219,12 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_fopen));
__e_acsl_store_block((void *)(& stderr),(size_t)8);
__e_acsl_full_init((void *)(& stderr));
__e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
__e_acsl_full_init((void *)(& __fc_p_random48_counter));
__e_acsl_store_block((void *)(random48_counter),(size_t)6);
__e_acsl_full_init((void *)(& random48_counter));
__e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
__e_acsl_full_init((void *)(& __fc_random48_init));
__e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
__e_acsl_full_init((void *)(& __fc_rand_max));
}
......@@ -1383,6 +1389,9 @@ int main(int argc, char const **argv)
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
__e_acsl_delete_block((void *)(& stderr));
__e_acsl_delete_block((void *)(& __fc_p_random48_counter));
__e_acsl_delete_block((void *)(random48_counter));
__e_acsl_delete_block((void *)(& __fc_random48_init));
__e_acsl_delete_block((void *)(& __fc_rand_max));
__e_acsl_delete_block((void *)(nar));
__e_acsl_delete_block((void *)(nal));
......
......@@ -17,10 +17,6 @@ char *__gen_e_acsl_literal_string_5;
char *__gen_e_acsl_literal_string;
extern int __e_acsl_sound_verdict;
/*@ assigns \result;
assigns \result \from \nothing; */
extern int ( /* missing proto */ fork)(void);
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
......@@ -98,6 +94,12 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_p_fopen));
__e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
__e_acsl_full_init((void *)(& __fc_fopen));
__e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
__e_acsl_full_init((void *)(& __fc_p_random48_counter));
__e_acsl_store_block((void *)(random48_counter),(size_t)6);
__e_acsl_full_init((void *)(& random48_counter));
__e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
__e_acsl_full_init((void *)(& __fc_random48_init));
__e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
__e_acsl_full_init((void *)(& __fc_rand_max));
}
......@@ -434,6 +436,9 @@ int main(int argc, char const **argv)
__e_acsl_delete_block((void *)(& __fc_strtok_ptr));
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
__e_acsl_delete_block((void *)(& __fc_p_random48_counter));
__e_acsl_delete_block((void *)(random48_counter));
__e_acsl_delete_block((void *)(& __fc_random48_init));
__e_acsl_delete_block((void *)(& __fc_rand_max));
__e_acsl_delete_block((void *)(& const_str));
__e_acsl_delete_block((void *)(stack_str));
......
......@@ -28,7 +28,7 @@
Neither code nor specification for function set_handler, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/builtin/signalled.h:22: Warning:
Neither code nor specification for function test_successful, generating default assigns from the prototype
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:394: Warning:
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:457: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:469: Warning:
......@@ -67,7 +67,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:140: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:406: Warning:
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:469: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
......@@ -80,13 +80,7 @@
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
<<<<<<< HEAD
||||||| merged common ancestors
testno ∈ {0}
=======
testno ∈ {0}
__e_acsl_sound_verdict ∈ [--..--]
>>>>>>> new option -e-acsl-instrument
__gen_e_acsl_literal_string ∈ {0}
__gen_e_acsl_literal_string_2 ∈ {0}
__gen_e_acsl_literal_string_3 ∈ {0}
......
......@@ -23,7 +23,7 @@
Neither code nor specification for function set_handler, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/builtin/signalled.h:22: Warning:
Neither code nor specification for function test_successful, generating default assigns from the prototype
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:394: Warning:
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:457: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:469: Warning:
......@@ -47,7 +47,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:406: Warning:
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:469: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
......@@ -60,7 +60,6 @@
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
testno ∈ {0}
__e_acsl_sound_verdict ∈ [--..--]
__gen_e_acsl_literal_string ∈ {0}
__gen_e_acsl_literal_string_2 ∈ {0}
......
......@@ -218,6 +218,12 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_fopen));
__e_acsl_store_block((void *)(& stdout),(size_t)8);
__e_acsl_full_init((void *)(& stdout));
__e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
__e_acsl_full_init((void *)(& __fc_p_random48_counter));
__e_acsl_store_block((void *)(random48_counter),(size_t)6);
__e_acsl_full_init((void *)(& random48_counter));
__e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
__e_acsl_full_init((void *)(& __fc_random48_init));
__e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
__e_acsl_full_init((void *)(& __fc_rand_max));
}
......@@ -598,6 +604,9 @@ int main(int argc, char const **argv)
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
__e_acsl_delete_block((void *)(& stdout));
__e_acsl_delete_block((void *)(& __fc_p_random48_counter));
__e_acsl_delete_block((void *)(random48_counter));
__e_acsl_delete_block((void *)(& __fc_random48_init));
__e_acsl_delete_block((void *)(& __fc_rand_max));
__e_acsl_delete_block((void *)(buf));
__e_acsl_delete_block((void *)(& fh));
......
......@@ -39,6 +39,12 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& __fc_p_fopen));
__e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
__e_acsl_full_init((void *)(& __fc_fopen));
__e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
__e_acsl_full_init((void *)(& __fc_p_random48_counter));
__e_acsl_store_block((void *)(random48_counter),(size_t)6);
__e_acsl_full_init((void *)(& random48_counter));
__e_acsl_store_block((void *)(& __fc_random48_init),(size_t)4);
__e_acsl_full_init((void *)(& __fc_random48_init));
__e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
__e_acsl_full_init((void *)(& __fc_rand_max));
}
......@@ -63,6 +69,9 @@ int main(void)
__e_acsl_delete_block((void *)(& f));
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
__e_acsl_delete_block((void *)(& __fc_p_random48_counter));
__e_acsl_delete_block((void *)(random48_counter));
__e_acsl_delete_block((void *)(& __fc_random48_init));
__e_acsl_delete_block((void *)(& __fc_rand_max));
__e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& __retres));
......
......@@ -2,10 +2,10 @@
[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:419: Warning:
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:482: Warning:
E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:419: Warning:
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:482: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment