diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 39705d1f9b036d0422c3ab534db5943fdb4ce6d3..515f1b1b5b7f708f1ddb61cbab1f032e33e36700 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -1,7 +1,6 @@
-- regarder la remarque sur le cas CInt64: distinction signed and unsigned type?
+- utiliser Options.use_asserts
-- access pointeurs: ajouter des warnings indiquant que les gardes sont
- manquantes
+- regarder la remarque sur le cas CInt64: distinction signed and unsigned type?
- gestion des initialiseurs des globals: requiert un main
@@ -16,9 +15,10 @@ the plug-in would generate something like
- mkcall ne devrait pas générer de nouvelles variables pour une même fonction
-- mettre des locations intelligentes
+[TODO?] mettre des locations intelligentes
-- guarde pour les divisions/modulos
+- garde pour les casts quand overflows potentiels
+ (même pas de warnings aujourd'hui)
- tester les opérations binaires sur les pointeurs (requiert complex left value)
@@ -32,3 +32,5 @@ en lien avec bts #743:
- headers (copyright 2011)
- license
- install répertoire share
+
+VOIR CPAN
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid.res.oracle
index 133a9cdcd2e51c24d9d54a72f95e85e042fd626a..b391ab242f1f27633303f0bd55d27dd11a50bb43 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid.res.oracle
@@ -1,3 +1,3 @@
[kernel] Plug-in e-acsl aborted because of unimplemented feature.
Please send a feature request at http://bts.frama-c.com with:
- '[Plug-in e-acsl] construct `\valid' is not yet supported'.
+ '[Plug-in e-acsl] construct `\valid' is not yet supported.'.
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
index 52ac08f2e0c102081525a6f6bbcd6ba8f66d473f..c2f59365f05615243478feb2fdbd9eecd5d3eab1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_index.res.oracle
@@ -1,3 +1,3 @@
[kernel] Plug-in e-acsl aborted because of unimplemented feature.
Please send a feature request at http://bts.frama-c.com with:
- '[Plug-in e-acsl] construct `\valid_index' is not yet supported'.
+ '[Plug-in e-acsl] construct `\valid_index' is not yet supported.'.
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
index 84ba89e4ef8e857c6a28e175aa8008f12524d52e..211e09903d7e206d86833b532ea9cf61d37cbdba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/valid_range.res.oracle
@@ -1,3 +1,3 @@
[kernel] Plug-in e-acsl aborted because of unimplemented feature.
Please send a feature request at http://bts.frama-c.com with:
- '[Plug-in e-acsl] construct `\valid_range' is not yet supported'.
+ '[Plug-in e-acsl] construct `\valid_range' is not yet supported.'.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index a85244fafff3d92ac50f173e0341c911483a9bf9..6305141757c1b4d7ee3e66853625d6bf49808b55 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -9,7 +9,7 @@ PROJECT_FILE.i:121:[value] Assertion got status valid.
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
- x ∈ {0; }
+ x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
ensures \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 037892419400db7546258b66a7e80bfc663aba73..4caed2143472a05b866269156a530966ba2aba6d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -1,3 +1,5 @@
+tests/e-acsl-runtime/arith.i:18:[e-acsl] warning: missing guard for ensuring that 3 is different of 0
+tests/e-acsl-runtime/arith.i:19:[e-acsl] warning: missing guard for ensuring that 2 is different of 0
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
@@ -726,8 +728,8 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies)
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
[value] Values for function main:
- x ∈ {-3; }
- y ∈ {2; }
+ x ∈ {-3}
+ y ∈ {2}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
int _mp_alloc ;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 93f7787744218301c4ebb7cf4542ed2f4c78f237..f9748ebda52be73f19ea6f8243c851b1f1b9ab2e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -10,8 +10,8 @@ PROJECT_FILE.i:126:[value] Assertion got status valid.
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
- x ∈ {0; }
- y ∈ {0; }
+ x ∈ {0}
+ y ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
ensures \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index c680c528f34a2352eb89d3bd7f9fec2a0662aa9d..96290ed950f45f4d068de0972b9a997a7cbb4860 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -241,8 +241,8 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies)
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
[value] Values for function main:
- x ∈ {0; }
- y ∈ {1; }
+ x ∈ {0}
+ y ∈ {1}
s ∈ {{ &"toto" ;}}
/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index 17e581bbedfe26295280adebbcd61d2b41931d46..a190379dc3f5c6861ef41c26a090c19fa786f173 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -8,7 +8,7 @@
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
- x ∈ {0; }
+ x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
ensures \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index b0051ed27e0b1bfbc32ce2bd44f56dcb28c448c9..b5abca15b2c160af505a51a76002eb97d5e4d74f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -9,7 +9,7 @@ PROJECT_FILE.i:121:[value] Assertion got status valid.
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
- x ∈ {0; }
+ x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
ensures \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index a13fbe47e1cd7dc4cacf83807b514f2736b1efbb..1643a62e02720c08f819e3dad1fdf7a6e822d0a9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -10,7 +10,7 @@ PROJECT_FILE.i:124:[value] Assertion got status valid.
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
- x ∈ {0; }
+ x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
ensures \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index 5633bb0393bf62ea36d09c26b541a4de25cf9616..f37068cb22c5a93aba6b610938f585f7c10481a7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -9,7 +9,7 @@ PROJECT_FILE.i:121:[value] Assertion got status valid.
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
- x ∈ {0; }
+ x ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
ensures \false;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 6e20d0851470716b00a57637b8034ba9bf539960..0229ed833c17916e8b92750b26aac5b3d7ffa4ea 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -21,38 +21,38 @@
open Db_types
open Cil_types
+open Cil_datatype
open Cil
(* ************************************************************************** *)
(* General constructs *)
(* ************************************************************************** *)
-let unknown_loc = Cil_datatype.Location.unknown
+let new_lval ?(loc=Location.unknown) v = new_exp ~loc (Lval (var v))
-let new_lval v = new_exp ~loc:unknown_loc (Lval (var v))
-
-let mk_call ?result fname args =
+let mk_call ?(loc=Location.unknown) ?result fname args =
(* the type is incorrect, but it doesn't matter *)
(* [JS 2011/04/12] should not generate a new variable by function name *)
- let f = new_lval (makeGlobalVar fname voidType) in
- mkStmt ~valid_sid:true (Instr(Call(result, f, args, unknown_loc)))
+ let f = new_lval ~loc (makeGlobalVar fname voidType) in
+ mkStmt ~valid_sid:true (Instr(Call(result, f, args, loc)))
exception Typing_error of string
let type_error s = raise (Typing_error s)
let not_yet s =
- Options.not_yet_implemented "construct `%s' is not yet supported" s
+ Options.not_yet_implemented "construct `%s' is not yet supported." s
let e_acsl_header () = GText (Read_header.text ())
(* Build a C conditional doing a runtime assertion check. *)
let mk_if e p =
+ let loc = p.loc in
let no_uni = Parameters.Unicode.get () in
Parameters.Unicode.off ();
let msg = Pretty_utils.sfprintf "%a@?" Cil.d_predicate_named p in
Parameters.Unicode.set no_uni;
- let s = mk_call "e_acsl_fail" [ mkString unknown_loc msg ] in
- mkStmt ~valid_sid:true (If(e, mkBlock [ s ], mkBlock [], unknown_loc))
+ let s = mk_call ~loc "e_acsl_fail" [ mkString loc msg ] in
+ mkStmt ~valid_sid:true (If(e, mkBlock [ s ], mkBlock [], loc))
(* ************************************************************************** *)
(* GMP values *)
@@ -95,7 +95,7 @@ end = struct
| TPtr(TInt(IChar, _), _) ->
"str",
(* decimal base for the number given as string *)
- [ e; integer ~loc:unknown_loc 10 ]
+ [ e; integer ~loc:Location.unknown 10 ]
| _ -> assert false
in
mk_call ("mpz_init_set_" ^ fname) (v :: args)
@@ -130,7 +130,7 @@ end = struct
makeVarinfo
~logic:false
~generated:true
- false (* is a global ? *)
+ false (* is a global? *)
false (* is a formal? *)
("e_acsl_cst_" ^ string_of_int !var_cpt)
ty
@@ -179,18 +179,18 @@ end
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)
-let constant_to_exp = function
+let constant_to_exp ?(loc=Location.unknown) = function
| CInt64(n, k, s) ->
(match k with
(* [JS 2011/04/12] why 3 distinct cases here (and not only 2)?
Should be something different between signed and unsigned type? *)
| IBool | IChar | IUChar | IUInt | IUShort | IULong ->
- kinteger64_repr ~loc:unknown_loc k n s
+ kinteger64_repr ?loc k n s
| ISChar | IShort | IInt | ILong ->
- kinteger64_repr ~loc:unknown_loc k n s
+ kinteger64_repr ?loc k n s
| ILongLong | IULongLong ->
- mkString ~loc:unknown_loc (Int64.to_string n))
- | CStr _ as c -> new_exp unknown_loc (Const c)
+ mkString ?loc (Int64.to_string n))
+ | CStr _ as c -> new_exp ?loc (Const c)
| CWStr _ -> not_yet "wide character string constant"
| CChr _ -> not_yet "character constant"
| CReal _ -> not_yet "floating point constant"
@@ -225,19 +225,20 @@ let wrap_leaf e = function
| Lreal -> not_yet "real number"
| Larrow _ -> not_yet "logic function"
-let rec term_to_exp t = match t.term_node with
- | TConst c -> wrap_leaf (constant_to_exp c) t.term_type
- | TLval lv ->
- wrap_leaf (new_exp ~loc:unknown_loc (Lval (tlval_to_lval lv))) t.term_type
- | TSizeOf ty -> sizeOf ~loc:unknown_loc ty
+let rec term_to_exp t =
+ let loc = t.term_loc in
+ match t.term_node with
+ | TConst c -> wrap_leaf (constant_to_exp ~loc c) t.term_type
+ | TLval lv -> wrap_leaf (new_exp ~loc (Lval (tlval_to_lval lv))) t.term_type
+ | TSizeOf ty -> sizeOf ~loc ty
| TSizeOfE t ->
let e = term_to_exp t in
- sizeOf ~loc:unknown_loc (typeOf e)
- | TSizeOfStr s -> new_exp ~loc:unknown_loc (SizeOfStr s)
- | TAlignOf ty -> new_exp ~loc:unknown_loc (AlignOf ty)
+ sizeOf ~loc (typeOf e)
+ | TSizeOfStr s -> new_exp ~loc (SizeOfStr s)
+ | TAlignOf ty -> new_exp ~loc (AlignOf ty)
| TAlignOfE t ->
let e = term_to_exp t in
- new_exp ~loc:unknown_loc (AlignOfE e)
+ new_exp ~loc (AlignOfE e)
| TUnOp(Neg | BNot as op, t) ->
let e = term_to_exp t in
assert (Mpz.e_got_t e);
@@ -246,33 +247,36 @@ let rec term_to_exp t = match t.term_node with
| BNot -> "mpz_com"
| LNot -> assert false
in
- New_vars.push_and_mpz_init (fun _ ev -> mk_call name [ ev; e ])
+ New_vars.push_and_mpz_init (fun _ ev -> mk_call ~loc name [ ev; e ])
| TUnOp(LNot, t) ->
let e = term_to_exp t in
let ty = typeOf e in
assert (not (Mpz.is_t ty));
- new_exp ~loc:unknown_loc (UnOp(LNot, e, ty))
+ new_exp ~loc (UnOp(LNot, e, ty))
| TBinOp(PlusA | MinusA | Mult | Div | Mod as bop, t1, t2) ->
(* arithmetic binary operator *)
let e1 = term_to_exp t1 in
let e2 = term_to_exp t2 in
assert (Cil_datatype.Typ.equal (typeOf e1) (typeOf e2));
let name = name_of_mpz_arith_bop bop in
-(* [JS 2011/04/13] TODO: issue with order of generation.
- New_vars.push_and_mpz_init pushes variables and their initialisations first,
- while New_block.push pushes stmts just after them. *)
-(* (* guarding divisions and modulos *)
+ (* guarding divisions and modulos *)
(match bop with
| Div | Mod ->
- let z = Logic_const.tinteger 0 in
- let guard = comparison_to_exp Eq t2 z in
- New_block.push (mk_if guard (Logic_const.prel (Req, t2, z)))
+ (* [JS 2011/04/13] TODO: issue with order of generation.
+ New_vars.push_and_mpz_init pushes variables and their initialisations
+ first, while New_block.push pushes stmts just after them. *)
+ Options.warning ~current:true ~once:true
+ "missing guard for ensuring that %a is different of 0"
+ d_term t2;
+ (* let z = Logic_const.tinteger 0 in
+ let guard = comparison_to_exp Eq t2 z in
+ New_block.push (mk_if guard (Logic_const.prel (Req, t2, z)))*)
| _ ->
- ());*)
- New_vars.push_and_mpz_init (fun _ e -> mk_call name [ e; e1; e2 ])
+ ());
+ New_vars.push_and_mpz_init (fun _ e -> mk_call ~loc name [ e; e1; e2 ])
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
- comparison_to_exp bop t1 t2
+ comparison_to_exp ~loc bop t1 t2
| TBinOp((Shiftlt | Shiftrt), _, _) ->
(* left/right shift *)
not_yet "left/right shift"
@@ -284,13 +288,17 @@ let rec term_to_exp t = match t.term_node with
(* [TODO] untested *)
let e1 = term_to_exp t1 in
let e2 = term_to_exp t2 in
+ Options.warning ~current:true ~once:true
+ "missing guard for ensuring that %a is a valid pointer"
+ d_term t;
(* the type of the result is the same than type of the pointer [e1],
whatever is [e2] *)
- new_exp ~loc:unknown_loc (BinOp(bop, e1, e2, typeOf e1))
+ new_exp ~loc (BinOp(bop, e1, e2, typeOf e1))
| TCastE(ty, t) ->
+ (* [TODO] missing guard for ensuring no overflow when casting *)
let e = term_to_exp t in
mkCast e ty
- | TAddrOf lv -> mkAddrOf unknown_loc (tlval_to_lval lv)
+ | TAddrOf lv -> mkAddrOf ~loc (tlval_to_lval lv)
| TStartOf _ -> not_yet "beginning of an array"
| Tapp _ -> not_yet "applying logic function"
| Tlambda _ -> not_yet "functional"
@@ -312,7 +320,7 @@ let rec term_to_exp t = match t.term_node with
| Trange _ -> not_yet "range"
| Tlet _ -> not_yet "let binding"
-and comparison_to_exp bop t1 t2 =
+and comparison_to_exp ?(loc=Location.unknown) bop t1 t2 =
let e1 = term_to_exp t1 in
let e2 = term_to_exp t2 in
(* Options.feedback "ty1=%a; ty2=%a" d_type (typeOf e1) d_type (typeOf e2);*)
@@ -323,18 +331,20 @@ and comparison_to_exp bop t1 t2 =
intType
(fun v _ -> mk_call ~result:(var v) "mpz_cmp" [ e1; e2 ])
in
- new_exp unknown_loc (BinOp(bop, e, zero unknown_loc, intType))
+ new_exp ?loc (BinOp(bop, e, zero ?loc, intType))
else
- new_exp unknown_loc (BinOp(bop, e1, e2, intType))
+ new_exp ?loc (BinOp(bop, e1, e2, intType))
(* convert an ACSL named predicate into the opposite C expression (if any).
E.g. \true is converted into 0. *)
-let rec named_predicate_to_revexp p = match p.content with
- | Pfalse -> one ~loc:unknown_loc
- | Ptrue -> zero ~loc:unknown_loc
+let rec named_predicate_to_revexp p =
+ let loc = p.loc in
+ match p.content with
+ | Pfalse -> one ~loc
+ | Ptrue -> zero ~loc
| Papp _ -> not_yet "logic function application"
| Pseparated _ -> not_yet "separated"
- | Prel(rel, t1, t2) -> comparison_to_exp (relation_to_revbinop rel) t1 t2
+ | Prel(rel, t1, t2) -> comparison_to_exp ~loc (relation_to_revbinop rel) t1 t2
| Pand _ -> not_yet "&&"
| Por _ -> not_yet "||"
| Pxor _ -> not_yet "xor"
@@ -342,7 +352,7 @@ let rec named_predicate_to_revexp p = match p.content with
| Piff _ -> not_yet "<==>"
| Pnot p ->
let e = named_predicate_to_revexp p in
- new_exp unknown_loc (UnOp(Neg, e, TInt(IInt, [])))
+ new_exp ~loc (UnOp(Neg, e, TInt(IInt, [])))
| Pif _ -> not_yet "_ ? _ : _"
| Plet _ -> not_yet "let _ = _ in _"
| Pforall _ -> not_yet "\\forall"