Skip to content
Snippets Groups Projects
Commit 3bc56749 authored by Julien Signoles's avatar Julien Signoles
Browse files

fix 'segfault' in the generated code when the main has a precondition depending on the memory model

parent d4c72e04
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/doc/Changelog
+ 3
− 0
View file @ 3bc56749
......@@ -15,6 +15,9 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
-* E-ACSL [2017/11/27] Fix 'segmentation fault' of the generated monitor
whenever the main as a precondition depending on the memory
model.
-* E-ACSL [2017/11/27] Restore behavior of option -e-acsl-valid broken
since Phosphorus (included).
-* E-ACSL [2017/10/25] Fix bug #2303 about unnamed formals in
......
src/plugins/e-acsl/tests/runtime/mainargs.c
+ 2
− 2
View file @ 3bc56749
......@@ -4,11 +4,11 @@
#include <string.h>
/*@ requires \valid(&argc);
@ requires \valid(&argv); */
int main(int argc, char **argv) {
int i;
/*@ assert \valid(&argc) ; */
/*@ assert \valid(&argv) ; */
/*@ assert \forall int k; 0 <= k && k < argc ==> \valid(argv + k) ; */
/*@ assert \block_length(argv) == (argc+1)*sizeof(char*) ; */
......
src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
+ 1
− 1
View file @ 3bc56749
......@@ -7,7 +7,6 @@ int main(void);
int __gen_e_acsl_main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
goto L1;
L1:
/*@ assert X ≡ 0; */
......@@ -38,6 +37,7 @@ int __gen_e_acsl_main(void)
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__retres = __gen_e_acsl_main();
__e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"main",
(char *)"X == 3",7);
......
src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+ 43
− 33
View file @ 3bc56749
/* Generated by Frama-C */
#include "stdlib.h"
#include "string.h"
int main(int argc, char **argv)
/*@ requires \valid(&argc);
requires \valid(&argv); */
int main(int argc, char **argv);
int __gen_e_acsl_main(int argc, char **argv)
{
int __retres;
int i;
__e_acsl_memory_init(& argc,& argv,(size_t)8);
/*@ assert \valid(&argc); */
{
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int),
(void *)(& argc),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&argc)",10);
}
/*@ assert \valid(&argv); */
{
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& argv),sizeof(char **),
(void *)(& argv),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&argv)",11);
}
/*@ assert ∀ int k; 0 ≤ k < argc ⇒ \valid(argv + k); */
{
int __gen_e_acsl_forall;
int __gen_e_acsl_k;
__e_acsl_store_block((void *)(& argv),(size_t)8);
__gen_e_acsl_forall = 1;
__gen_e_acsl_k = 0;
while (1) {
if (__gen_e_acsl_k < argc) ; else break;
{
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
sizeof(char *),(void *)argv,
(void *)(& argv));
if (__gen_e_acsl_valid_3) ;
int __gen_e_acsl_valid;
__gen_e_acsl_valid = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
sizeof(char *),(void *)argv,
(void *)(& argv));
if (__gen_e_acsl_valid) ;
else {
__gen_e_acsl_forall = 0;
goto e_acsl_end_loop1;
......@@ -86,7 +74,7 @@ int main(int argc, char **argv)
sizeof(char *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_valid_4;
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(argv + argc),
sizeof(char *),
(void *)argv,
......@@ -94,11 +82,11 @@ int main(int argc, char **argv)
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",16);
/*@ assert Value: mem_access: \valid_read(argv + argc); */
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)*(argv + argc),
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)*(argv + argc),
sizeof(char),
(void *)*(argv + argc),
(void *)(argv + argc));
__gen_e_acsl_and = __gen_e_acsl_valid_4;
__gen_e_acsl_and = __gen_e_acsl_valid_2;
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(! __gen_e_acsl_and,(char *)"Assertion",(char *)"main",
......@@ -118,7 +106,7 @@ int main(int argc, char **argv)
sizeof(char *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_valid_5;
int __gen_e_acsl_valid_3;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(argv + i),
sizeof(char *),
(void *)argv,
......@@ -126,11 +114,11 @@ int main(int argc, char **argv)
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv + i)",19);
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)*(argv + i),
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)*(argv + i),
sizeof(char),
(void *)*(argv + i),
(void *)(argv + i));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_5;
__gen_e_acsl_and_2 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_2 = 0;
__e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",
......@@ -146,7 +134,7 @@ int main(int argc, char **argv)
if (__gen_e_acsl_k_2 <= len) ; else break;
{
int __gen_e_acsl_valid_read_4;
int __gen_e_acsl_valid_6;
int __gen_e_acsl_valid_4;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(
argv + i),
sizeof(char *),
......@@ -155,11 +143,11 @@ int main(int argc, char **argv)
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(argv + i)",20);
__gen_e_acsl_valid_6 = __e_acsl_valid((void *)(*(argv + i) + __gen_e_acsl_k_2),
__gen_e_acsl_valid_4 = __e_acsl_valid((void *)(*(argv + i) + __gen_e_acsl_k_2),
sizeof(char),
(void *)*(argv + i),
(void *)(argv + i));
if (__gen_e_acsl_valid_6) ;
if (__gen_e_acsl_valid_4) ;
else {
__gen_e_acsl_forall_2 = 0;
goto e_acsl_end_loop2;
......@@ -178,7 +166,29 @@ int main(int argc, char **argv)
}
__retres = 0;
__e_acsl_delete_block((void *)(& argv));
__e_acsl_delete_block((void *)(& argc));
return __retres;
}
/*@ requires \valid(&argc);
requires \valid(&argv); */
int main(int argc, char **argv)
{
int __retres;
__e_acsl_memory_init(& argc,& argv,(size_t)8);
{
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
__gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int),
(void *)(& argc),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"main",
(char *)"\\valid(&argc)",7);
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& argv),sizeof(char **),
(void *)(& argv),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
(char *)"main",(char *)"\\valid(&argv)",8);
}
__retres = __gen_e_acsl_main(argc,argv);
__e_acsl_delete_block((void *)(& argv));
__e_acsl_memory_clean();
return __retres;
}
......
src/plugins/e-acsl/visit.ml
+ 3
− 2
View file @ 3bc56749
......@@ -370,8 +370,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
vi.vghost <- false;
Builtins.update vi.vname vi;
(* remember that we have to remove the main later (see method
[vfile]) *)
if vi.vorig_name = Kernel.MainFunction.get () then
[vfile]); do not use the [vorig_name] since both [main] and
[__e_acsl_main] have the same [vorig_name]. *)
if vi.vname = Kernel.MainFunction.get () then
main_fct <- Some fundec
| GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
(* do not convert extern ghost variables, because they can't be linked,
......
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