From b543078e04af864e9c9e7ba8544b89ffd2705d9b Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Mon, 30 Aug 2021 15:05:17 +0200
Subject: [PATCH] [e-acsl] fix assigns clauses for generated logic functions
---
src/plugins/e-acsl/Makefile.in | 1 -
.../src/code_generator/logic_functions.ml | 140 +++++++----
.../e-acsl/src/code_generator/smart_term.ml | 78 ------
.../e-acsl/src/code_generator/smart_term.mli | 33 ---
.../arith/oracle/functions_rec.res.oracle | 232 ------------------
.../e-acsl/tests/arith/oracle/gen_functions.c | 11 +-
.../tests/arith/oracle/gen_functions_rec.c | 126 ++--------
.../tests/bts/oracle/gen_issue-eacsl-177.c | 14 +-
.../tests/gmp-only/oracle/gen_functions.c | 21 +-
9 files changed, 129 insertions(+), 527 deletions(-)
delete mode 100644 src/plugins/e-acsl/src/code_generator/smart_term.ml
delete mode 100644 src/plugins/e-acsl/src/code_generator/smart_term.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e3538068d25..18869a85f29 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -77,7 +77,6 @@ CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))
SRC_CODE_GENERATOR:= \
smart_exp \
smart_stmt \
- smart_term \
gmp \
label \
env \
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 2d60e2c9f17..3d771f9ec37 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+exception NoAssigns
+
(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)
@@ -56,6 +58,59 @@ let result_as_extra_argument = Gmp_types.Z.is_t
(* TODO: to be extended to any compound type? E.g. returning a struct is not
good practice... *)
+(*****************************************************************************)
+(****************** Generation of function assigns ***************************)
+(*****************************************************************************)
+let rec ptr_free typ = match Cil.unrollType typ with
+ | TVoid _
+ | TInt (_, _)
+ | TFloat (_, _) -> true
+ | TPtr (_, _) -> false
+ | TArray (ty, _, _, _) -> ptr_free ty
+ | TFun (_, _, _, _) ->
+ (* a fucntion cannot be an argument of a function *)
+ assert false
+ | TNamed (_, _) ->
+ (* The named types are unfolded with [Cil.unrolltype] *)
+ assert false
+ | TEnum (_, _)
+ | TBuiltin_va_list _ -> true
+ | TComp (cinfo, _, _) ->
+ match cinfo.cfields with
+ | None -> assert false
+ | Some fields -> List.for_all
+ (fun fi -> (fi.fbitfield != None)||(ptr_free fi.ftype))
+ fields
+
+let deref_gmp_arg ~loc var =
+ Smart_exp.lval ~loc
+ (Mem (Cil.mkAddrOrStartOf ~loc (Var var , NoOffset)), NoOffset)
+
+let rec get_assigns_from ~loc env lprofile =
+ match lprofile with
+ | [] -> []
+ | lvar :: lvars ->
+ let var = Env.Logic_binding.get env lvar in
+ if ptr_free var.vtype then
+ (Smart_exp.lval ~loc (Cil.var var)) :: (get_assigns_from ~loc env lvars)
+ else if lvar.lv_type == Linteger then
+ (deref_gmp_arg ~loc var) :: (get_assigns_from ~loc env lvars)
+ else begin
+ Options.warning ~current:true "Generating assigns clause for arguments \
+ with pointers is not supported, skipping \
+ assigns clause";
+ raise NoAssigns
+ end
+
+let get_gmp_integer ~loc vi =
+ Smart_exp.lval
+ ~loc
+ (Mem
+ (Smart_exp.lval
+ ~loc
+ (Var vi, NoOffset)),
+ (Index (Cil.zero ~loc, NoOffset)))
+
(*****************************************************************************)
(****************** Generation of function bodies ****************************)
(*****************************************************************************)
@@ -147,22 +202,16 @@ let generate_kf ~loc fname env ret_ty params_ty li =
([], [])
in
(* build the varinfo storing the result *)
- let ret_vi, ret_ty, params_with_ret, params_ty_with_ret, extra_arg =
+ let res_as_extra_arg = result_as_extra_argument ret_ty in
+ let ret_vi, ret_ty, params_with_ret, params_ty_with_ret =
let vname = "__retres" in
- if result_as_extra_argument ret_ty then
+ if res_as_extra_arg then
let ret_ty_ptr = TPtr(ret_ty, []) (* call by reference *) in
let vname = vname ^ "_arg" in
let vi = Cil.makeVarinfo false true vname ret_ty_ptr in
- vi,
- Cil.voidType,
- vi :: params, (vname, ret_ty_ptr, []) :: params_ty_vi,
- true
+ vi, Cil.voidType, vi :: params, (vname, ret_ty_ptr, []) :: params_ty_vi
else
- Cil.makeVarinfo false false vname ret_ty,
- ret_ty,
- params,
- params_ty_vi,
- false
+ Cil.makeVarinfo false false vname ret_ty, ret_ty, params, params_ty_vi
in
(* build the function's varinfo *)
let vi =
@@ -219,45 +268,35 @@ let generate_kf ~loc fname env ret_ty params_ty li =
in
List.fold_left2 add env li.l_profile params
in
- let assigned_var =
- let loc = Location.unknown in
- if extra_arg
- then
- (* If the result is passed as argument, it is of type __e_acsl_mpz_t
- accessing the left value which is assigned is then done by
- *__retres_arg[0] *)
- let vi_res = match params_with_ret with
- | vi :: _ -> vi
- | [] -> assert false
- in
- Logic_const.new_identified_term
- (Smart_term.array_at0 ~loc
- (Smart_term.deref ~
- loc
- (Logic_const.tvar (Cil.cvar_to_lvar vi_res))))
- else
- Logic_const.new_identified_term (Logic_const.tresult fundec.svar.vtype)
- in
- let rec deref_all tm cty deps =
- if Smart_term.is_pointer_type cty then
- deref_all
- (Smart_term.deref ~loc ~cty tm)
- (Smart_term.deref_cty cty)
- ((Logic_const.new_identified_term tm)::deps)
- else
- (Logic_const.new_identified_term tm)::deps
+ let assigns_from =
+ try Some (get_assigns_from Location.unknown env li.l_profile)
+ with NoAssigns -> None
in
- let deps = List.fold_right2
- (fun lv (_,cty,_) -> deref_all (Logic_const.tvar lv) cty)
- li.l_profile params_ty_vi
- []
+ let assigned_var =
+ if res_as_extra_arg then
+ Logic_const.new_identified_term
+ (Logic_utils.expr_to_term (get_gmp_integer Location.unknown ret_vi))
+ else
+ Logic_const.new_identified_term (Logic_const.tresult fundec.svar.vtype)
in
- Annotations.add_assigns
- ~keep_empty:false
- Options.emitter
- ~behavior:Cil.default_behavior_name
- kf
- (Writes [ assigned_var , From deps]);
+ begin
+ match assigns_from with
+ | None -> ()
+ | Some assigns_from ->
+ let assigns_from =
+ List.map
+ (fun e ->
+ Logic_const.new_identified_term
+ (Logic_utils.expr_to_term e))
+ assigns_from
+ in
+ Annotations.add_assigns
+ ~keep_empty:false
+ Options.emitter
+ ~behavior:Cil.default_behavior_name
+ kf
+ (Writes [ assigned_var , From assigns_from]);
+ end;
let b, env = generate_body ~loc kf env ret_ty ret_vi li.l_body in
fundec.sbody <- b;
(* add the generated variables in the necessary lists *)
@@ -265,7 +304,10 @@ let generate_kf ~loc fname env ret_ty params_ty li =
[add_generated_variables_in_function] in the main visitor *)
let vars =
let l = Env.get_generated_variables env in
- if ret_vi.vdefined then (ret_vi, Env.LFunction kf) :: l else l
+ if ret_vi.vdefined then
+ (ret_vi, Env.LFunction kf) :: l
+ else
+ l
in
let locals, blocks =
List.fold_left
diff --git a/src/plugins/e-acsl/src/code_generator/smart_term.ml b/src/plugins/e-acsl/src/code_generator/smart_term.ml
deleted file mode 100644
index 73746edfebf..00000000000
--- a/src/plugins/e-acsl/src/code_generator/smart_term.ml
+++ /dev/null
@@ -1,78 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-let is_pointer_type cty =
- let cty = Cil.unrollType cty in
- match cty with
- | TInt(_,_)
- | TVoid _
- | TFloat(_,_)
- | TFun(_,_,_,_)
- | TBuiltin_va_list _
- | TComp (_,_,_)
- | TNamed (_,_)
- | TEnum (_,_)
- -> false
- | TPtr(_,_)
- | TArray(_,_,_,_) -> true
-
-let deref_cty cty =
- let cty = Cil.unrollType cty in
- match cty with
- | TInt(_,_)
- | TVoid _
- | TFloat(_,_)
- | TFun(_,_,_,_)
- | TBuiltin_va_list _
- | TComp (_,_,_)
- | TNamed (_,_)
- | TEnum (_,_)
- -> Options.fatal "recieved the type %a when a pointer type was expected"
- Printer.pp_typ cty
- | TPtr(cty,_)
- | TArray(cty,_,_,_)
- -> cty
-
-let deref_lty ?cty lty = match lty with
- | Lreal | Lvar _ | Larrow (_ , _) | Ltype (_ , _)->
- Options.fatal "recieved the type %a when a pointer type was expected"
- Printer.pp_logic_type lty
- | Ctype cty -> Ctype (deref_cty cty)
- | Linteger ->
- match cty with
- | None -> Options.fatal "recieved the type %a when a pointer type was expected"
- Printer.pp_logic_type lty
- | Some cty -> Ctype (deref_cty cty)
-
-let logic_type ?cty = function
- | TVar vi -> vi.lv_type
- | TResult ty -> Ctype ty
- | TMem tm -> deref_lty ?cty tm.term_type
-
-let lval ?cty ~loc (thost,_ as tlv) =
- Logic_const.term ~loc (TLval tlv) (logic_type ?cty thost)
-
-let deref ?cty ~loc tlv = lval ?cty ~loc (TMem tlv, TNoOffset)
-
-let array_at0 ~loc tlv = lval ~loc (TMem (Logic_utils.mk_logic_StartOf tlv), TNoOffset)
diff --git a/src/plugins/e-acsl/src/code_generator/smart_term.mli b/src/plugins/e-acsl/src/code_generator/smart_term.mli
deleted file mode 100644
index c2d03b6e88d..00000000000
--- a/src/plugins/e-acsl/src/code_generator/smart_term.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of the Frama-C's E-ACSL plug-in. *)
-(* *)
-(* Copyright (C) 2012-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-val is_pointer_type : typ -> bool
-
-val deref_cty : typ -> typ
-
-val lval : ?cty:typ -> loc:location -> term_lval -> term
-
-val deref : ?cty:typ -> loc:location -> term -> term
-
-val array_at0 : loc:location -> term -> term
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
index 91cd6ea7f26..c2c703a86c9 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
@@ -18,18 +18,6 @@
Using specification of function __gen_e_acsl_f1_3 for recursive calls.
Analysis of function __gen_e_acsl_f1_3 is thus incomplete and its soundness
relies on the written specification.
-[inout] tests/arith/functions_rec.c:10: Warning:
- failed to interpret inputs in assigns clause 'assigns
- *((__e_acsl_mpz_struct *)*__retres_arg)
- \from *n, n;'
-[eva] tests/arith/functions_rec.c:10: Warning:
- cannot interpret \from clause *n (unsupported logic var n);
- effects will be ignored
-[eva] tests/arith/functions_rec.c:10: Warning:
- cannot interpret \from clause n (unsupported logic var n);
- effects will be ignored
-[eva:locals-escaping] tests/arith/functions_rec.c:10: Warning:
- locals {__gen_e_acsl__4, __gen_e_acsl_le, __gen_e_acsl_if} escaping the scope of __gen_e_acsl_f1_3 through __gen_e_acsl_f1_5
[eva:alarm] tests/arith/functions_rec.c:30: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:30: Warning:
@@ -44,16 +32,6 @@
Using specification of function __gen_e_acsl_f2_3 for recursive calls.
Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
relies on the written specification.
-[inout] tests/arith/functions_rec.c:13: Warning:
- failed to interpret inputs in assigns clause 'assigns \result \from *n, n;'
-[eva] tests/arith/functions_rec.c:13: Warning:
- cannot interpret \from clause *n (unsupported logic var n);
- effects will be ignored
-[eva] tests/arith/functions_rec.c:13: Warning:
- cannot interpret \from clause n (unsupported logic var n);
- effects will be ignored
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl__11, __gen_e_acsl_lt, __gen_e_acsl_if_4} escaping the scope of __gen_e_acsl_f2_3 through \result<__gen_e_acsl_f2_3>
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
@@ -61,16 +39,6 @@
Using specification of function __gen_e_acsl_f2_3 for recursive calls.
Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
relies on the written specification.
-[inout] tests/arith/functions_rec.c:13: Warning:
- failed to interpret inputs in assigns clause 'assigns \result \from *n, n;'
-[eva] tests/arith/functions_rec.c:13: Warning:
- cannot interpret \from clause *n (unsupported logic var n);
- effects will be ignored
-[eva] tests/arith/functions_rec.c:13: Warning:
- cannot interpret \from clause n (unsupported logic var n);
- effects will be ignored
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl__11, __gen_e_acsl_lt, __gen_e_acsl_if_4} escaping the scope of __gen_e_acsl_f2_3 through \result<__gen_e_acsl_f2_3>
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
@@ -78,27 +46,8 @@
Using specification of function __gen_e_acsl_f2_3 for recursive calls.
Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
relies on the written specification.
-[inout] tests/arith/functions_rec.c:13: Warning:
- failed to interpret inputs in assigns clause 'assigns \result \from *n, n;'
-[eva] tests/arith/functions_rec.c:13: Warning:
- cannot interpret \from clause *n (unsupported logic var n);
- effects will be ignored
-[eva] tests/arith/functions_rec.c:13: Warning:
- cannot interpret \from clause n (unsupported logic var n);
- effects will be ignored
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl__11, __gen_e_acsl_lt, __gen_e_acsl_if_4} escaping the scope of __gen_e_acsl_f2_3 through \result<__gen_e_acsl_f2_3>
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_9);
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_5);
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_7);
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
division by zero. assert __gen_e_acsl_f2_9 ≢ 0;
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
@@ -106,38 +55,17 @@
assert -2147483648 ≤ __gen_e_acsl_f2_5 * __gen_e_acsl_f2_7;
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
signed overflow. assert __gen_e_acsl_f2_5 * __gen_e_acsl_f2_7 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- signed overflow.
- assert
- -2147483648 ≤
- (int)(__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7) / __gen_e_acsl_f2_9;
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
signed overflow.
assert
(int)(__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7) / __gen_e_acsl_f2_9 ≤
2147483647;
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl__12, __gen_e_acsl_sub_4, __gen_e_acsl_f2_5,
- __gen_e_acsl__13, __gen_e_acsl_sub_5, __gen_e_acsl_f2_7,
- __gen_e_acsl__14, __gen_e_acsl_sub_6, __gen_e_acsl_f2_9} escaping the scope of a block of __gen_e_acsl_f2_3 through __gen_e_acsl_if_4
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_4);
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_14);
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_10);
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_12);
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
division by zero. assert __gen_e_acsl_f2_14 ≢ 0;
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
@@ -146,39 +74,11 @@
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
signed overflow.
assert __gen_e_acsl_f2_10 * __gen_e_acsl_f2_12 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- signed overflow.
- assert
- -2147483648 ≤
- (int)(__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12) / __gen_e_acsl_f2_14;
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
signed overflow.
assert
(int)(__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12) / __gen_e_acsl_f2_14 ≤
2147483647;
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl_n_3, __gen_e_acsl__10, __gen_e_acsl_sub_3,
- __gen_e_acsl_f2_10, __gen_e_acsl__15, __gen_e_acsl_sub_7,
- __gen_e_acsl_f2_12, __gen_e_acsl__16, __gen_e_acsl_sub_8,
- __gen_e_acsl_f2_14} escaping the scope of a block of __gen_e_acsl_f2_2 through __gen_e_acsl_if_5
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_5);
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl_if_5} escaping the scope of __gen_e_acsl_f2_2 through \result<__gen_e_acsl_f2_2>
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl_if_5} escaping the scope of __gen_e_acsl_f2_2 through \result<__gen_e_acsl_f2_2>
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl_if_5} escaping the scope of __gen_e_acsl_f2_2 through \result<__gen_e_acsl_f2_2>
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_19);
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_15);
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_17);
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
division by zero. assert __gen_e_acsl_f2_19 ≢ 0;
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
@@ -187,26 +87,11 @@
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
signed overflow.
assert __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:13: Warning:
- signed overflow.
- assert
- -2147483648 ≤
- (int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19;
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
signed overflow.
assert
(int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19 ≤
2147483647;
-[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
- locals {__gen_e_acsl_f2_15, __gen_e_acsl_f2_17, __gen_e_acsl_f2_19} escaping the scope of a block of __gen_e_acsl_f2 through __gen_e_acsl_if_6
-[eva:alarm] tests/arith/functions_rec.c:32: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_6);
-[eva:locals-escaping] tests/arith/functions_rec.c:32: Warning:
- locals {__gen_e_acsl_if_6} escaping the scope of __gen_e_acsl_f2 through \result<__gen_e_acsl_f2>
-[eva:alarm] tests/arith/functions_rec.c:32: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f2_20);
[eva:alarm] tests/arith/functions_rec.c:32: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:32: Warning:
@@ -221,84 +106,9 @@
Using specification of function __gen_e_acsl_f3_3 for recursive calls.
Analysis of function __gen_e_acsl_f3_3 is thus incomplete and its soundness
relies on the written specification.
-[inout] tests/arith/functions_rec.c:17: Warning:
- failed to interpret inputs in assigns clause 'assigns \result \from *n, n;'
-[eva] tests/arith/functions_rec.c:17: Warning:
- cannot interpret \from clause *n (unsupported logic var n);
- effects will be ignored
-[eva] tests/arith/functions_rec.c:17: Warning:
- cannot interpret \from clause n (unsupported logic var n);
- effects will be ignored
-[eva:locals-escaping] tests/arith/functions_rec.c:17: Warning:
- locals {__gen_e_acsl__18, __gen_e_acsl_gt, __gen_e_acsl_if_7} escaping the scope of __gen_e_acsl_f3_3 through \result<__gen_e_acsl_f3_3>
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f3_5);
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow. assert -2147483648 ≤ __gen_e_acsl_g_6 * __gen_e_acsl_f3_5;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow. assert __gen_e_acsl_g_6 * __gen_e_acsl_f3_5 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow.
- assert -2147483648 ≤ (int)(__gen_e_acsl_g_6 * __gen_e_acsl_f3_5) - 5;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow.
- assert (int)(__gen_e_acsl_g_6 * __gen_e_acsl_f3_5) - 5 ≤ 2147483647;
[eva:alarm] tests/arith/functions_rec.c:17: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
-[eva:locals-escaping] tests/arith/functions_rec.c:17: Warning:
- locals {__gen_e_acsl_g_6, __gen_e_acsl__19, __gen_e_acsl_sub_10,
- __gen_e_acsl_f3_5} escaping the scope of a block of __gen_e_acsl_f3_3 through __gen_e_acsl_if_7
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_7);
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f3_6);
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow. assert -2147483648 ≤ __gen_e_acsl_g_4 * __gen_e_acsl_f3_6;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow. assert __gen_e_acsl_g_4 * __gen_e_acsl_f3_6 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow.
- assert -2147483648 ≤ (int)(__gen_e_acsl_g_4 * __gen_e_acsl_f3_6) - 5;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow.
- assert (int)(__gen_e_acsl_g_4 * __gen_e_acsl_f3_6) - 5 ≤ 2147483647;
-[eva:locals-escaping] tests/arith/functions_rec.c:17: Warning:
- locals {__gen_e_acsl_g_4, __gen_e_acsl_n_4, __gen_e_acsl__17,
- __gen_e_acsl_sub_9, __gen_e_acsl_f3_6} escaping the scope of a block of __gen_e_acsl_f3_2 through __gen_e_acsl_if_8
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_8);
-[eva:locals-escaping] tests/arith/functions_rec.c:17: Warning:
- locals {__gen_e_acsl_if_8} escaping the scope of __gen_e_acsl_f3_2 through \result<__gen_e_acsl_f3_2>
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f3_7);
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow. assert -2147483648 ≤ __gen_e_acsl_g_2 * __gen_e_acsl_f3_7;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow. assert __gen_e_acsl_g_2 * __gen_e_acsl_f3_7 ≤ 2147483647;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow.
- assert -2147483648 ≤ (int)(__gen_e_acsl_g_2 * __gen_e_acsl_f3_7) - 5;
-[eva:alarm] tests/arith/functions_rec.c:17: Warning:
- signed overflow.
- assert (int)(__gen_e_acsl_g_2 * __gen_e_acsl_f3_7) - 5 ≤ 2147483647;
-[eva:locals-escaping] tests/arith/functions_rec.c:17: Warning:
- locals {__gen_e_acsl_g_2, __gen_e_acsl_f3_7} escaping the scope of a block of __gen_e_acsl_f3 through __gen_e_acsl_if_9
-[eva:alarm] tests/arith/functions_rec.c:34: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_9);
-[eva:locals-escaping] tests/arith/functions_rec.c:34: Warning:
- locals {__gen_e_acsl_if_9} escaping the scope of __gen_e_acsl_f3 through \result<__gen_e_acsl_f3>
-[eva:alarm] tests/arith/functions_rec.c:34: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f3_8);
-[eva:alarm] tests/arith/functions_rec.c:34: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:34: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/functions_rec.c:20: Warning:
@@ -311,48 +121,6 @@
Using specification of function __gen_e_acsl_f4_3 for recursive calls.
Analysis of function __gen_e_acsl_f4_3 is thus incomplete and its soundness
relies on the written specification.
-[inout] tests/arith/functions_rec.c:20: Warning:
- failed to interpret inputs in assigns clause 'assigns \result \from *n, n;'
-[eva] tests/arith/functions_rec.c:20: Warning:
- cannot interpret \from clause *n (unsupported logic var n);
- effects will be ignored
-[eva] tests/arith/functions_rec.c:20: Warning:
- cannot interpret \from clause n (unsupported logic var n);
- effects will be ignored
-[eva:locals-escaping] tests/arith/functions_rec.c:20: Warning:
- locals {__gen_e_acsl__23, __gen_e_acsl_lt_2, __gen_e_acsl_if_11} escaping the scope of __gen_e_acsl_f4_3 through \result<__gen_e_acsl_f4_3>
-[eva:alarm] :0: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f4_5);
-[eva:locals-escaping] tests/arith/functions_rec.c:20: Warning:
- locals {__gen_e_acsl__24, __gen_e_acsl_add_7, __gen_e_acsl_f4_5} escaping the scope of a block of __gen_e_acsl_f4_3 through __gen_e_acsl_if_11
-[eva:alarm] tests/arith/functions_rec.c:20: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_11);
-[eva:alarm] :0: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f4_6);
-[eva:locals-escaping] tests/arith/functions_rec.c:20: Warning:
- locals {__gen_e_acsl_n_6, __gen_e_acsl__22, __gen_e_acsl_add_6,
- __gen_e_acsl_f4_6} escaping the scope of a block of __gen_e_acsl_f4_2 through __gen_e_acsl_if_13
-[eva:alarm] tests/arith/functions_rec.c:20: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_13);
-[eva:locals-escaping] tests/arith/functions_rec.c:20: Warning:
- locals {__gen_e_acsl_if_13} escaping the scope of __gen_e_acsl_f4_2 through \result<__gen_e_acsl_f4_2>
-[eva:alarm] :0: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f4_7);
-[eva:locals-escaping] :0: Warning:
- locals {__gen_e_acsl_f4_7} escaping the scope of a block of __gen_e_acsl_f4 through __gen_e_acsl_if_15
-[eva:alarm] tests/arith/functions_rec.c:36: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_if_15);
-[eva:locals-escaping] tests/arith/functions_rec.c:36: Warning:
- locals {__gen_e_acsl_if_15} escaping the scope of __gen_e_acsl_f4 through \result<__gen_e_acsl_f4>
-[eva:alarm] tests/arith/functions_rec.c:36: Warning:
- accessing left-value that contains escaping addresses.
- assert ¬\dangling(&__gen_e_acsl_f4_8);
[eva:alarm] tests/arith/functions_rec.c:36: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:36: Warning:
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index 41efac7324d..becea12ff18 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -275,7 +275,7 @@ int __gen_e_acsl_p2_5(int x, long y)
}
/*@ assigns \result;
- assigns \result \from x, *y, y; */
+ assigns \result \from x, *((__e_acsl_mpz_struct *)y); */
int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
{
__e_acsl_mpz_t __gen_e_acsl_x;
@@ -304,8 +304,8 @@ long __gen_e_acsl_f1(int x, int y)
return __retres;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from x, *y, y;
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from x, *((__e_acsl_mpz_struct *)y);
*/
void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
__e_acsl_mpz_struct * y)
@@ -324,8 +324,9 @@ void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from *x, x, *y, y;
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0]
+ \from *((__e_acsl_mpz_struct *)x), *((__e_acsl_mpz_struct *)y);
*/
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
index 9461cbf897d..b63ae684d46 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
@@ -107,7 +107,6 @@ int main(void)
{
int __gen_e_acsl_f2_20;
__gen_e_acsl_f2_20 = __gen_e_acsl_f2(7);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_20); */
__e_acsl_assert(__gen_e_acsl_f2_20 == 1,1,"Assertion","main",
"f2(7) == 1","tests/arith/functions_rec.c",32);
}
@@ -115,7 +114,6 @@ int main(void)
{
int __gen_e_acsl_f3_8;
__gen_e_acsl_f3_8 = __gen_e_acsl_f3(6);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f3_8); */
__e_acsl_assert(__gen_e_acsl_f3_8 == -5,1,"Assertion","main",
"f3(6) == -5","tests/arith/functions_rec.c",34);
}
@@ -123,7 +121,6 @@ int main(void)
{
unsigned long __gen_e_acsl_f4_8;
__gen_e_acsl_f4_8 = __gen_e_acsl_f4(9);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f4_8); */
__e_acsl_assert(__gen_e_acsl_f4_8 > 0UL,1,"Assertion","main","f4(9) > 0",
"tests/arith/functions_rec.c",36);
}
@@ -163,9 +160,8 @@ int main(void)
return __retres;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from n;
- */
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
{
__e_acsl_mpz_t __gen_e_acsl_if_3;
@@ -198,9 +194,8 @@ void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from n;
- */
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n)
{
__e_acsl_mpz_t __gen_e_acsl_if_2;
@@ -247,8 +242,8 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from *n, n;
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/
void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
{
@@ -311,12 +306,9 @@ int __gen_e_acsl_f2(int n)
__gen_e_acsl_f2_15 = __gen_e_acsl_f2_2(n - 1L);
__gen_e_acsl_f2_17 = __gen_e_acsl_f2_2(n - 2L);
__gen_e_acsl_f2_19 = __gen_e_acsl_f2_2(n - 3L);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_19); */
__e_acsl_assert(__gen_e_acsl_f2_19 != 0,1,"RTE","f2",
"division_by_zero: __gen_e_acsl_f2_19 != 0",
"tests/arith/functions_rec.c",13);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_15); */
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_17); */
/*@ assert Eva: division_by_zero: __gen_e_acsl_f2_19 ≢ 0; */
/*@ assert
Eva: signed_overflow:
@@ -326,11 +318,6 @@ int __gen_e_acsl_f2(int n)
Eva: signed_overflow:
__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17 ≤ 2147483647;
*/
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤
- (int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19;
- */
/*@ assert
Eva: signed_overflow:
(int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19
@@ -338,7 +325,6 @@ int __gen_e_acsl_f2(int n)
*/
__gen_e_acsl_if_6 = (__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19;
}
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_6); */
return __gen_e_acsl_if_6;
}
@@ -390,12 +376,9 @@ int __gen_e_acsl_f2_2(long n)
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
*/
__gen_e_acsl_f2_14 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_14); */
__e_acsl_assert(__gen_e_acsl_f2_14 != 0,1,"RTE","f2_2",
"division_by_zero: __gen_e_acsl_f2_14 != 0",
"tests/arith/functions_rec.c",13);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_10); */
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_12); */
/*@ assert Eva: division_by_zero: __gen_e_acsl_f2_14 ≢ 0; */
/*@ assert
Eva: signed_overflow:
@@ -405,11 +388,6 @@ int __gen_e_acsl_f2_2(long n)
Eva: signed_overflow:
__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12 ≤ 2147483647;
*/
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤
- (int)(__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12) / __gen_e_acsl_f2_14;
- */
/*@ assert
Eva: signed_overflow:
(int)(__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12) / __gen_e_acsl_f2_14
@@ -424,12 +402,11 @@ int __gen_e_acsl_f2_2(long n)
__gmpz_clear(__gen_e_acsl__16);
__gmpz_clear(__gen_e_acsl_sub_8);
}
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_5); */
return __gen_e_acsl_if_5;
}
/*@ assigns \result;
- assigns \result \from *n, n; */
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n)
{
__e_acsl_mpz_t __gen_e_acsl__11;
@@ -476,12 +453,9 @@ int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n)
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
*/
__gen_e_acsl_f2_9 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_9); */
__e_acsl_assert(__gen_e_acsl_f2_9 != 0,1,"RTE","f2_3",
"division_by_zero: __gen_e_acsl_f2_9 != 0",
"tests/arith/functions_rec.c",13);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_5); */
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_7); */
/*@ assert Eva: division_by_zero: __gen_e_acsl_f2_9 ≢ 0; */
/*@ assert
Eva: signed_overflow:
@@ -491,11 +465,6 @@ int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n)
Eva: signed_overflow:
__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7 ≤ 2147483647;
*/
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤
- (int)(__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7) / __gen_e_acsl_f2_9;
- */
/*@ assert
Eva: signed_overflow:
(int)(__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7) / __gen_e_acsl_f2_9
@@ -510,7 +479,6 @@ int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n)
__gmpz_clear(__gen_e_acsl_sub_6);
}
__gmpz_clear(__gen_e_acsl__11);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_4); */
return __gen_e_acsl_if_4;
}
@@ -531,7 +499,7 @@ int __gen_e_acsl_g_3(long n)
}
/*@ assigns \result;
- assigns \result \from *n, n; */
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n)
{
int __retres = 0;
@@ -548,23 +516,6 @@ int __gen_e_acsl_f3(int n)
int __gen_e_acsl_f3_7;
__gen_e_acsl_g_2 = __gen_e_acsl_g(n);
__gen_e_acsl_f3_7 = __gen_e_acsl_f3_2(n - 1L);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f3_7); */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ __gen_e_acsl_g_2 * __gen_e_acsl_f3_7;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_g_2 * __gen_e_acsl_f3_7 ≤ 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ (int)(__gen_e_acsl_g_2 * __gen_e_acsl_f3_7) - 5;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_g_2 * __gen_e_acsl_f3_7) - 5 ≤ 2147483647;
- */
__gen_e_acsl_if_9 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_7 - 5;
}
else {
@@ -572,7 +523,6 @@ int __gen_e_acsl_f3(int n)
__gen_e_acsl_g_12 = __gen_e_acsl_g_3(n + 1L);
__gen_e_acsl_if_9 = __gen_e_acsl_g_12;
}
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_9); */
return __gen_e_acsl_if_9;
}
@@ -599,23 +549,6 @@ int __gen_e_acsl_f3_2(long n)
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_9);
*/
__gen_e_acsl_f3_6 = __gen_e_acsl_f3_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_9);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f3_6); */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ __gen_e_acsl_g_4 * __gen_e_acsl_f3_6;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_g_4 * __gen_e_acsl_f3_6 ≤ 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ (int)(__gen_e_acsl_g_4 * __gen_e_acsl_f3_6) - 5;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_g_4 * __gen_e_acsl_f3_6) - 5 ≤ 2147483647;
- */
__gen_e_acsl_if_8 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_6 - 5;
__gmpz_clear(__gen_e_acsl_n_4);
__gmpz_clear(__gen_e_acsl__17);
@@ -638,12 +571,11 @@ int __gen_e_acsl_f3_2(long n)
__gmpz_clear(__gen_e_acsl__21);
__gmpz_clear(__gen_e_acsl_add_5);
}
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_8); */
return __gen_e_acsl_if_8;
}
/*@ assigns \result;
- assigns \result \from *n, n; */
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n)
{
__e_acsl_mpz_t __gen_e_acsl__18;
@@ -667,23 +599,6 @@ int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n)
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_10);
*/
__gen_e_acsl_f3_5 = __gen_e_acsl_f3_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_10);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f3_5); */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ __gen_e_acsl_g_6 * __gen_e_acsl_f3_5;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_g_6 * __gen_e_acsl_f3_5 ≤ 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ (int)(__gen_e_acsl_g_6 * __gen_e_acsl_f3_5) - 5;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_g_6 * __gen_e_acsl_f3_5) - 5 ≤ 2147483647;
- */
__gen_e_acsl_if_7 = __gen_e_acsl_g_6 * __gen_e_acsl_f3_5 - 5;
__gmpz_clear(__gen_e_acsl__19);
__gmpz_clear(__gen_e_acsl_sub_10);
@@ -706,7 +621,6 @@ int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n)
__gmpz_clear(__gen_e_acsl_add_4);
}
__gmpz_clear(__gen_e_acsl__18);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_7); */
return __gen_e_acsl_if_7;
}
@@ -718,7 +632,6 @@ unsigned long __gen_e_acsl_f4(int n)
if (n < 100) {
unsigned long __gen_e_acsl_f4_7;
__gen_e_acsl_f4_7 = __gen_e_acsl_f4_2(n + 1L);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f4_7); */
__gen_e_acsl_if_15 = __gen_e_acsl_f4_7;
}
else {
@@ -727,7 +640,6 @@ unsigned long __gen_e_acsl_f4(int n)
else __gen_e_acsl_if_14 = 6UL;
__gen_e_acsl_if_15 = __gen_e_acsl_if_14;
}
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_15); */
return __gen_e_acsl_if_15;
}
@@ -752,7 +664,6 @@ unsigned long __gen_e_acsl_f4_2(long n)
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
*/
__gen_e_acsl_f4_6 = __gen_e_acsl_f4_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f4_6); */
__gen_e_acsl_if_13 = __gen_e_acsl_f4_6;
__gmpz_clear(__gen_e_acsl_n_6);
__gmpz_clear(__gen_e_acsl__22);
@@ -764,12 +675,11 @@ unsigned long __gen_e_acsl_f4_2(long n)
else __gen_e_acsl_if_12 = 6UL;
__gen_e_acsl_if_13 = __gen_e_acsl_if_12;
}
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_13); */
return __gen_e_acsl_if_13;
}
/*@ assigns \result;
- assigns \result \from *n, n; */
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n)
{
__e_acsl_mpz_t __gen_e_acsl__23;
@@ -791,7 +701,6 @@ unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n)
\initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
*/
__gen_e_acsl_f4_5 = __gen_e_acsl_f4_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f4_5); */
__gen_e_acsl_if_11 = __gen_e_acsl_f4_5;
__gmpz_clear(__gen_e_acsl__24);
__gmpz_clear(__gen_e_acsl_add_7);
@@ -809,13 +718,11 @@ unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n)
__gmpz_clear(__gen_e_acsl__25);
}
__gmpz_clear(__gen_e_acsl__23);
- /*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_if_11); */
return __gen_e_acsl_if_11;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from n;
- */
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n)
{
__e_acsl_mpz_t __gen_e_acsl_if_18;
@@ -848,9 +755,8 @@ void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n)
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from n;
- */
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n)
{
__e_acsl_mpz_t __gen_e_acsl_if_17;
@@ -893,8 +799,8 @@ void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from *n, n;
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/
void __gen_e_acsl_f5_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
index edd1eec97bb..dce9ccced14 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
@@ -52,9 +52,8 @@ int main(void)
return __retres;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from n;
- */
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n)
{
int __gen_e_acsl_or;
@@ -101,9 +100,8 @@ void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n)
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from n;
- */
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n)
{
int __gen_e_acsl_or_2;
@@ -164,8 +162,8 @@ void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from *n, n;
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/
void __gen_e_acsl_f_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
{
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
index 01c2a3dbbfc..8ca29e4f6d7 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
@@ -340,7 +340,7 @@ int __gen_e_acsl_p2(int x, int y)
}
/*@ assigns \result;
- assigns \result \from x, *y, y; */
+ assigns \result \from x, *((__e_acsl_mpz_struct *)y); */
int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
{
__e_acsl_mpz_t __gen_e_acsl_x_3;
@@ -362,9 +362,8 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
return __retres;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from x, y;
- */
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from x, y; */
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
{
__e_acsl_mpz_t __gen_e_acsl_x_4;
@@ -384,8 +383,8 @@ void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from x, *y, y;
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from x, *((__e_acsl_mpz_struct *)y);
*/
void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
__e_acsl_mpz_struct * y)
@@ -404,8 +403,9 @@ void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
return;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from *x, x, *y, y;
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0]
+ \from *((__e_acsl_mpz_struct *)x), *((__e_acsl_mpz_struct *)y);
*/
void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
__e_acsl_mpz_struct * y)
@@ -457,9 +457,8 @@ mystruct __gen_e_acsl_t1(mystruct m)
return m;
}
-/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
- assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from m;
- */
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from m; */
void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
{
__e_acsl_mpz_t __gen_e_acsl__10;
--
GitLab