Commit b0d6eaac authored by Julien Signoles's avatar Julien Signoles Committed by Zaynah Dargaye
Browse files

fix bug #1717 about instrumentation of labeled stmt

parent 8f8c433c
......@@ -20,6 +20,8 @@
some messages.
- E-ACSL [2014/03/26] Remove a spurious warning when an annotated
function is first declared, then defined.
-* E-ACSL [2014/03/26] Fix bug #1717 about instrumentation of
labeled statements.
-* E-ACSL [2014/03/25] Fix bug #1716 with annotations in while(1).
-* E-ACSL [2014/03/25] Fix bug #1715 about -e-acsl-full-mmodel which
generates incorrect code.
......
......@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
module E_acsl_label = Label
open Cil_types
open Cil_datatype
......@@ -305,12 +306,13 @@ let add_assert env stmt annot = match current_kf env with
(fun () -> Annotations.add_assert emitter ~kf stmt annot)
env.visitor#get_filling_actions
let add_stmt ?(init=false) env stmt =
let add_stmt ?(init=false) ?before env stmt =
Extlib.may (fun old -> E_acsl_label.move env.visitor ~old stmt) before;
let local_env, tl = top init env in
let block = local_env.block_info in
let block = { block with new_stmts = stmt :: block.new_stmts } in
let local_env = { local_env with block_info = block } in
{ env with
{ env with
init_env = if init then local_env else env.init_env;
env_stack = if init then env.env_stack else local_env :: tl }
......
......@@ -62,8 +62,9 @@ val add_assert: t -> stmt -> predicate named -> unit
(** [add_assert env s p] associates the assertion [p] to the statement [s] in
the environment [env]. *)
val add_stmt: ?init:bool -> t -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s] *)
val add_stmt: ?init:bool -> ?before:stmt -> t -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s].
[before] may define which stmt the new is included before. *)
val extend_stmt_in_place: t -> stmt -> pre:bool -> block -> t
(** [extend_stmt_in_place env stmt ~pre b] modifies [stmt] in place in order to
......
......@@ -22,6 +22,21 @@
open Cil_types
(* The keys are the stmts which were previously labeled, whereas the associated
values are the new stmts containing the same labels. *)
module Labeled_stmts =
Cil_state_builder.Stmt_hashtbl
(Cil_datatype.Stmt)
(struct
let size = 7
let dependencies = [] (* delayed *)
let name = "E-ACSL.Labels"
end)
let self = Labeled_stmts.self
let new_labeled_stmt stmt = try Labeled_stmts.find stmt with Not_found -> stmt
let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
let labels = old.labels in
match labels with
......@@ -29,6 +44,7 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
| _ :: _ ->
old.labels <- [];
new_stmt.labels <- labels @ new_stmt.labels;
Labeled_stmts.add old new_stmt;
(* update the gotos of the function jumping to one of the labels *)
let o = object
inherit Visitor.frama_c_inplace
......
......@@ -29,6 +29,13 @@ val move: Visitor.generic_frama_c_visitor -> old:stmt -> stmt -> unit
val get_stmt: Visitor.generic_frama_c_visitor -> logic_label -> stmt
(** @return the statement where the logic label points to. *)
val new_labeled_stmt: stmt -> stmt
(** @return the labeled stmt to use instead of the given one (which
previously contained a label *)
val self: State.t
(** Internal state *)
(*
Local Variables:
compile-command: "make"
......
......@@ -133,6 +133,11 @@ module Resulting_projects =
let dependencies = [ Ast.self ]
end)
let () =
State_dependency_graph.add_dependencies
~from:Resulting_projects.self
[ Label.self ]
let generate_code =
Resulting_projects.memo
(fun name ->
......
/* run.config
COMMENT: bts #1717, issue with labels on memory-related statements
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1717.c > /dev/null && ./gcc_test.sh bts1717
EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts17172.c > /dev/null && ./gcc_test.sh bts17172
*/
int main(void) {
int a = 10, *p;
goto lbl_1;
lbl_2:
/*@ assert \valid(p); */
return 0;
lbl_1:
p = &a;
goto lbl_2;
}
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
tests/e-acsl-runtime/bts1717.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
tests/e-acsl-runtime/bts1717.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
......@@ -123,7 +123,6 @@ void g(int *p, int *q)
*(p + 1) = 1;
__initialize((void *)q,sizeof(int));
*q = 0;
__initialize((void *)p,sizeof(int));
L1:
{
int __e_acsl_valid_read_3;
......@@ -141,7 +140,8 @@ void g(int *p, int *q)
__store_block((void *)(& __e_acsl_at),4U);
__e_acsl_at = *q;
}
*p = 2;
__initialize((void *)p,sizeof(int));
*p = 2;
__initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
__initialize((void *)q,sizeof(int));
......
......@@ -229,7 +229,6 @@ void g(int *p, int *q)
*(p + 1) = 1;
__initialize((void *)q,sizeof(int));
*q = 0;
__initialize((void *)p,sizeof(int));
L1:
{
int __e_acsl_valid_read_3;
......@@ -247,7 +246,8 @@ void g(int *p, int *q)
__store_block((void *)(& __e_acsl_at),4U);
__e_acsl_at = *q;
}
*p = 2;
__initialize((void *)p,sizeof(int));
*p = 2;
__initialize((void *)(p + 1),sizeof(int));
*(p + 1) = 3;
__initialize((void *)q,sizeof(int));
......
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
int _mp_alloc ;
int _mp_size ;
unsigned long *_mp_d ;
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *kind,
char *fct,
char *pred_txt,
int line);
/*@
model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
}
*/
/*@ ghost extern int __e_acsl_init; */
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1));
*/
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1));
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
/*@ ghost extern int __e_acsl_internal_heap; */
/*@ assigns __e_acsl_internal_heap;
assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
/*@ ghost extern size_t __memory_size; */
/*@
predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
int main(void)
{
int __retres;
int a;
int *p;
__store_block((void *)(& p),4U);
__store_block((void *)(& a),4U);
__full_init((void *)(& a));
a = 10;
goto lbl_1;
lbl_2:
/*@ assert \valid(p); */
{
int __e_acsl_initialized;
int __e_acsl_and;
__e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
__e_acsl_valid = __valid((void *)p,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
(char *)"\\valid(p)",13);
}
__retres = 0;
goto return_label;
lbl_1: __full_init((void *)(& p));
p = & a;
goto lbl_2;
return_label:
__delete_block((void *)(& p));
__delete_block((void *)(& a));
__e_acsl_memory_clean();
return __retres;
}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
int _mp_alloc ;
int _mp_size ;
unsigned long *_mp_d ;
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
/*@ requires predicate ≢ 0;
assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
char *kind,
char *fct,
char *pred_txt,
int line);
/*@
model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
axiomatic
dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
}
*/
/*@ ghost extern int __e_acsl_init; */
/*@ assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1)); */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1));
*/
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
ensures
\result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
assigns \result;
assigns \result \from *((char *)ptr+(0 .. size-1));
*/
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
/*@ ghost extern int __e_acsl_internal_heap; */
/*@ assigns __e_acsl_internal_heap;
assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
*/
extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
/*@ ghost extern size_t __memory_size; */
/*@
predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
int main(void)
{
int __retres;
int a;
int *p;
__store_block((void *)(& p),4U);
__store_block((void *)(& a),4U);
__full_init((void *)(& a));
a = 10;
goto lbl_1;
lbl_2:
/*@ assert \valid(p); */
{
int __e_acsl_initialized;
int __e_acsl_and;
__e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
if (__e_acsl_initialized) {
int __e_acsl_valid;
__e_acsl_valid = __valid((void *)p,sizeof(int));
__e_acsl_and = __e_acsl_valid;
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
(char *)"\\valid(p)",13);
}
__retres = 0;
goto return_label;
lbl_1: __full_init((void *)(& p));
p = & a;
goto lbl_2;
return_label:
__delete_block((void *)(& p));
__delete_block((void *)(& a));
__e_acsl_memory_clean();
return __retres;
}
......@@ -535,12 +535,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(Pre_analysis.must_model_lval ~kf ~stmt checked_lv);*)
if not (may_safely_ignore assigned_lv) &&
Pre_analysis.must_model_lval ~kf ~stmt checked_lv
then begin
let stmt =
then
let new_stmt =
Misc.mk_debug_mmodel_stmt (Misc.mk_initialize loc assigned_lv)
in
function_env := Env.add_stmt !function_env stmt
end
let before = Cil.memo_stmt self#behavior stmt in
function_env := Env.add_stmt ~before !function_env new_stmt
method !vinst = function
| Set(old_lv, _, _) ->
......@@ -631,7 +631,16 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
else
Cil.SkipChildren
initializer
method !vterm _ =
Cil.DoChildrenPost
(fun t ->
(match t.term_node with
| Tat(_, StmtLabel s_ref) ->
s_ref := E_acsl_label.new_labeled_stmt !s_ref
| _ -> ());
t)
initializer
Misc.reset ();
self#reset_env ();
Translate.set_original_project (Project.current ())
......
Markdown is supported
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