diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e7380d160ca17283c96d9b3684fdb3a4a7bc0d2c..936fc6f57fa40ce5d5602545bb8151cce84eb9a0 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -74,6 +74,7 @@ SRC_CODE_GENERATOR:= \
at_with_lscope \
mmodel_translate \
logic_functions \
+ logic_array \
translate \
temporal \
memory_observer \
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index d32d106def951ea26c47935ac6322519fd02208d..65af1bd039b44a2e3ff0fb1a77a3930c47676240 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,8 @@
Plugin E-ACSL <next-release>
############################
+- E-ACSL [2020-08-07] Add support for logical array comparison.
+ (frama-c/e-acsl#99)
- E-ACSL [2020-07-28] Add support of bitwise operators.
(frama-c/e-acsl#33)
-* E-ACSL [2020-07-20] Fix unstable order of generated globals.
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 4266ddd7e32525ee9990447e923a4d91831c2c42..4f0069fb4e7c0d7e473ef5906dc90906f4b35de0 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -128,6 +128,7 @@ in \lstinline|\\at|}
\begin{itemize}
\item \changeinsection{expressions}{support of bitwise operations}
+\item \changeinsection{aggregates}{support of logic arrays}
\end{itemize}
\subsection*{Version Scandium-21}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index df96f85ecbf85ece5c33083aace3c1af24a8f013..686b9c95d324a5d4874fc700060a33647aed493d 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -277,9 +277,18 @@ It is not possible to define logic types introduced by the specification writer
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Structures, Unions and Arrays in logic}
+\label{sec:aggregates}
\nodiff
-\difficults{\notimplemented{Logic arrays} without an explicit length}
+\difficults{Logic arrays without an explicit length}
+
+\begin{notimplementedenv}
+ The \lstinline|\length| function is currently not supported by the \eacsl
+ plug-in.
+
+ The comparison of unions and structures is currently not supported by the
+ \eacsl plug-in.
+\end{notimplementedenv}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 1d8b97641ff92e1b8763d1549cddb241cbe27b5e..ece261d80bc5f5feb371e6a88d13f8b1b3235fc4 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -66,6 +66,8 @@ src/code_generator/label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/literal_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/literal_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/logic_array.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/logic_array.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/logic_functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/logic_functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index c80f627edd31c06ace8f3d5f9b9e03ad07ff3159..59a6acb5cf95cc7762a67ebbb5af99c854579eed 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -295,14 +295,14 @@ let to_exp ~loc kf env pot label =
let e, env = named_predicate_to_exp kf env p in
let e = Cil.constFold false e in
let storing_stmt =
- Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
+ Constructor.mk_assigns ~loc ~result:lval e
in
let block, env =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
- [ Cil.mkStmt ~valid_sid:true (Block block) ], env
+ [ Constructor.mk_block_stmt block ], env
| Misc.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
@@ -311,14 +311,14 @@ let to_exp ~loc kf env pot label =
let e, env = term_to_exp kf env t in
let e = Cil.constFold false e in
let storing_stmt =
- Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
+ Constructor.mk_assigns ~loc ~result:lval e
in
let block, env =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
- [ Cil.mkStmt ~valid_sid:true (Block block) ], env
+ [ Constructor.mk_block_stmt block ], env
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
@@ -334,7 +334,7 @@ let to_exp ~loc kf env pot label =
let storing_loops_block = Cil.mkBlock storing_loops_stmts in
let storing_loops_block, env = Env.pop_and_get
env
- (Cil.mkStmt ~valid_sid:true (Block storing_loops_block))
+ (Constructor.mk_block_stmt storing_loops_block)
~global_clear:false
Env.After
in
@@ -342,7 +342,7 @@ let to_exp ~loc kf env pot label =
let env = put_block_at_label env kf storing_loops_block label in
(* Returning *)
let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
- let e = Cil.new_exp ~loc (Lval lval_at_index) in
+ let e = Constructor.mk_lval ~loc lval_at_index in
e, env
(*
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index eb010f92eb65a2cf9cacdd39a3e5ea53a47dd8d4..4848a1f2e2191770084af933d615f5326926c81c 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.ml
+++ b/src/plugins/e-acsl/src/code_generator/constructor.ml
@@ -26,7 +26,31 @@ open Cil_types
(* Expressions *)
(* ********************************************************************** *)
-let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))
+let extract_uncoerced_lval e =
+ let rec aux e =
+ match e.enode with
+ | Lval _ -> Some e
+ | CastE (_, e) -> aux e
+ | _ -> None
+ in
+ aux e
+
+let mk_lval ~loc lval =
+ Cil.new_exp ~loc (Lval lval)
+
+let mk_deref ~loc lv = mk_lval ~loc (Mem lv, NoOffset)
+
+let mk_subscript ~loc array idx =
+ match extract_uncoerced_lval array with
+ | Some { enode = Lval lval } ->
+ let subscript_lval = Cil.addOffsetLval (Index(idx, NoOffset)) lval in
+ mk_lval ~loc subscript_lval
+ | Some _ | None ->
+ Options.fatal
+ ~current:true
+ "Trying to create a subscript on an array that is not an Lval: %a"
+ Cil_types_debug.pp_exp
+ array
(* ********************************************************************** *)
(* Statements *)
@@ -34,8 +58,16 @@ let mk_deref ~loc lv = Cil.new_exp ~loc (Lval(Mem(lv), NoOffset))
let mk_stmt sk = Cil.mkStmt ~valid_sid:true sk
let mk_instr i = mk_stmt (Instr i)
+let mk_block_stmt blk = mk_stmt (Block blk)
let mk_call ~loc ?result e args = mk_instr (Call(result, e, args, loc))
+let mk_assigns ~loc ~result e = mk_instr (Set(result, e, loc))
+
+let mk_if ~loc ~cond ?(else_blk=Cil.mkBlock []) then_blk =
+ mk_stmt (If (cond, then_blk, else_blk, loc))
+
+let mk_break ~loc = mk_stmt (Break loc)
+
type annotation_kind =
| Assertion
| Precondition
@@ -59,7 +91,7 @@ let mk_block stmt b = match b.bstmts with
| Instr(Skip _) -> stmt
| _ -> assert false)
| [ s ] -> s
- | _ :: _ -> mk_stmt (Block b)
+ | _ :: _ -> mk_block_stmt b
(* ********************************************************************** *)
(* E-ACSL specific code *)
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index 676bfe14af6286cc19179f2d0c8c0aa1a6badc4e..731734839878fda808895f9a71e4fde5858f4d4c 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -25,13 +25,54 @@
open Cil_types
open Cil_datatype
+(* ********************************************************************** *)
+(* Expressions *)
+(* ********************************************************************** *)
+
+val extract_uncoerced_lval: exp -> exp option
+(** Unroll the [CastE] part of the expression until an [Lval] is found, and
+ return it.
+
+ If at some point the expression is neither a [CastE] nor an [Lval], then
+ return [None]. *)
+
+val mk_lval: loc:location -> lval -> exp
+(** Construct an lval expression from an lval. *)
+
val mk_deref: loc:Location.t -> exp -> exp
(** Construct a dereference of an expression. *)
+val mk_subscript: loc:location -> exp -> exp -> exp
+(** [mk_subscript ~loc array idx] Create an expression to access the [idx]'th
+ element of the [array]. *)
+
+(* ********************************************************************** *)
+(* Statements *)
+(* ********************************************************************** *)
+
+val mk_stmt: stmtkind -> stmt
+(** Create a statement from a statement kind. *)
+
val mk_block: stmt -> block -> stmt
(** Create a block statement from a block to replace a given statement.
Requires that (1) the block is not empty, or (2) the statement is a skip. *)
+val mk_block_stmt: block -> stmt
+(** Create a block statement from a block *)
+
+val mk_assigns: loc:location -> result:lval -> exp -> stmt
+(** [mk_assigns ~loc ~result value] create a statement to assign the [value]
+ expression to the [result] lval. *)
+
+val mk_if:
+ loc:location -> cond:exp -> ?else_blk:block -> block -> stmt
+(** [mk_if ~loc ~cond ~then_blk ~else_blk] create an if statement with [cond]
+ as condition and [then_blk] and [else_blk] as respectively "then" block and
+ "else" block. *)
+
+val mk_break: loc:location -> stmt
+(** Create a break statement *)
+
(* ********************************************************************** *)
(* E-ACSL specific code: build calls to its RTL API *)
(* ********************************************************************** *)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index b41dd240b6cdee12cb1cc7c9489fd8b94ee6aaf4..e457ac5c2264548399b60b7ed77206f49cd6973e 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -246,6 +246,21 @@ let new_var_and_mpz_init ~loc ?scope ?name env kf t mk_stmts =
(Gmp_types.Z.t ())
(fun v e -> Gmp.init ~loc e :: mk_stmts v e)
+let rtl_call_to_new_var ~loc ?scope ?name env kf t ty func_name args =
+ let _, exp, env =
+ new_var
+ ~loc
+ ?scope
+ ?name
+ env
+ kf
+ t
+ ty
+ (fun v _ ->
+ [ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) func_name args ])
+ in
+ exp, env
+
module Logic_binding = struct
let add_binding env logic_v vi =
@@ -336,9 +351,9 @@ let add_stmt ?(post=false) ?before env kf stmt =
{ env with env_stack = local_env :: tl }
let extend_stmt_in_place env stmt ~label block =
- let new_stmt = Cil.mkStmt ~valid_sid:true (Block block) in
+ let new_stmt = Constructor.mk_block_stmt block in
let sk = stmt.skind in
- stmt.skind <- Block (Cil.mkBlock [ new_stmt; Cil.mkStmt ~valid_sid:true sk ]);
+ stmt.skind <- Block (Cil.mkBlock [ new_stmt; Constructor.mk_stmt sk ]);
let pre = match label with
| BuiltinLabel(Here | Post) -> true
| BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
@@ -432,7 +447,7 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
add the given [stmt] afterwards. This way, we have the guarantee that
the final block does not contain any local, so may be transient. *)
if split then
- let sblock = Cil.mkStmt ~valid_sid:true (Block b) in
+ let sblock = Constructor.mk_block_stmt b in
Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
else
b
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 31abba5dfff6980ca097d352239a898d790d8f01..847b551cacb7222e4efdf9f1448012bcc655496a 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -59,6 +59,15 @@ val new_var_and_mpz_init:
(** Same as [new_var], but dedicated to mpz_t variables initialized by
{!Mpz.init}. *)
+val rtl_call_to_new_var:
+ loc:location -> ?scope:Varname.scope -> ?name:string ->
+ t -> kernel_function -> term option -> typ ->
+ string -> exp list ->
+ exp * t
+(** [rtl_call_to_new_var env t ty name args] Same as [new_var] but initialize
+ the variable with a call to the RTL function [name] with the given [args].
+*)
+
module Logic_binding: sig
val add: ?ty:typ -> t -> kernel_function -> logic_var -> varinfo * exp * t
(* Add a new C binding to the list of bindings for the logic variable. *)
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index a89178c89937f87f01466e80690473f37d7f64e6..ab1d0ed88db4408e4dd14635e8291350f6666ba8 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -136,7 +136,7 @@ let mk_init_function () =
let loc = Location.unknown in
let e = Cil.new_exp ~loc:loc (Const (CStr s)) in
let str_size = Cil.new_exp loc (SizeOfStr s) in
- Cil.mkStmtOneInstr ~valid_sid:true (Set(Cil.var vi, e, loc))
+ Constructor.mk_assigns ~loc ~result:(Cil.var vi) e
:: Constructor.mk_store_stmt ~str_size vi
:: Constructor.mk_full_init_stmt vi
:: Constructor.mk_mark_readonly vi
@@ -150,7 +150,7 @@ let mk_init_function () =
let b, _env = Env.pop_and_get env stmt ~global_clear:true Env.Before in
b, stmts
in
- let stmts = Cil.mkStmt ~valid_sid:true (Block b) :: stmts in
+ let stmts = Constructor.mk_block_stmt b :: stmts in
(* prevent multiple calls to [__e_acsl_globals_init] *)
let loc = Location.unknown in
let vi_already_run =
@@ -168,14 +168,18 @@ let mk_init_function () =
(Local_init (vi_already_run, init, loc))
in
let already_run =
- Cil.mkStmtOneInstr ~valid_sid:true
- (Set (Cil.var vi_already_run, Cil.one ~loc, loc))
+ Constructor.mk_assigns
+ ~loc
+ ~result:(Cil.var vi_already_run)
+ (Cil.one ~loc)
in
let stmts = already_run :: stmts in
let guard =
- Cil.mkStmt
- ~valid_sid:true
- (If (Cil.evar vi_already_run, Cil.mkBlock [], Cil.mkBlock stmts, loc))
+ Constructor.mk_if
+ ~loc
+ ~cond:(Cil.evar vi_already_run)
+ (Cil.mkBlock [])
+ ~else_blk:(Cil.mkBlock stmts)
in
let return = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
let stmts = [ init_stmt; guard; return ] in
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index b35afd1163cd65d1ab4ff68e9c93e18a94fa0323..8c28ac5e32e0267754723bd1a0042f492fb6cb17 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -92,7 +92,7 @@ let generic_affect ~loc fname lv ev e =
let suf, args = get_set_suffix_and_arg ty e in
Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
end else
- Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))
+ Constructor.mk_assigns ~loc:e.eloc ~result:lv e
let init_set ~loc lv ev e =
let fname =
@@ -121,7 +121,7 @@ let init_set ~loc lv ev e =
Cil.zero ~loc;
Cil.mkAddrOf ~loc elv ]
in
- Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ init ~loc ev; call ]))
+ Constructor.mk_block_stmt (Cil.mkBlock [ init ~loc ev; call ])
| _ ->
Error.not_yet "unsigned long long expression requiring GMP")
| Longlong ILongLong ->
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
new file mode 100644
index 0000000000000000000000000000000000000000..af522479dc6c22f7926c9edfee20c28821c1ce1a
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -0,0 +1,294 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+(* Forward references *)
+let translate_rte_ref:
+ (?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp ->
+ Env.t) ref =
+ let func ?filter _kf _env _e =
+ let _ = filter in
+ Extlib.mk_labeled_fun "translate_rte_ref"
+ in
+ ref func
+
+(** @return the content of the array type if [ty] is an array, or None
+ otherwise. *)
+let rec get_array_typ_opt ty =
+ if Gmp_types.is_t ty then
+ (* GMP pointer types are declared as arrays of one element. They are treated
+ as a special case here to ensure that they are not considered as arrays.
+ *)
+ None
+ else
+ match ty with
+ | TNamed (r, _) -> get_array_typ_opt r.ttype
+ | TArray (t, eo, bsot, a) -> Some (t, eo, bsot, a)
+ | _ -> None
+
+let is_array ty =
+ match get_array_typ_opt ty with
+ | Some _ -> true
+ | None -> false
+
+(** Retrieve the length of the [array] expression in a new variable [name] and
+ return it as an expression.
+ If the length is present in the type then the function directly assigns the
+ length to the variable, otherwise it is computed with the formula
+ [length = (\block_length(array) - \offset(array)) / sizeof(elem_typ)]. *)
+let length_exp ~loc kf env ~name array =
+ let elem_typ, array_len =
+ match get_array_typ_opt (Cil.typeOf array) with
+ | None -> Options.fatal "Trying to retrieve the length of a non-array"
+ | Some (t, len, _, _) -> t, len
+ in
+ try
+ let len = Cil.lenOfArray64 array_len in
+ (Cil.kinteger64 ~loc len), env
+ with Cil.LenOfArray ->
+ (* check RTE on the array before accessing its block length and offset *)
+ let env = !translate_rte_ref kf env array in
+ (* helper function *)
+ let rtl env name =
+ Env.rtl_call_to_new_var
+ ~loc
+ env
+ kf
+ None
+ Cil.theMachine.typeOfSizeOf
+ name
+ [ array ]
+ in
+ (* block_length(array) *)
+ let block_length_exp, env = rtl env "block_length" in
+ (* offset(array) *)
+ let offset_exp, env = rtl env "offset" in
+ (* sizeof(elem_typ) *)
+ let sizeof_exp = Cil.new_exp ~loc (SizeOf elem_typ) in
+ (* Create var and compute length *)
+ let _, len_exp, env =
+ Env.new_var
+ ~loc
+ env
+ kf
+ None
+ ~name
+ Cil.theMachine.typeOfSizeOf
+ (fun v _ -> [
+ Constructor.mk_assigns
+ ~loc
+ ~result:(Cil.var v)
+ (Cil.mkBinOp
+ ~loc
+ Div
+ (Cil.mkBinOp ~loc MinusA block_length_exp offset_exp)
+ sizeof_exp)
+ ])
+ in
+ len_exp, env
+
+let comparison_to_exp ~loc kf env ~name bop array1 array2 =
+ (match bop with
+ | Eq | Ne -> () (* Ok *)
+ | _ ->
+ Options.fatal ~current:true "Something else than comparison of equality\
+ between two arrays.");
+
+ (* The generated code can be the same for [Ne] and [Eq] if we just adjust the
+ values for the result.
+ [res_value()] returns the initial value for
+ the result and [res_flip_value()] returns the flipped value of the result.
+ If the arrays have been coerced in ACSL to a different array size, then we
+ add a check to see if the coerced size is lesser or equal to then actual
+ length of the array.
+ The generated code returned by this function is equivalent to:
+ int result = res_value();
+ size_t len1 = length(array1);
+ size_t len2 = length(array2);
+ if (len1 == len2) {
+ // Here we add check that the coerced length doesn't exceed the
+ // actual length of the arrays.
+ // Then we compare the content of the arrays, using the coerced
+ // length.
+ for (int i = 0 ; i < len1 ; ++i) {
+ if (array1[i] != array2[i]) {
+ result = res_value(flip);
+ break;
+ }
+ }
+ } else {
+ result = res_value(flip);
+ }
+ result
+ *)
+ let res_value ?(flip=false) () =
+ match flip, bop with
+ | false, Eq | true, Ne -> Cil.one ~loc
+ | true, Eq | false, Ne -> Cil.zero ~loc
+ | _ -> assert false
+ in
+
+ (* Helper function: call [Env.pop_and_get] with [global_clear] and [where]
+ pre-set *)
+ let pop_and_get_env env stmt =
+ Env.pop_and_get
+ env
+ stmt
+ ~global_clear:false
+ Env.Middle
+ in
+
+ (* Create var that will hold the result of the comparison between the
+ two arrays *)
+ let comparison_vi, comparison_exp, env =
+ Env.new_var
+ ~loc
+ env
+ kf
+ None
+ ~name
+ Cil.intType
+ (fun v _ -> [ Constructor.mk_assigns ~loc ~result:(Cil.var v) (res_value ()) ])
+ in
+
+ (* Retrieve the length of the arrays *)
+ let len1_exp, env = length_exp ~loc kf env ~name:"length1" array1 in
+ let len2_exp, env = length_exp ~loc kf env ~name:"length2" array2 in
+
+ (* Push a new env to declare the variable that will hold the iterator of the
+ loop *)
+ let env = Env.push env in
+ let iter, iter_e, env =
+ Env.new_var
+ ~loc
+ env
+ kf
+ None
+ ~name:"iter"
+ Cil.theMachine.typeOfSizeOf
+ (fun _ _ -> [])
+ in
+
+ (* Push a new env to do the innermost comparison between two elements of the
+ arrays. This env will enable us to also check RTEs *)
+ let env = Env.push env in
+ (* Create the access to the arrays *)
+ let array1_iter_e = Constructor.mk_subscript ~loc array1 iter_e in
+ let array2_iter_e = Constructor.mk_subscript ~loc array2 iter_e in
+ (* Check RTE on the arrays, filtering out bounding checks since the accesses
+ are built already in bounds *)
+ let filter a =
+ let index_bound =
+ Alarms.get_name (Index_out_of_bound (iter_e, Some len1_exp))
+ in
+ match a.annot_content with
+ | AAssert (_, _, { pred_name = hd :: _ })
+ when Datatype.String.equal hd index_bound -> false
+ | _ -> true
+ in
+ let env = !translate_rte_ref ~filter kf env array1_iter_e in
+ let env = !translate_rte_ref ~filter kf env array2_iter_e in
+ (* Create the condition *)
+ let cond = Cil.mkBinOp ~loc Ne array1_iter_e array2_iter_e in
+ (* Create the statement representing the body of the for loop *)
+ let body =
+ Constructor.mk_if
+ ~loc
+ ~cond
+ (Cil.mkBlock [
+ Constructor.mk_assigns ~loc ~result:(Cil.var comparison_vi) (res_value ~flip:true ());
+ Constructor.mk_break ~loc
+ ])
+ in
+ (* Pop the env to build the body of the for loop *)
+ let body_blk, env = pop_and_get_env env body in
+
+ (* Create the statement representing the full for loop *)
+ let for_loop =
+ (Constructor.mk_block_stmt
+ (Cil.mkBlock
+ (Cil.mkForIncr
+ ~iter
+ ~first:(Cil.zero ~loc)
+ ~stopat:len1_exp
+ ~incr:(Cil.one ~loc)
+ ~body:[ Constructor.mk_block_stmt body_blk ]
+ )
+ )
+ )
+ in
+
+ (* Create the list of statements that will be in the `then` block of the
+ top-level if *)
+ let then_stmts = [ for_loop ] in
+
+ (* Add the check for the length before the for loop *)
+ let prepend_coercion_check ~name env stmts array len =
+ let array_orig = Option.get (Constructor.extract_uncoerced_lval array) in
+ if array_orig == array then
+ stmts, env
+ else
+ let len_orig, env =
+ length_exp ~loc kf env ~name:(name ^ "_orig") array_orig
+ in
+ let e = Cil.mkBinOp ~loc Le len len_orig in
+ let p =
+ Logic_const.prel
+ ~loc
+ (Rle, Logic_utils.expr_to_term len, Logic_utils.expr_to_term len_orig)
+ in
+ let p = { p with pred_name = "array_coercion" :: p.pred_name } in
+ let stmt =
+ Constructor.mk_runtime_check Constructor.RTE kf e p
+ in
+ stmt :: stmts, env
+ in
+ let then_stmts, env =
+ prepend_coercion_check ~name:"length2" env then_stmts array2 len2_exp
+ in
+ let then_stmts, env =
+ prepend_coercion_check ~name:"length1" env then_stmts array1 len1_exp
+ in
+
+ (* Pop the env to build the full then block *)
+ let then_blk, env =
+ pop_and_get_env env (Constructor.mk_block_stmt (Cil.mkBlock then_stmts))
+ in
+
+ (* Create the statement representing the whole generated code *)
+ let stmt =
+ Constructor.mk_if
+ ~loc
+ ~cond:(Cil.mkBinOp ~loc Eq len1_exp len2_exp)
+ then_blk
+ ~else_blk:(Cil.mkBlock
+ [ Constructor.mk_assigns
+ ~loc
+ ~result:(Cil.var comparison_vi)
+ (res_value ~flip:true ()) ])
+ in
+ (* Build the statement in the current env *)
+ let env = Env.add_stmt env kf stmt in
+
+ (* Return the result expression with the result of the comparison *)
+ comparison_exp, env
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.mli b/src/plugins/e-acsl/src/code_generator/logic_array.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e6ca3976f85d4fba9837cafe40bd9f674d85f446
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.mli
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* 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_array: typ -> bool
+(** @return true iff the type is an array *)
+
+val comparison_to_exp: loc:location -> kernel_function -> Env.t ->
+ name:string -> binop -> exp -> exp -> exp * Env.t
+(** [comparison_to_exp ~loc kf env ~name bop e1 e2] generate the C code
+ equivalent to [e1 bop e2].
+ Requires that [bop] is either [Ne] or [Eq] and that [e1] and [e2] are
+ arrays. *)
+
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val translate_rte_ref:
+ (?filter:(code_annotation -> bool) -> kernel_function -> Env.t -> exp ->
+ Env.t) ref
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 c51d4190fe76bfd16f63f4daed9ac65f219607ff..d5bf1c4da99b052ef55ba976adb9eba5c4929ff7 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -98,7 +98,7 @@ let term_to_block ~loc kf env ret_ty ret_vi t =
function (by reference). *)
let set =
let lv_star_ret = Cil.mkMem ~addr:(Cil.evar ~loc ret_vi) ~off:NoOffset in
- let star_ret = Cil.new_exp ~loc (Lval lv_star_ret) in
+ let star_ret = Constructor.mk_lval ~loc lv_star_ret in
Gmp.init_set ~loc lv_star_ret star_ret e
in
let return_void = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index d76bac69fc4f89b825141d83ccc88461fb9f0289..bca60ec4f2cd8197f440f38a15241dd03c70761e 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -212,7 +212,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Env.Middle
in
(* generate the guard [x bop t2] *)
- let block_to_stmt b = mkStmt ~valid_sid:true (Block b) in
+ let block_to_stmt b = Constructor.mk_block_stmt b in
let tlv = Logic_const.tvar ~loc logic_x in
let guard =
(* must copy [t2] to force being typed again *)
@@ -221,16 +221,14 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
in
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
let guard_exp, env = term_to_exp kf (Env.push env) guard in
- let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
+ let break_stmt = Constructor.mk_break ~loc:guard_exp.eloc in
let guard_blk, env = Env.pop_and_get
env
- (mkStmt
- ~valid_sid:true
- (If(
- guard_exp,
- mkBlock [ mkEmptyStmt ~loc () ],
- mkBlock [ break_stmt ],
- guard_exp.eloc)))
+ (Constructor.mk_if
+ ~loc:guard_exp.eloc
+ ~cond:guard_exp
+ (mkBlock [ mkEmptyStmt ~loc () ])
+ ~else_blk:(mkBlock [ break_stmt ]))
~global_clear:false
Env.Middle
in
@@ -256,7 +254,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Constructor.mk_runtime_check Constructor.RTE kf e p, env
in
let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
- let guard_for_small_type = Cil.mkStmt ~valid_sid:true (Block b) in
+ let guard_for_small_type = Constructor.mk_block_stmt b in
guard_for_small_type :: guard :: body @ [ next ], env
in
let start = block_to_stmt init_blk in
diff --git a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
index 41a1245eed32cade67ec277a16e931e21de66282..f5cae16eb0bdb82fc8330038a5c218c6c79f50f7 100644
--- a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -116,19 +116,15 @@ let call ~loc kf name ctx env t =
assert (name = "base_addr" || name = "block_length"
|| name = "offset" || name ="freeable");
let e, env = !term_to_exp_ref kf (Env.rte env true) t in
- let _, res, env =
- Env.new_var
- ~loc
- ~name
- env
- kf
- None
- ctx
- (fun v _ ->
- let name = Functions.RTL.mk_api_name name in
- [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) name [ e ] ])
- in
- res, env
+ Env.rtl_call_to_new_var
+ ~loc
+ ~name
+ env
+ kf
+ None
+ ctx
+ name
+ [ e ]
(*****************************************************************************)
(************************* Calls with Range Elimination **********************)
@@ -234,24 +230,20 @@ let call_memory_block ~loc kf name ctx env ptr r p =
| _ -> assert false
in
(* generating env *)
- let _, e, env =
- Env.new_var
- ~loc
- ~name
- env
- kf
- None
- ctx
- (fun v _ ->
- let fname = Functions.RTL.mk_api_name name in
- let args = match name with
- | "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
- | "initialized" -> [ ptr; size ]
- | _ -> Error.not_yet ("builtin " ^ name)
- in
- [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname args ])
+ let args = match name with
+ | "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
+ | "initialized" -> [ ptr; size ]
+ | _ -> Error.not_yet ("builtin " ^ name)
in
- e, env
+ Env.rtl_call_to_new_var
+ ~loc
+ ~name
+ env
+ kf
+ None
+ ctx
+ name
+ args
(* [call_with_ranges] handles ranges in [t] when calling builtin [name].
It only supports the following cases for the time being:
@@ -342,23 +334,17 @@ let call_with_size ~loc kf name ctx env t p =
let call_for_unsupported_constructs ~loc kf name ctx env t =
let term_to_exp = !term_to_exp_ref in
let e, env = term_to_exp kf (Env.rte env true) t in
- let _, res, env =
- Env.new_var
- ~loc
- ~name
- env
- kf
- None
- ctx
- (fun v _ ->
- let ty = Misc.cty t.term_type in
- let sizeof = Misc.mk_ptr_sizeof ty loc in
- [ Constructor.mk_rtl_call ~loc
- ~result:(Cil.var v)
- name
- [ e; sizeof ] ])
- in
- res, env
+ let ty = Misc.cty t.term_type in
+ let sizeof = Misc.mk_ptr_sizeof ty loc in
+ Env.rtl_call_to_new_var
+ ~loc
+ ~name
+ env
+ kf
+ None
+ ctx
+ name
+ [ e; sizeof ]
in
call_with_ranges
~loc
@@ -382,21 +368,18 @@ let call_valid ~loc kf name ctx env t p =
| Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
| _ -> assert false
in
- let _, res, env =
- Env.new_var
- ~loc
- ~name
- env
- kf
- None
- ctx
- (fun v _ ->
- let ty = Misc.cty t.term_type in
- let sizeof = Misc.mk_ptr_sizeof ty loc in
- let args = [ e; sizeof; base; base_addr ] in
- [ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) name args ])
- in
- res, env
+ let ty = Misc.cty t.term_type in
+ let sizeof = Misc.mk_ptr_sizeof ty loc in
+ let args = [ e; sizeof; base; base_addr ] in
+ Env.rtl_call_to_new_var
+ ~loc
+ ~name
+ env
+ kf
+ None
+ ctx
+ name
+ args
in
call_with_ranges
~loc
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 7298f8c82bc652078a24a71b2a86d24010bf5b40..b6114f25cd132102a8ccd4e606ca1ad303c2047a 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -174,7 +174,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
intType
(fun v _ ->
let lv = var v in
- [ mkStmtOneInstr ~valid_sid:true (Set(lv, init_val, loc)) ])
+ [ Constructor.mk_assigns ~loc ~result:lv init_val ])
in
let end_loop_ref = ref dummyStmt in
(* innermost block *)
@@ -183,29 +183,28 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
to evaluation of the goal *)
let named_predicate_to_exp = !predicate_to_exp_ref in
let test, env = named_predicate_to_exp kf (Env.push env) goal in
- let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
- let else_block =
+ let then_blk = mkBlock [ mkEmptyStmt ~loc () ] in
+ let else_blk =
(* use a 'goto', not a simple 'break' in order to handle 'forall' with
multiple binders (leading to imbricated loops) *)
mkBlock
- [ mkStmtOneInstr ~valid_sid:true (Set(var var_res, found_val, loc));
+ [ Constructor.mk_assigns ~loc ~result:(var var_res) found_val;
mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
in
let blk, env = Env.pop_and_get
env
- (mkStmt ~valid_sid:true
- (If(mk_guard test, then_block, else_block, loc)))
+ (Constructor.mk_if ~loc ~cond:(mk_guard test) then_blk ~else_blk)
~global_clear:false
Env.After
in
let blk = Cil.flatten_transient_sub_blocks blk in
- [ mkStmt ~valid_sid:true (Block blk) ], env
+ [ Constructor.mk_block_stmt blk ], env
in
let stmts, env =
Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
in
let env =
- Env.add_stmt env kf (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
+ Env.add_stmt env kf (Constructor.mk_block_stmt (mkBlock stmts))
in
(* where to jump to go out of the loop *)
let end_loop = mkEmptyStmt ~loc () in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 4c0ae922b43921e75e447b0fd6e5660a77f44a26..3a0da53951b3b4f569e7f55bc2ea3d4849e1fcc4 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -24,11 +24,10 @@ open Cil_types
(* No init_set for GMPQ: init then set separately *)
let init_set ~loc lval vi_e e =
- Cil.mkStmt
- ~valid_sid:true
- (Block (Cil.mkBlock
- [ Gmp.init ~loc vi_e ;
- Gmp.affect ~loc lval vi_e e ]))
+ Constructor.mk_block_stmt
+ (Cil.mkBlock
+ [ Gmp.init ~loc vi_e ;
+ Gmp.affect ~loc lval vi_e e ])
let create ~loc ?name e env kf t_opt =
let ty = Cil.typeOf e in
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index 8686559615068533ec432a081e927c87e4ec9ea7..a2694969cc618f039f6314f651099618e8985184 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -262,7 +262,7 @@ end = struct
(* Update local environment with a statement tracking temporal metadata
associated with assignment [ret] = [func(args)]. *)
let call_with_ret ?(alloc=false) current_stmt loc ret env kf =
- let rhs = Cil.new_exp ~loc (Lval ret) in
+ let rhs = Constructor.mk_lval ~loc ret in
let vals = assign ret rhs loc in
(* Track referent numbers of assignments via function calls.
Library functions (i.e., with no source code available) that return
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 4e310e1b4adfbc577e2aaa98178f4be15ed50693..b9dfc2390c42fb5519843333f0fb83f8b0bc2c0d 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -221,15 +221,15 @@ let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
Gmp.init_set
in
let affect e = init_set ~loc lv ev e in
- let then_block, _ =
+ let then_blk, _ =
let s = affect e2 in
Env.pop_and_get env2 s ~global_clear:false Env.Middle
in
- let else_block, _ =
+ let else_blk, _ =
let s = affect e3 in
Env.pop_and_get env3 s ~global_clear:false Env.Middle
in
- [ Cil.mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
+ [ Constructor.mk_if ~loc ~cond:e1 then_blk ~else_blk ])
in
e, env
@@ -276,7 +276,7 @@ and context_insensitive_term_to_exp kf env t =
c, env, strnum, ""
| TLval lv ->
let lv, env, name = tlval_to_lval kf env lv in
- Cil.new_exp ~loc (Lval lv), env, C_number, name
+ Constructor.mk_lval ~loc lv, env, C_number, name
| TSizeOf ty -> Cil.sizeOf ~loc ty, env, C_number, "sizeof"
| TSizeOfE t ->
let e, env = term_to_exp kf env t in
@@ -762,29 +762,46 @@ and comparison_to_exp
| Some e1 ->
e1, env
in
+ let ty1 = Cil.typeOf e1 in
let e2, env = term_to_exp kf env t2 in
- match ity with
- | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
- Cil.mkBinOp ~loc bop e1 e2, env
- | Typing.Gmpz ->
- let _, e, env = Env.new_var
- ~loc
- env
- kf
- t_opt
- ~name
- Cil.intType
- (fun v _ ->
- [ Constructor.mk_lib_call ~loc
- ~result:(Cil.var v)
- "__gmpz_cmp"
- [ e1; e2 ] ])
- in
- Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
- | Typing.Rational ->
- Rational.cmp ~loc bop e1 e2 env kf t_opt
- | Typing.Real ->
- Error.not_yet "comparison involving real numbers"
+ let ty2 = Cil.typeOf e2 in
+ match Logic_array.is_array ty1, Logic_array.is_array ty2 with
+ | true, true ->
+ Logic_array.comparison_to_exp
+ ~loc
+ kf
+ env
+ ~name
+ bop
+ e1
+ e2
+ | false, false -> (
+ match ity with
+ | Typing.C_integer _ | Typing.C_float _ | Typing.Nan ->
+ Cil.mkBinOp ~loc bop e1 e2, env
+ | Typing.Gmpz ->
+ let _, e, env = Env.new_var
+ ~loc
+ env
+ kf
+ t_opt
+ ~name
+ Cil.intType
+ (fun v _ ->
+ [ Constructor.mk_lib_call ~loc
+ ~result:(Cil.var v)
+ "__gmpz_cmp"
+ [ e1; e2 ] ])
+ in
+ Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+ | Typing.Rational ->
+ Rational.cmp ~loc bop e1 e2 env kf t_opt
+ | Typing.Real ->
+ Error.not_yet "comparison involving real numbers"
+ )
+ | _, _ ->
+ Options.fatal ~current:true "Comparison involving an array with something \
+ else."
and at_to_exp_no_lscope env kf t_opt label e =
let stmt = E_acsl_label.get_stmt kf label in
@@ -838,7 +855,7 @@ and env_of_li li kf env loc =
let e, env = term_to_exp kf env t in
let stmt = match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
- Cil.mkStmtOneInstr ~valid_sid:true (Set (Cil.var vi, e, loc))
+ Constructor.mk_assigns ~loc ~result:(Cil.var vi) e
| Typing.Gmpz ->
Gmp.init_set ~loc (Cil.var vi) vi_e e
| Typing.Rational ->
@@ -1040,9 +1057,14 @@ and translate_rte_annots:
is_visiting_valid := old_valid;
Env.set_annotation_kind env old_kind
-and translate_rte kf env e =
+and translate_rte ?filter kf env e =
let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
let l = Rte.exp kf stmt e in
+ let l =
+ match filter with
+ | Some f -> List.filter f l
+ | None -> l
+ in
translate_rte_annots Printer.pp_exp e kf env l
and translate_named_predicate kf env p =
@@ -1075,7 +1097,8 @@ let () =
Mmodel_translate.term_to_exp_ref := term_to_exp;
Mmodel_translate.predicate_to_exp_ref := named_predicate_to_exp;
Logic_functions.term_to_exp_ref := term_to_exp;
- Logic_functions.named_predicate_to_exp_ref := named_predicate_to_exp
+ Logic_functions.named_predicate_to_exp_ref := named_predicate_to_exp;
+ Logic_array.translate_rte_ref := translate_rte
(* This function is used by Guillaume.
However, it is correct to use it only in specific contexts. *)
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml
index 6b89bba519386a97b974f290eca81a5e3ba0933b..2022682fa13c33f0c73268591b97b0181baaa564 100644
--- a/src/plugins/e-acsl/src/libraries/gmp_types.ml
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.ml
@@ -123,6 +123,9 @@ let init () =
end in
try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()
+let is_t ty =
+ Z.is_t ty || Q.is_t ty
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.mli b/src/plugins/e-acsl/src/libraries/gmp_types.mli
index 3c9db48c536ba039e7e9bba155e2824170828161..fc818fbe4b66450710ded247878f46daa944102a 100644
--- a/src/plugins/e-acsl/src/libraries/gmp_types.mli
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.mli
@@ -27,6 +27,9 @@ open Cil_types
val init: unit -> unit
(** Must be called before any use of GMP *)
+val is_t: typ -> bool
+(** @return true iff the given type is equivalent to one of the GMP type. *)
+
(**************************************************************************)
(******************************** Types ***********************************)
(**************************************************************************)
diff --git a/src/plugins/e-acsl/tests/arith/array.i b/src/plugins/e-acsl/tests/arith/array.i
index 6211cf0950134f6a9c05becab68884473392be21..192094bfbdee5042d17c0e6225eb70a1cc87cbf1 100644
--- a/src/plugins/e-acsl/tests/arith/array.i
+++ b/src/plugins/e-acsl/tests/arith/array.i
@@ -5,6 +5,102 @@
int T1[3],T2[4];
+void arrays() {
+ // Pure logic arrays
+ // (Unsupported at the moment by the kernel)
+ // /*@ assert {[0] = 1, [1] = 2, [2] = 3} == {[0] = 1, [1] = 2, [2] = 3}; */
+ // /*@ assert {[0] = 1, [1] = 2, [2] = 3} != {[0] = 4, [1] = 5, [2] = 6}; */
+ // /*@ assert {[0] = 1, [1] = 2, [2] = 3} !=
+ // {[0] = 1, [1] = 2, [2] = 3, [3] = 4, [4] = 5, [5] = 6}; */
+
+ // C arrays
+ int a[] = {1, 2, 3};
+ int b[] = {4, 5, 6};
+ int c[] = {1, 2, 3};
+ int d[] = {1, 2, 3, 4, 5, 6};
+ /*@ assert a != b; */
+ /*@ assert a == c; */
+ /*@ assert a != d; */
+
+ // Pointers to arrays
+ int * e = a;
+ int * f = b;
+ int * g = c;
+ int * h = a;
+ /*@ assert e != f; */
+ /*@ assert e != g; */
+ /*@ assert e == h; */
+
+ // Comparison between C arrays, logic arrays and pointer to arrays
+ // /*@ assert a == {[0] = 1, [1] = 2, [2] = 3}; */ UNSUPPORTED by the kernel
+ /*@ assert e == (int *) a; */
+ /*@ assert e != (int *) c; */
+ // /*@ assert (int[3])e == {[0] = 1, [1] = 2, [2] = 3}; */ UNSUPPORTED by the kernel
+ // /*@ assert (int[])e == {[0] = 1, [1] = 2, [2] = 3}; */ UNSUPPORTED by the kernel
+ /*@ assert a == (int[3])g; */
+ /*@ assert a == (int[])g; */
+ /*@ assert a != (int[3])f; */
+ /*@ assert a != (int[])f; */
+
+ // Comparison between sub-arrays
+ int i[] = {1, 2, 3, 4, 5, 6};
+ int j[] = {4, 5, 6, 1, 2, 3};
+ int k[] = {4, 5, 6, 4, 5, 6};
+ /*@ assert i != j; */
+ /*@ assert i != k; */
+ /*@ assert j != k; */
+ int * l = &i[3];
+ int * m = &j[3];
+ int * n = &k[3];
+ /*@ assert (int[3])l != (int[3])m; */
+ /*@ assert (int[3])l == (int[3])n; */
+
+ // Array truncation
+ /*@ assert (int[3])i != (int[3])k; */
+ /*@ assert (int[3])j == (int[3])k; */
+ /*@ assert (int[2])l != (int[2])m; */
+ /*@ assert (int[2])l == (int[2])n; */
+
+ // Errors if trying an array extension
+ /*ERROR assert (int[10])i != (int[10])k; */
+ /*ERROR assert (int[10])j != (int[10])k; */
+ /*ERROR assert (int[6])l != (int[6])m; */
+ /*ERROR assert (int[6])l == (int[6])n; */
+
+
+ // Errors while comparing a pointer to array with an array (logic or C)
+ /*ERROR: assert e == a; */
+ /*ERROR: assert e == {[0] = 1, [1] = 2, [2] = 3}; */
+
+ // Error while casting a logic array to a pointer to array
+ /*ERROR: assert e != (int*){[0] = 1, [1] = 2, [2] = 3}; */
+}
+
+void vlas(int n) {
+ // FIXME: There is currently an error with the support of VLA in E-ACSL
+ // https://git.frama-c.com/frama-c/e-acsl/-/issues/119
+
+ // // Declare VLAs
+ // int a[n+1];
+ // int b[n+1];
+ // int c[n+1];
+
+ // // Initialize arrays
+ // for (int i = 0; i < (n+1) ; ++i) {
+ // a[i] = i;
+ // b[i] = n + 1 - i;
+ // c[i] = i;
+ // }
+
+ // // // Compare VLAs
+ // // // The naive comparison compare pointers
+ // // /*@ assert a != b; */
+ // // /*@ assert a == c; */
+ // // // We need to cast to int[] to have an array comparison
+ // // /*@ assert (int[])a != (int[])b; */
+ // // /*@ assert (int[])a == (int[])c; */
+}
+
int main(void) {
for(int i = 0; i < 3; i++) T1[i] = i;
@@ -13,5 +109,8 @@ int main(void) {
/*@ assert T1[0] == T2[0]; */
/*@ assert T1[1] != T2[1]; */
+ arrays();
+ vlas(3);
+
return 0;
-}
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle
index efd026311297e55d8fefb674326118e6ece88624..c1008f0532893f6c5af5afe4bb908dfae70f97b0 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle
@@ -1,2 +1,18 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/arith/array.i:21: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:22: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:23: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:40: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:41: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:42: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:43: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:49: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:50: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:51: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:55: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:56: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:59: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:60: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:61: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:62: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
index 334e1f1891acd45ad6414ea94e962a4e8325adf2..b65d0e8fe7686a76b411ddaa1c26c7d331c15ce1 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
@@ -3,9 +3,535 @@
#include "stdlib.h"
int T1[3];
int T2[4];
+void arrays(void)
+{
+ int a[3] = {1, 2, 3};
+ int b[3] = {4, 5, 6};
+ __e_acsl_store_block((void *)(b),(size_t)12);
+ __e_acsl_full_init((void *)(& b));
+ int c[3] = {1, 2, 3};
+ __e_acsl_store_block((void *)(c),(size_t)12);
+ __e_acsl_full_init((void *)(& c));
+ int d[6] = {1, 2, 3, 4, 5, 6};
+ {
+ int __gen_e_acsl_ne;
+ __gen_e_acsl_ne = 0;
+ if (1) {
+ unsigned long __gen_e_acsl_iter;
+ __gen_e_acsl_iter = 0;
+ while (__gen_e_acsl_iter < 3) {
+ if (a[__gen_e_acsl_iter] != b[__gen_e_acsl_iter]) {
+ __gen_e_acsl_ne = 1;
+ break;
+ }
+ __gen_e_acsl_iter ++;
+ }
+ }
+ else __gen_e_acsl_ne = 1;
+ __e_acsl_assert(__gen_e_acsl_ne,"Assertion","arrays","a != b",
+ "tests/arith/array.i",21);
+ }
+ /*@ assert a ≢ b; */ ;
+ {
+ int __gen_e_acsl_eq;
+ __gen_e_acsl_eq = 1;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_2;
+ __gen_e_acsl_iter_2 = 0;
+ while (__gen_e_acsl_iter_2 < 3) {
+ if (a[__gen_e_acsl_iter_2] != c[__gen_e_acsl_iter_2]) {
+ __gen_e_acsl_eq = 0;
+ break;
+ }
+ __gen_e_acsl_iter_2 ++;
+ }
+ }
+ else __gen_e_acsl_eq = 0;
+ __e_acsl_assert(__gen_e_acsl_eq,"Assertion","arrays","a == c",
+ "tests/arith/array.i",22);
+ }
+ /*@ assert a ≡ c; */ ;
+ {
+ int __gen_e_acsl_ne_2;
+ __gen_e_acsl_ne_2 = 0;
+ if (0) {
+ unsigned long __gen_e_acsl_iter_3;
+ __gen_e_acsl_iter_3 = 0;
+ while (__gen_e_acsl_iter_3 < 3) {
+ if (a[__gen_e_acsl_iter_3] != d[__gen_e_acsl_iter_3]) {
+ __gen_e_acsl_ne_2 = 1;
+ break;
+ }
+ __gen_e_acsl_iter_3 ++;
+ }
+ }
+ else __gen_e_acsl_ne_2 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_2,"Assertion","arrays","a != d",
+ "tests/arith/array.i",23);
+ }
+ /*@ assert a ≢ d; */ ;
+ int *e = a;
+ int *f = b;
+ __e_acsl_store_block((void *)(& f),(size_t)8);
+ __e_acsl_full_init((void *)(& f));
+ int *g = c;
+ __e_acsl_store_block((void *)(& g),(size_t)8);
+ __e_acsl_full_init((void *)(& g));
+ int *h = a;
+ __e_acsl_assert(e != f,"Assertion","arrays","e != f","tests/arith/array.i",
+ 30);
+ /*@ assert e ≢ f; */ ;
+ __e_acsl_assert(e != g,"Assertion","arrays","e != g","tests/arith/array.i",
+ 31);
+ /*@ assert e ≢ g; */ ;
+ __e_acsl_assert(e == h,"Assertion","arrays","e == h","tests/arith/array.i",
+ 32);
+ /*@ assert e ≡ h; */ ;
+ __e_acsl_assert(e == a,"Assertion","arrays","e == (int *)a",
+ "tests/arith/array.i",36);
+ /*@ assert e ≡ (int *)a; */ ;
+ __e_acsl_assert(e != c,"Assertion","arrays","e != (int *)c",
+ "tests/arith/array.i",37);
+ /*@ assert e ≢ (int *)c; */ ;
+ {
+ int __gen_e_acsl_eq_2;
+ __gen_e_acsl_eq_2 = 1;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_4;
+ __gen_e_acsl_iter_4 = 0;
+ while (__gen_e_acsl_iter_4 < 3) {
+ {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& (*((int (*)[3])g))[__gen_e_acsl_iter_4]),
+ sizeof(int),
+ (void *)(& (*((int (*)[3])g))[__gen_e_acsl_iter_4]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[3])g))[__gen_e_acsl_iter_4])",
+ "tests/arith/array.i",40);
+ if (a[__gen_e_acsl_iter_4] != (*((int (*)[3])g))[__gen_e_acsl_iter_4]) {
+ __gen_e_acsl_eq_2 = 0;
+ break;
+ }
+ }
+ __gen_e_acsl_iter_4 ++;
+ }
+ }
+ else __gen_e_acsl_eq_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_eq_2,"Assertion","arrays",
+ "a == *((int (*)[3])g)","tests/arith/array.i",40);
+ }
+ /*@ assert a ≡ *((int (*)[3])g); */ ;
+ {
+ int __gen_e_acsl_eq_3;
+ int __gen_e_acsl_valid_read_2;
+ unsigned long __gen_e_acsl_;
+ unsigned long __gen_e_acsl__2;
+ unsigned long __gen_e_acsl_length2;
+ __gen_e_acsl_eq_3 = 1;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(*((int (*)[])g)),
+ sizeof(int),
+ (void *)(*((int (*)[])g)),
+ (void *)(*((int (*)[])g)));
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","arrays",
+ "mem_access: \\valid_read((int *)*((int (*)[])g))",
+ "tests/arith/array.i",41);
+ __gen_e_acsl_ = __e_acsl_block_length((void *)(*((int (*)[])g)));
+ __gen_e_acsl__2 = __e_acsl_offset((void *)(*((int (*)[])g)));
+ __gen_e_acsl_length2 = (__gen_e_acsl_ - __gen_e_acsl__2) / sizeof(int);
+ if (3UL == __gen_e_acsl_length2) {
+ unsigned long __gen_e_acsl_iter_5;
+ __gen_e_acsl_iter_5 = 0;
+ while (__gen_e_acsl_iter_5 < 3) {
+ {
+ int __gen_e_acsl_valid_read_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*((int (*)[])g))[__gen_e_acsl_iter_5]),
+ sizeof(int),
+ (void *)(& (*((int (*)[])g))[__gen_e_acsl_iter_5]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[])g))[__gen_e_acsl_iter_5])",
+ "tests/arith/array.i",41);
+ if (a[__gen_e_acsl_iter_5] != (*((int (*)[])g))[__gen_e_acsl_iter_5]) {
+ __gen_e_acsl_eq_3 = 0;
+ break;
+ }
+ }
+ __gen_e_acsl_iter_5 ++;
+ }
+ }
+ else __gen_e_acsl_eq_3 = 0;
+ __e_acsl_assert(__gen_e_acsl_eq_3,"Assertion","arrays",
+ "a == *((int (*)[])g)","tests/arith/array.i",41);
+ }
+ /*@ assert a ≡ *((int (*)[])g); */ ;
+ {
+ int __gen_e_acsl_ne_3;
+ __gen_e_acsl_ne_3 = 0;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_6;
+ __gen_e_acsl_iter_6 = 0;
+ while (__gen_e_acsl_iter_6 < 3) {
+ {
+ int __gen_e_acsl_valid_read_4;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*((int (*)[3])f))[__gen_e_acsl_iter_6]),
+ sizeof(int),
+ (void *)(& (*((int (*)[3])f))[__gen_e_acsl_iter_6]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[3])f))[__gen_e_acsl_iter_6])",
+ "tests/arith/array.i",42);
+ if (a[__gen_e_acsl_iter_6] != (*((int (*)[3])f))[__gen_e_acsl_iter_6]) {
+ __gen_e_acsl_ne_3 = 1;
+ break;
+ }
+ }
+ __gen_e_acsl_iter_6 ++;
+ }
+ }
+ else __gen_e_acsl_ne_3 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_3,"Assertion","arrays",
+ "a != *((int (*)[3])f)","tests/arith/array.i",42);
+ }
+ /*@ assert a ≢ *((int (*)[3])f); */ ;
+ {
+ int __gen_e_acsl_ne_4;
+ int __gen_e_acsl_valid_read_5;
+ unsigned long __gen_e_acsl__3;
+ unsigned long __gen_e_acsl__4;
+ unsigned long __gen_e_acsl_length2_2;
+ __gen_e_acsl_ne_4 = 0;
+ __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(*((int (*)[])f)),
+ sizeof(int),
+ (void *)(*((int (*)[])f)),
+ (void *)(*((int (*)[])f)));
+ __e_acsl_assert(__gen_e_acsl_valid_read_5,"RTE","arrays",
+ "mem_access: \\valid_read((int *)*((int (*)[])f))",
+ "tests/arith/array.i",43);
+ __gen_e_acsl__3 = __e_acsl_block_length((void *)(*((int (*)[])f)));
+ __gen_e_acsl__4 = __e_acsl_offset((void *)(*((int (*)[])f)));
+ __gen_e_acsl_length2_2 = (__gen_e_acsl__3 - __gen_e_acsl__4) / sizeof(int);
+ if (3UL == __gen_e_acsl_length2_2) {
+ unsigned long __gen_e_acsl_iter_7;
+ __gen_e_acsl_iter_7 = 0;
+ while (__gen_e_acsl_iter_7 < 3) {
+ {
+ int __gen_e_acsl_valid_read_6;
+ __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(& (*((int (*)[])f))[__gen_e_acsl_iter_7]),
+ sizeof(int),
+ (void *)(& (*((int (*)[])f))[__gen_e_acsl_iter_7]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_6,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[])f))[__gen_e_acsl_iter_7])",
+ "tests/arith/array.i",43);
+ if (a[__gen_e_acsl_iter_7] != (*((int (*)[])f))[__gen_e_acsl_iter_7]) {
+ __gen_e_acsl_ne_4 = 1;
+ break;
+ }
+ }
+ __gen_e_acsl_iter_7 ++;
+ }
+ }
+ else __gen_e_acsl_ne_4 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_4,"Assertion","arrays",
+ "a != *((int (*)[])f)","tests/arith/array.i",43);
+ }
+ /*@ assert a ≢ *((int (*)[])f); */ ;
+ int i[6] = {1, 2, 3, 4, 5, 6};
+ __e_acsl_store_block((void *)(i),(size_t)24);
+ __e_acsl_full_init((void *)(& i));
+ int j[6] = {4, 5, 6, 1, 2, 3};
+ __e_acsl_store_block((void *)(j),(size_t)24);
+ __e_acsl_full_init((void *)(& j));
+ int k[6] = {4, 5, 6, 4, 5, 6};
+ __e_acsl_store_block((void *)(k),(size_t)24);
+ __e_acsl_full_init((void *)(& k));
+ {
+ int __gen_e_acsl_ne_5;
+ __gen_e_acsl_ne_5 = 0;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_8;
+ __gen_e_acsl_iter_8 = 0;
+ while (__gen_e_acsl_iter_8 < 6) {
+ if (i[__gen_e_acsl_iter_8] != j[__gen_e_acsl_iter_8]) {
+ __gen_e_acsl_ne_5 = 1;
+ break;
+ }
+ __gen_e_acsl_iter_8 ++;
+ }
+ }
+ else __gen_e_acsl_ne_5 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_5,"Assertion","arrays","i != j",
+ "tests/arith/array.i",49);
+ }
+ /*@ assert i ≢ j; */ ;
+ {
+ int __gen_e_acsl_ne_6;
+ __gen_e_acsl_ne_6 = 0;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_9;
+ __gen_e_acsl_iter_9 = 0;
+ while (__gen_e_acsl_iter_9 < 6) {
+ if (i[__gen_e_acsl_iter_9] != k[__gen_e_acsl_iter_9]) {
+ __gen_e_acsl_ne_6 = 1;
+ break;
+ }
+ __gen_e_acsl_iter_9 ++;
+ }
+ }
+ else __gen_e_acsl_ne_6 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_6,"Assertion","arrays","i != k",
+ "tests/arith/array.i",50);
+ }
+ /*@ assert i ≢ k; */ ;
+ {
+ int __gen_e_acsl_ne_7;
+ __gen_e_acsl_ne_7 = 0;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_10;
+ __gen_e_acsl_iter_10 = 0;
+ while (__gen_e_acsl_iter_10 < 6) {
+ if (j[__gen_e_acsl_iter_10] != k[__gen_e_acsl_iter_10]) {
+ __gen_e_acsl_ne_7 = 1;
+ break;
+ }
+ __gen_e_acsl_iter_10 ++;
+ }
+ }
+ else __gen_e_acsl_ne_7 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_7,"Assertion","arrays","j != k",
+ "tests/arith/array.i",51);
+ }
+ /*@ assert j ≢ k; */ ;
+ int *l = & i[3];
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_full_init((void *)(& l));
+ int *m = & j[3];
+ __e_acsl_store_block((void *)(& m),(size_t)8);
+ __e_acsl_full_init((void *)(& m));
+ int *n = & k[3];
+ __e_acsl_store_block((void *)(& n),(size_t)8);
+ __e_acsl_full_init((void *)(& n));
+ {
+ int __gen_e_acsl_ne_8;
+ __gen_e_acsl_ne_8 = 0;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_11;
+ __gen_e_acsl_iter_11 = 0;
+ while (__gen_e_acsl_iter_11 < 3) {
+ {
+ int __gen_e_acsl_valid_read_7;
+ int __gen_e_acsl_valid_read_8;
+ __gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)(& (*((int (*)[3])l))[__gen_e_acsl_iter_11]),
+ sizeof(int),
+ (void *)(& (*((int (*)[3])l))[__gen_e_acsl_iter_11]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_7,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[3])l))[__gen_e_acsl_iter_11])",
+ "tests/arith/array.i",55);
+ __gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)(& (*((int (*)[3])m))[__gen_e_acsl_iter_11]),
+ sizeof(int),
+ (void *)(& (*((int (*)[3])m))[__gen_e_acsl_iter_11]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_8,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[3])m))[__gen_e_acsl_iter_11])",
+ "tests/arith/array.i",55);
+ if ((*((int (*)[3])l))[__gen_e_acsl_iter_11] != (*((int (*)[3])m))[__gen_e_acsl_iter_11]) {
+ __gen_e_acsl_ne_8 = 1;
+ break;
+ }
+ }
+ __gen_e_acsl_iter_11 ++;
+ }
+ }
+ else __gen_e_acsl_ne_8 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_8,"Assertion","arrays",
+ "*((int (*)[3])l) != *((int (*)[3])m)",
+ "tests/arith/array.i",55);
+ }
+ /*@ assert *((int (*)[3])l) ≢ *((int (*)[3])m); */ ;
+ {
+ int __gen_e_acsl_eq_4;
+ __gen_e_acsl_eq_4 = 1;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_12;
+ __gen_e_acsl_iter_12 = 0;
+ while (__gen_e_acsl_iter_12 < 3) {
+ {
+ int __gen_e_acsl_valid_read_9;
+ int __gen_e_acsl_valid_read_10;
+ __gen_e_acsl_valid_read_9 = __e_acsl_valid_read((void *)(& (*((int (*)[3])l))[__gen_e_acsl_iter_12]),
+ sizeof(int),
+ (void *)(& (*((int (*)[3])l))[__gen_e_acsl_iter_12]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_9,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[3])l))[__gen_e_acsl_iter_12])",
+ "tests/arith/array.i",56);
+ __gen_e_acsl_valid_read_10 = __e_acsl_valid_read((void *)(& (*((int (*)[3])n))[__gen_e_acsl_iter_12]),
+ sizeof(int),
+ (void *)(& (*((int (*)[3])n))[__gen_e_acsl_iter_12]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_10,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[3])n))[__gen_e_acsl_iter_12])",
+ "tests/arith/array.i",56);
+ if ((*((int (*)[3])l))[__gen_e_acsl_iter_12] != (*((int (*)[3])n))[__gen_e_acsl_iter_12]) {
+ __gen_e_acsl_eq_4 = 0;
+ break;
+ }
+ }
+ __gen_e_acsl_iter_12 ++;
+ }
+ }
+ else __gen_e_acsl_eq_4 = 0;
+ __e_acsl_assert(__gen_e_acsl_eq_4,"Assertion","arrays",
+ "*((int (*)[3])l) == *((int (*)[3])n)",
+ "tests/arith/array.i",56);
+ }
+ /*@ assert *((int (*)[3])l) ≡ *((int (*)[3])n); */ ;
+ {
+ int __gen_e_acsl_ne_9;
+ __gen_e_acsl_ne_9 = 0;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_13;
+ __e_acsl_assert(1,"RTE","arrays","array_coercion: (int)3 <= (int)6",
+ "tests/arith/array.i",59);
+ __e_acsl_assert(1,"RTE","arrays","array_coercion: (int)3 <= (int)6",
+ "tests/arith/array.i",59);
+ __gen_e_acsl_iter_13 = 0;
+ while (__gen_e_acsl_iter_13 < 3) {
+ if (i[__gen_e_acsl_iter_13] != k[__gen_e_acsl_iter_13]) {
+ __gen_e_acsl_ne_9 = 1;
+ break;
+ }
+ __gen_e_acsl_iter_13 ++;
+ }
+ }
+ else __gen_e_acsl_ne_9 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_9,"Assertion","arrays",
+ "(int [3])i != (int [3])k","tests/arith/array.i",59);
+ }
+ /*@ assert (int [3])i ≢ (int [3])k; */ ;
+ {
+ int __gen_e_acsl_eq_5;
+ __gen_e_acsl_eq_5 = 1;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_14;
+ __e_acsl_assert(1,"RTE","arrays","array_coercion: (int)3 <= (int)6",
+ "tests/arith/array.i",60);
+ __e_acsl_assert(1,"RTE","arrays","array_coercion: (int)3 <= (int)6",
+ "tests/arith/array.i",60);
+ __gen_e_acsl_iter_14 = 0;
+ while (__gen_e_acsl_iter_14 < 3) {
+ if (j[__gen_e_acsl_iter_14] != k[__gen_e_acsl_iter_14]) {
+ __gen_e_acsl_eq_5 = 0;
+ break;
+ }
+ __gen_e_acsl_iter_14 ++;
+ }
+ }
+ else __gen_e_acsl_eq_5 = 0;
+ __e_acsl_assert(__gen_e_acsl_eq_5,"Assertion","arrays",
+ "(int [3])j == (int [3])k","tests/arith/array.i",60);
+ }
+ /*@ assert (int [3])j ≡ (int [3])k; */ ;
+ {
+ int __gen_e_acsl_ne_10;
+ __gen_e_acsl_ne_10 = 0;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_15;
+ __gen_e_acsl_iter_15 = 0;
+ while (__gen_e_acsl_iter_15 < 2) {
+ {
+ int __gen_e_acsl_valid_read_11;
+ int __gen_e_acsl_valid_read_12;
+ __gen_e_acsl_valid_read_11 = __e_acsl_valid_read((void *)(& (*((int (*)[2])l))[__gen_e_acsl_iter_15]),
+ sizeof(int),
+ (void *)(& (*((int (*)[2])l))[__gen_e_acsl_iter_15]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_11,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[2])l))[__gen_e_acsl_iter_15])",
+ "tests/arith/array.i",61);
+ __gen_e_acsl_valid_read_12 = __e_acsl_valid_read((void *)(& (*((int (*)[2])m))[__gen_e_acsl_iter_15]),
+ sizeof(int),
+ (void *)(& (*((int (*)[2])m))[__gen_e_acsl_iter_15]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_12,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[2])m))[__gen_e_acsl_iter_15])",
+ "tests/arith/array.i",61);
+ if ((*((int (*)[2])l))[__gen_e_acsl_iter_15] != (*((int (*)[2])m))[__gen_e_acsl_iter_15]) {
+ __gen_e_acsl_ne_10 = 1;
+ break;
+ }
+ }
+ __gen_e_acsl_iter_15 ++;
+ }
+ }
+ else __gen_e_acsl_ne_10 = 1;
+ __e_acsl_assert(__gen_e_acsl_ne_10,"Assertion","arrays",
+ "*((int (*)[2])l) != *((int (*)[2])m)",
+ "tests/arith/array.i",61);
+ }
+ /*@ assert *((int (*)[2])l) ≢ *((int (*)[2])m); */ ;
+ {
+ int __gen_e_acsl_eq_6;
+ __gen_e_acsl_eq_6 = 1;
+ if (1) {
+ unsigned long __gen_e_acsl_iter_16;
+ __gen_e_acsl_iter_16 = 0;
+ while (__gen_e_acsl_iter_16 < 2) {
+ {
+ int __gen_e_acsl_valid_read_13;
+ int __gen_e_acsl_valid_read_14;
+ __gen_e_acsl_valid_read_13 = __e_acsl_valid_read((void *)(& (*((int (*)[2])l))[__gen_e_acsl_iter_16]),
+ sizeof(int),
+ (void *)(& (*((int (*)[2])l))[__gen_e_acsl_iter_16]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_13,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[2])l))[__gen_e_acsl_iter_16])",
+ "tests/arith/array.i",62);
+ __gen_e_acsl_valid_read_14 = __e_acsl_valid_read((void *)(& (*((int (*)[2])n))[__gen_e_acsl_iter_16]),
+ sizeof(int),
+ (void *)(& (*((int (*)[2])n))[__gen_e_acsl_iter_16]),
+ (void *)0);
+ __e_acsl_assert(__gen_e_acsl_valid_read_14,"RTE","arrays",
+ "mem_access: \\valid_read(&(*((int (*)[2])n))[__gen_e_acsl_iter_16])",
+ "tests/arith/array.i",62);
+ if ((*((int (*)[2])l))[__gen_e_acsl_iter_16] != (*((int (*)[2])n))[__gen_e_acsl_iter_16]) {
+ __gen_e_acsl_eq_6 = 0;
+ break;
+ }
+ }
+ __gen_e_acsl_iter_16 ++;
+ }
+ }
+ else __gen_e_acsl_eq_6 = 0;
+ __e_acsl_assert(__gen_e_acsl_eq_6,"Assertion","arrays",
+ "*((int (*)[2])l) == *((int (*)[2])n)",
+ "tests/arith/array.i",62);
+ }
+ /*@ assert *((int (*)[2])l) ≡ *((int (*)[2])n); */ ;
+ __e_acsl_delete_block((void *)(& n));
+ __e_acsl_delete_block((void *)(& m));
+ __e_acsl_delete_block((void *)(& l));
+ __e_acsl_delete_block((void *)(k));
+ __e_acsl_delete_block((void *)(j));
+ __e_acsl_delete_block((void *)(i));
+ __e_acsl_delete_block((void *)(& g));
+ __e_acsl_delete_block((void *)(& f));
+ __e_acsl_delete_block((void *)(c));
+ __e_acsl_delete_block((void *)(b));
+ return;
+}
+
+void vlas(int n)
+{
+ return;
+}
+
int main(void)
{
int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
int i = 0;
while (i < 3) {
@@ -21,12 +547,15 @@ int main(void)
}
}
__e_acsl_assert(T1[0] == T2[0],"Assertion","main","T1[0] == T2[0]",
- "tests/arith/array.i",13);
+ "tests/arith/array.i",109);
/*@ assert T1[0] ≡ T2[0]; */ ;
__e_acsl_assert(T1[1] != T2[1],"Assertion","main","T1[1] != T2[1]",
- "tests/arith/array.i",14);
+ "tests/arith/array.i",110);
/*@ assert T1[1] ≢ T2[1]; */ ;
+ arrays();
+ vlas(3);
__retres = 0;
+ __e_acsl_memory_clean();
return __retres;
}