From 3bc567495c7cc143bb1dd28719a14af91945dddd Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 27 Nov 2017 14:27:28 +0100
Subject: [PATCH] fix 'segfault' in the generated code when the main has a
precondition depending on the memory model
---
src/plugins/e-acsl/doc/Changelog | 3 +
src/plugins/e-acsl/tests/runtime/mainargs.c | 4 +-
.../tests/runtime/oracle/gen_labeled_stmt.c | 2 +-
.../tests/runtime/oracle/gen_mainargs.c | 76 +++++++++++--------
src/plugins/e-acsl/visit.ml | 5 +-
5 files changed, 52 insertions(+), 38 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 1fe23700390..8ae905a0832 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -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
diff --git a/src/plugins/e-acsl/tests/runtime/mainargs.c b/src/plugins/e-acsl/tests/runtime/mainargs.c
index df475a66627..19bfe02f552 100644
--- a/src/plugins/e-acsl/tests/runtime/mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/mainargs.c
@@ -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*) ; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
index 5a9054e4599..67b4fb27b2c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
@@ -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);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index d4427946aca..d86edf694ff 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -1,41 +1,29 @@
/* 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;
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index c475f5398ba..6e8131899b5 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -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,
--
GitLab