diff --git a/Changelog b/Changelog
index 3093bcd3766b85f6b85958dd6bfc49fd33f42bc0..d6cb74c629b2bcd3289153888bdb04ce073246b7 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,8 @@
Open Source Release <next-release>
##################################
+o! Kernel [2021-04-09] Change the type of the measure from string to
+ logic_info in the variant AST node.
-* Kernel [2021-03-26] Raise an error if trying to merge a tentative
definition with a proper definition during linking
o Ptests [2021-03-24] Add new EXIT directive
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index eb920a51c908ceb0db8dc38638bc32db2d169db3..0c6f467509621c2a67019ac8153939e94e340d95 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1620,7 +1620,7 @@ and predicate = {
}
(** variant of a loop or a recursive function. *)
-and variant = term * string option
+and variant = term * logic_info option
(** allocates and frees.
@since Oxygen-20120901 *)
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 506bb221ee18751fb718f5c3806dc5f243890f31..6d6d06b8b3a2c7a741a6e75492d64b5a936afa1b 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1121,7 +1121,7 @@ struct
else b.b_name ^ "_"
let variant_suffix = function
- | (_,Some s) -> s
+ | (_,Some s) -> s.l_var_info.lv_name
| _ -> ""
let string_of_termination_kind = function
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 10e359d4b91f4b15b4365918dc2ad4b1a54a86c9..a98a8021d4d29a6ad15946a930dd330743cd8802 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2862,13 +2862,12 @@ class cil_printer () = object (self)
method private decrement kw fmt (t, rel) = match rel with
| None -> fprintf fmt "@[<2>%a@ %a;@]" self#pp_acsl_keyword kw self#term t
- | Some str ->
- (*TODO: replace this string with an interpreted variable*)
- fprintf fmt "@[<2>%a@ %a@ %a@ %s;@]"
+ | Some li ->
+ fprintf fmt "@[<2>%a@ %a@ %a@ %a;@]"
self#pp_acsl_keyword kw
self#term t
self#pp_acsl_keyword "for"
- str
+ self#logic_info li
method decreases fmt v = self#decrement "decreases" fmt v
method variant fmt v = self#decrement "loop variant" fmt v
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 60f93f7bb1b8c480cf391f4ef18f14c4ae95bd1f..d180c0eb9b16f72345d92c089f43e960643c6aa8 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -1037,7 +1037,7 @@ and pp_global_annotation fmt = function
and pp_custom_tree fmt _custom_tree = Format.fprintf fmt "CustomDummy"
-and pp_variant fmt = pp_pair pp_term (pp_option pp_string) fmt
+and pp_variant fmt = pp_pair pp_term (pp_option pp_logic_info) fmt
let pp_kinstr fmt = function
| Kstmt(stmt) -> Format.fprintf fmt "Kstmt(%a)" pp_stmt stmt
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 177bb48546c3d0fb3e8253674bd6c053cca8e62b..a1b0106a43512a0cb8a4b521ae017c404d3fa455 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3541,7 +3541,11 @@ struct
let type_variant env = function
| (t, None) -> (type_int_term (base_ctxt env) env t, None)
- | (t, r) -> (term env t, r)
+ | (t, Some r) ->
+ let loc = t.lexpr_loc in
+ let t = term env t in
+ let li, _, _, _ = type_logic_app env loc r [] [t; t] in
+ (t, Some li)
let id_predicate env pred = Logic_const.new_predicate (predicate env pred)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index cdf795b172ca4a20b047f8b8e7ffaf7abed40ceb..83c4a7647cb171e1138b9eadb3212f9056058ab9 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -83,11 +83,12 @@ SRC_CODE_GENERATOR:= \
label \
env \
rational \
+ typed_number \
+ logic_functions \
loops \
quantif \
at_with_lscope \
memory_translate \
- logic_functions \
logic_array \
translate \
contract \
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8fed599b80e26fcb87b3f3cf7fc0e4475e1f9975..f3a19a88325ff3e46a7405c06ec4c4e4cf0cc63b 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,7 @@
Plugin E-ACSL <next-release>
############################
+- E-ACSL [2021-04-09] Add support for loop variant.
- E-ACSL [2021-04-07] Add support for multiple binders in guarded
quantifications (frama-c/e-acsl#127).
-* runtime [2021-04-08] Fix backtrace output on failed assertion
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index a8514fc0dd945aa19088ab45a021b7878c01b97f..4e85af395ced1a11e8513c64f3c13fb55cca4d32 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -61,7 +61,6 @@ currently implemented into the \framac's \eacsl plug-in.
annotations
& behavior-specific annotations \\
& loop assigns \\
- & loop variants \\
& global annotations
\\
\hline
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
index 1de09ce3a638ab6f99d83e5be39edbb0b1cf955e..f9e3599b0b739122e5c63a997eaf979734a34b0f 100644
--- a/src/plugins/e-acsl/doc/refman/loops.tex
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -11,7 +11,7 @@
\
loop-annot ::= loop-clause* ;
{ loop-behavior* } ;
- { loop-variant? }
+ loop-variant?
\
loop-clause ::= loop-invariant ;
| { loop-assigns }
@@ -23,6 +23,6 @@
{ loop-behavior } ::= { "for" id ("," id)* ":" } ;
{ loop-clause* } ; \hspace{-35mm} annotation for behavior $id$
\
- { loop-variant } ::= { "loop" "variant" term ";" } ;
- | { "loop" "variant" term "for" id ";" } ; \hspace{-35mm} variant for relation $id$
+ loop-variant ::= "loop" "variant" term ";" ;
+ | "loop" "variant" term "for" id ";" ; \hspace{-35mm} variant for relation $id$
\end{syntax}
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index b617a2a25a6db53ae67acc05e0627d8041b58505..82e0dc5a87c8525b82c160f0d198bed05dbead73 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -122,6 +122,8 @@ src/code_generator/translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/translate_annots.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/translate_annots.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/typed_number.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/typed_number.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/dependencies/dep_eva.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/dependencies/dep_eva.enabled.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/dependencies/dep_eva.disabled.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index d10a15f1587e2974fbaa5c5311a6c1ad515a20a9..24775347413b7975db7d758f4c61ae1adcdf6b5a 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -54,6 +54,11 @@ type local_env = {
rte: bool
}
+type loop_env = {
+ variant: (term * logic_info option) option;
+ invariants: toplevel_predicate list;
+}
+
type t = {
lscope: Lscope.t;
lscope_reset: bool;
@@ -67,8 +72,8 @@ type t = {
(* Stack of contracts for active functions and statements *)
var_mapping: Varinfo.t Stack.t Logic_var.Map.t;
(* records of C bindings for logic vars *)
- loop_invariants: toplevel_predicate list list;
- (* list of loop invariants for each currently visited loops *)
+ loop_envs: loop_env list;
+ (* list of loop environment for each currently visited loops *)
cpt: int;
(* counter used when generating variables *)
}
@@ -88,6 +93,9 @@ let empty_local_env =
mp_tbl = empty_mp_tbl;
rte = true }
+let empty_loop_env =
+ { variant = None;
+ invariants = [] }
let empty =
{ lscope = Lscope.empty;
lscope_reset = true;
@@ -97,7 +105,7 @@ let empty =
env_stack = [];
contract_stack = [];
var_mapping = Logic_var.Map.empty;
- loop_invariants = [];
+ loop_envs = [];
cpt = 0 }
let top env = match env.env_stack with
@@ -113,15 +121,36 @@ let has_no_new_stmt env =
(* ************************************************************************** *)
let push_loop env =
- { env with loop_invariants = [] :: env.loop_invariants }
+ { env with loop_envs = empty_loop_env :: env.loop_envs }
-let add_loop_invariant env inv = match env.loop_invariants with
+let top_loop_env env =
+ match env.loop_envs with
| [] -> assert false
- | invs :: tl -> { env with loop_invariants = (inv :: invs) :: tl }
+ | loop_env :: tl -> loop_env, tl
+
+let set_loop_variant ?measure env t =
+ let loop_env, tl = top_loop_env env in
+ let loop_env = { loop_env with variant = Some (t, measure) } in
+ { env with loop_envs = loop_env :: tl }
-let pop_loop env = match env.loop_invariants with
+let add_loop_invariant env inv =
+ match env.loop_envs with
| [] -> assert false
- | invs :: tl -> invs, { env with loop_invariants = tl }
+ | loop_env :: tl ->
+ let loop_env = { loop_env with invariants = inv :: loop_env.invariants} in
+ { env with loop_envs = loop_env :: tl }
+
+let top_loop_variant env =
+ let loop_env, _ = top_loop_env env in
+ loop_env.variant
+
+let top_loop_invariants env =
+ let loop_env, _ = top_loop_env env in
+ loop_env.invariants
+
+let pop_loop env =
+ let _, tl = top_loop_env env in
+ { env with loop_envs = tl }
(* ************************************************************************** *)
(** {2 RTEs} *)
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 8c8152b97183aeaa0be6d330b6fc8ca4b1f4684f..3c521f8635eaedc7fbb6c2e47538343b07a76789 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -153,12 +153,15 @@ val annotation_kind: t -> Smart_stmt.annotation_kind
val set_annotation_kind: t -> Smart_stmt.annotation_kind -> t
(* ************************************************************************** *)
-(** {2 Loop invariants} *)
+(** {2 Loop annotations} *)
(* ************************************************************************** *)
val push_loop: t -> t
+val set_loop_variant: ?measure:logic_info -> t -> term -> t
val add_loop_invariant: t -> toplevel_predicate -> t
-val pop_loop: t -> toplevel_predicate list * t
+val top_loop_variant: t -> (term * logic_info option) option
+val top_loop_invariants: t -> toplevel_predicate list
+val pop_loop: t -> t
(* ************************************************************************** *)
(** {2 RTEs} *)
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index cfc504740298f8517998be505a7512b21b9e50a4..ce2757719cbb4693ca98c49c0160925e35b0fd99 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -35,6 +35,23 @@ let apply_on_var ~loc funname e =
in
Smart_stmt.rtl_call ~loc ~prefix funname [ e ]
+let name_of_mpz_arith_bop = function
+ | PlusA -> "__gmpz_add"
+ | MinusA -> "__gmpz_sub"
+ | Mult -> "__gmpz_mul"
+ | Div -> "__gmpz_tdiv_q"
+ | Mod -> "__gmpz_tdiv_r"
+ | BAnd -> "__gmpz_and"
+ | BOr -> "__gmpz_ior"
+ | BXor -> "__gmpz_xor"
+ | Shiftlt -> "__gmpz_mul_2exp"
+ | Shiftrt -> "__gmpz_tdiv_q_2exp"
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | IndexPI | MinusPI
+ | MinusPP as bop ->
+ Options.fatal
+ "Operation '%a' either not arithmetic or not supported on GMP integers"
+ Printer.pp_binop bop
+
let init ~loc e = apply_on_var "init" ~loc e
let clear ~loc e = apply_on_var "clear" ~loc e
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.mli b/src/plugins/e-acsl/src/code_generator/gmp.mli
index db4811dbeca2f1b6925cdc933215ea28c7a5cded..a4d86ff66e8969776b4061d4ba26e9990621bf08 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.mli
+++ b/src/plugins/e-acsl/src/code_generator/gmp.mli
@@ -24,6 +24,10 @@
open Cil_types
+val name_of_mpz_arith_bop: binop -> string
+(** [name_of_mpz_arith_bop bop] returns the name of the GMP function on integer
+ corresponding to the [bop] arithmetic operation. *)
+
val init: loc:location -> exp -> stmt
(** build stmt [mpz_init(v)] or [mpq_init(v)] depending on typ of [v] *)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index f095fa81d2cf4144cf04e60d98175a71b82b5bda..d9d96e9c8d7b05790452beef63497ffde4f3a958 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -224,8 +224,8 @@ let add_new_block_in_stmt env kf stmt =
end else
env
in
- (* handle loop invariants *)
- let new_stmt, env = Loops.preserve_invariant env kf stmt in
+ (* handle loop annotations *)
+ let new_stmt, env = Loops.handle_annotations env kf stmt in
new_stmt, env
else
stmt, 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 ebb75d0b2b7cda9a7955284269fcb74cab8f1041..860869d2fdc79820789af7e753044cdb8aad74ce 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -283,7 +283,9 @@ let add_generated_functions globals =
in
List.rev rev_globals
-let tapp_to_exp ~loc fname env kf t li params_ty args =
+(* Generate (and memoize) the function body and create the call to the
+ generated function. *)
+let function_to_exp ~loc fname env kf t li params_ty args =
let ret_ty = Typing.get_typ t in
let gen tbl =
let vi, kf, gen_body = generate_kf fname ~loc env ret_ty params_ty li in
@@ -342,6 +344,101 @@ let tapp_to_exp ~loc fname env kf t li params_ty args =
ret_ty
(fun vi _ -> [ Cil.mkStmtOneInstr ~valid_sid:true (mkcall vi) ])
+let tapp_to_exp kf env ?eargs tapp =
+ match tapp.term_node with
+ | Tapp(li, [], targs) ->
+ let loc = tapp.term_loc in
+ let fname = li.l_var_info.lv_name in
+ (* build the varinfo (as an expression) which stores the result of the
+ function call. *)
+ let _, e, env =
+ if Builtins.mem li.l_var_info.lv_name then
+ (* E-ACSL built-in function call *)
+ let args, env =
+ match eargs with
+ | None ->
+ List.fold_right
+ (fun targ (l, env) ->
+ let e, env = !term_to_exp_ref kf env targ in
+ e :: l, env)
+ targs
+ ([], env)
+ | Some eargs ->
+ if List.compare_lengths targs eargs != 0 then
+ Options.fatal
+ "[Tapp] unexpected number of arguments when calling %s"
+ fname;
+ eargs, env
+ in
+ Env.new_var
+ ~loc
+ ~name:(fname ^ "_app")
+ env
+ kf
+ (Some tapp)
+ (Misc.cty (Option.get li.l_type))
+ (fun vi _ ->
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var vi)
+ ~prefix:""
+ fname
+ args ])
+ else
+ (* build the arguments and compute the integer_ty of the parameters *)
+ let params_ty, args, env =
+ let eargs, env =
+ match eargs with
+ | None ->
+ List.fold_right
+ (fun targ (eargs, env) ->
+ let e, env = !term_to_exp_ref kf env targ in
+ e :: eargs, env)
+ targs
+ ([], env)
+ | Some eargs ->
+ if List.compare_lengths targs eargs != 0 then
+ Options.fatal
+ "[Tapp] unexpected number of arguments when calling %s"
+ fname;
+ eargs, env
+ in
+ try
+ List.fold_right2
+ (fun targ earg (params_ty, args, env) ->
+ let param_ty = Typing.get_number_ty targ in
+ let e, env =
+ try
+ let ty = Typing.typ_of_number_ty param_ty in
+ Typed_number.add_cast
+ ~loc
+ env
+ kf
+ (Some ty)
+ Typed_number.C_number
+ (Some targ)
+ earg
+ with Typing.Not_a_number ->
+ earg, env
+ in
+ param_ty :: params_ty, e :: args, env)
+ targs eargs
+ ([], [], env)
+ with Invalid_argument _ ->
+ Options.fatal
+ "[Tapp] unexpected number of arguments when calling %s"
+ fname
+ in
+ let gen_fname =
+ Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
+ in
+ function_to_exp ~loc gen_fname env kf tapp li params_ty args
+ in
+ e, env
+ | _ ->
+ Options.fatal
+ "tapp_to_exp called with '%a' instead of Tapp term"
+ Printer.pp_term tapp
+
(*
Local Variables:
compile-command: "make -C ../.."
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.mli b/src/plugins/e-acsl/src/code_generator/logic_functions.mli
index 0f8898ffb67155c4231e4f960f4d80b6c15c6ad8..6e3e662d05d912a3052c90d734515200a95bf118 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.mli
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.mli
@@ -37,10 +37,9 @@ open Cil_types
val reset: unit -> unit
val tapp_to_exp:
- loc:location ->
- string -> Env.t -> kernel_function ->
- term -> logic_info -> Typing.number_ty list -> exp list ->
- varinfo * exp * Env.t
+ kernel_function -> Env.t -> ?eargs:exp list -> term -> exp * Env.t
+(** Translate a Tapp term to an expression. If the optional argument [eargs] is
+ provided, then these expressions are used as arguments of the fonction. *)
val add_generated_functions: global list -> global list
(* @return the input list of globals in which the generated functions have been
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index ab0c7fa3d38c81d2a0e42f34332bdcb9897d0ed0..656f790c6b03964797ddc44cf27dd361cb7cb684 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -40,17 +40,129 @@ let term_to_exp_ref
= Extlib.mk_fun "term_to_exp_ref"
(**************************************************************************)
-(************************* Loop invariants ********************************)
+(************************* Loop annotations *******************************)
(**************************************************************************)
-let preserve_invariant env kf stmt = match stmt.skind with
+let handle_annotations env kf stmt =
+ match stmt.skind with
| Loop(_, ({ bstmts = stmts } as blk), loc, cont, break) ->
- let rec handle_invariants (stmts, env as acc) = function
- | [] ->
- (* empty loop body: no need to verify the invariant twice *)
- acc
+ (* Loop variant, save the current value of the variant *)
+ let stmts, env, variant =
+ match Env.top_loop_variant env with
+ | Some (t, measure_opt) ->
+ let env = Env.set_annotation_kind env Smart_stmt.Variant in
+ let env = Env.push env in
+ Typing.type_term ~use_gmp_opt:true t;
+ let ty = Typing.get_typ t in
+ let e, env = !term_to_exp_ref kf env t in
+ let vi_old, e_old, env =
+ Env.new_var
+ ~loc
+ ~scope:Varname.Function
+ ~name:"old_variant"
+ env
+ kf
+ (Some t)
+ ty
+ (fun _ _ -> [])
+ in
+ let stmt =
+ Smart_stmt.assigns ~loc ~result:(Cil.var vi_old) e
+ in
+ let blk, env =
+ Env.pop_and_get env stmt ~global_clear:false Env.Middle
+ in
+ Smart_stmt.block_stmt blk :: stmts, env, Some (t, e_old, measure_opt)
+ | None -> stmts, env, None
+ in
+ (* Auxiliary function to generate variant and invariant checks *)
+ let rec aux (stmts, env) = function
+ | [] -> begin
+ (* No statements remaining in the loop: variant check *)
+ let env = Env.set_annotation_kind env Smart_stmt.Variant in
+ match variant with
+ | Some (t, e_old, Some measure) ->
+ let env = Env.push env in
+ let t_old = { t with term_node = t.term_node } in
+ let tapp =
+ { term_node = Tapp(measure, [], [t_old; t]);
+ term_loc = loc;
+ term_name = [];
+ term_type = Linteger;}
+ in
+ Typing.type_term ~use_gmp_opt:true tapp;
+ let e, env = !term_to_exp_ref kf env t in
+ let e_tapp, env =
+ Logic_functions.tapp_to_exp kf env ~eargs:[e_old; e] tapp
+ in
+ let msg =
+ Format.asprintf
+ "%s(old %a, %a)"
+ measure.l_var_info.lv_name
+ Printer.pp_term t_old
+ Printer.pp_term t
+ in
+ let stmt =
+ Smart_stmt.runtime_check_with_msg
+ ~loc
+ msg
+ ~pred_kind:Assert
+ Smart_stmt.Variant
+ kf
+ e_tapp
+ in
+ let blk, env =
+ Env.pop_and_get env stmt ~global_clear:false Env.Middle
+ in
+ let stmts = Smart_stmt.block_stmt blk :: stmts in
+ stmts, env
+ | Some (t, e_old, None) ->
+ let env = Env.push env in
+ Typing.type_term ~use_gmp_opt:true t;
+ let e, env = !term_to_exp_ref kf env t in
+ let msg1 =
+ Format.asprintf
+ "(old %a) %a 0"
+ Printer.pp_term t
+ Printer.pp_relation Rge
+ in
+ let msg2 =
+ Format.asprintf
+ "(old %a) > %a"
+ Printer.pp_term t
+ Printer.pp_term t
+ in
+ let stmt =
+ Smart_stmt.block_from_stmts [
+ Smart_stmt.runtime_check_with_msg
+ ~loc
+ msg1
+ ~pred_kind:Assert
+ Smart_stmt.Variant
+ kf
+ (Cil.mkBinOp ~loc Ge e_old (Cil.zero ~loc));
+ Smart_stmt.runtime_check_with_msg
+ ~loc
+ msg2
+ ~pred_kind:Assert
+ Smart_stmt.Variant
+ kf
+ (Cil.mkBinOp ~loc Gt e_old e)
+ ]
+ in
+ let blk, env =
+ Env.pop_and_get env stmt ~global_clear:false Env.Middle
+ in
+ let stmts = Smart_stmt.block_stmt blk :: stmts in
+ stmts, env
+ | None ->
+ stmts, env
+ end
| [ last ] ->
- let invariants, env = Env.pop_loop env in
+ (* Last statement of the loop: invariant check *)
+ (* Optimisation to only verify invariant on a non-empty body loop. *)
+ let invariants = Env.top_loop_invariants env in
+ let env = Env.set_annotation_kind env Smart_stmt.Invariant in
let env = Env.push env in
let env =
let translate_named_predicate = !translate_predicate_ref in
@@ -59,15 +171,15 @@ let preserve_invariant env kf stmt = match stmt.skind with
let blk, env =
Env.pop_and_get env last ~global_clear:false Env.Before
in
- Smart_stmt.block last blk :: stmts, env
- | s :: tl ->
- handle_invariants (s :: stmts, env) tl
+ aux (Smart_stmt.block last blk :: stmts, env) []
+ | hd :: tl -> aux (hd :: stmts, env) tl
in
- let env = Env.set_annotation_kind env Smart_stmt.Invariant in
- let stmts, env = handle_invariants ([], env) stmts in
+ let stmts, env = aux ([], env) stmts in
+ (* The loop annotations have been handled, the loop environment can be
+ popped *)
+ let env = Env.pop_loop env in
let new_blk = { blk with bstmts = List.rev stmts } in
- { stmt with skind = Loop([], new_blk, loc, cont, break) },
- env
+ { stmt with skind = Loop([], new_blk, loc, cont, break) }, env
| _ ->
stmt, env
diff --git a/src/plugins/e-acsl/src/code_generator/loops.mli b/src/plugins/e-acsl/src/code_generator/loops.mli
index c797919dabca98e48323974115c2c0dc560f9d56..20b0a1262aceec6a10d19f14324afbfbb318eaff 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.mli
+++ b/src/plugins/e-acsl/src/code_generator/loops.mli
@@ -25,13 +25,14 @@
open Cil_types
(**************************************************************************)
-(************************* Loop invariants ********************************)
+(************************* Loop annotations *******************************)
(**************************************************************************)
-val preserve_invariant:
+val handle_annotations:
Env.t -> Kernel_function.t -> stmt -> stmt * Env.t
-(** Modify the given stmt loop to insert the code which preserves its loop
- invariants. Also return the modified environment. *)
+(** Modify the given stmt loop to insert the code which verifies the loop
+ annotations, ie. preserves its loop invariants and checks the loop variant.
+ Also return the modified environment. *)
(**************************************************************************)
(**************************** Nested loops ********************************)
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index 1cc37e8113c2e018354194b310ba91c89ce61a85..9799cadb813983e5a73c2fdc5844fa035b8beb34 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -44,6 +44,7 @@ type annotation_kind =
| Precondition
| Postcondition
| Invariant
+ | Variant
| RTE
let kind_to_string loc k =
@@ -54,6 +55,7 @@ let kind_to_string loc k =
| Precondition -> "Precondition"
| Postcondition -> "Postcondition"
| Invariant -> "Invariant"
+ | Variant -> "Variant"
| RTE -> "RTE")
let block stmt b = match b.bstmts with
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
index c56404a5a7120a2b752aacca94471f0c9f1ff758..4cdeb0fd23d1f0d62cb58b15806a3c321dc45c55 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.mli
@@ -104,6 +104,7 @@ type annotation_kind =
| Precondition
| Postcondition
| Invariant
+ | Variant
| RTE
val runtime_check:
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index b5b44048da759670b1884a7e9d2123655d6afd62..2c4ace3aea337c3113b74e6f977b64824b33b8b9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -45,114 +45,10 @@ let relation_to_binop = function
| Req -> Eq
| Rneq -> Ne
-let name_of_mpz_arith_bop = function
- | PlusA -> "__gmpz_add"
- | MinusA -> "__gmpz_sub"
- | Mult -> "__gmpz_mul"
- | Div -> "__gmpz_tdiv_q"
- | Mod -> "__gmpz_tdiv_r"
- | BAnd -> "__gmpz_and"
- | BOr -> "__gmpz_ior"
- | BXor -> "__gmpz_xor"
- | Shiftlt -> "__gmpz_mul_2exp"
- | Shiftrt -> "__gmpz_tdiv_q_2exp"
- | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | IndexPI | MinusPI
- | MinusPP -> assert false
-
-(* Type of a string that represents a number.
- Used when a string is required to encode a constant number because it is not
- representable in any C type *)
-type strnum =
- | Str_Z (* integers *)
- | Str_R (* reals *)
- | C_number (* integers and floats included *)
-
-(* convert [e] in a way that it is compatible with the given typing context. *)
-let add_cast ~loc ?name env kf ctx strnum t_opt e =
- let mk_mpz e =
- let _, e, env =
- Env.new_var
- ~loc
- ?name
- env
- kf
- t_opt
- (Gmp_types.Z.t ())
- (fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
- in
- e, env
- in
- let e, env = match strnum with
- | Str_Z -> mk_mpz e
- | Str_R -> Rational.create ~loc ?name e env kf t_opt
- | C_number -> e, env
- in
- match ctx with
- | None ->
- e, env
- | Some ctx ->
- let ty = Cil.typeOf e in
- match Gmp_types.Z.is_t ty, Gmp_types.Z.is_t ctx with
- | true, true ->
- (* Z --> Z *)
- e, env
- | false, true ->
- if Gmp_types.Q.is_t ty then
- (* R --> Z *)
- Rational.cast_to_z ~loc ?name e env
- else
- (* C integer --> Z *)
- let e =
- if not (Cil.isIntegralType ty) && strnum = C_number then
- (* special case for \null that must be casted to long: it is the
- only non integral value that can be seen as an integer, while the
- type system infers that it is C-representable (see
- tests/runtime/null.i) *)
- Cil.mkCast Cil.longType e (* \null *)
- else
- e
- in
- mk_mpz e
- | _, false ->
- if Gmp_types.Q.is_t ctx then
- if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *)
- e, env
- else (* C integer or Z --> R *)
- Rational.create ~loc ?name e env kf t_opt
- else if Gmp_types.Z.is_t ty || strnum = Str_Z then
- (* Z --> C type or the integer is represented by a string:
- anyway, it fits into a C integer: convert it *)
- let fname, new_ty =
- if Cil.isSignedInteger ctx then "__gmpz_get_si", Cil.longType
- else "__gmpz_get_ui", Cil.ulongType
- in
- let _, e, env =
- Env.new_var
- ~loc
- ?name
- env
- kf
- None
- new_ty
- (fun v _ ->
- [ Smart_stmt.rtl_call ~loc
- ~result:(Cil.var v)
- ~prefix:""
- fname
- [ e ] ])
- in
- e, env
- else if Gmp_types.Q.is_t ty || strnum = Str_R then
- (* R --> C type or the real is represented by a string *)
- Rational.add_cast ~loc ?name e env kf ctx
- else
- (* C type --> another C type *)
- Cil.mkCastT ~force:false ~oldt:ty ~newt:ctx e, env
-
let constant_to_exp ~loc t c =
let mk_real s =
let s = Rational.normalize_str s in
- Cil.mkString ~loc s, Str_R
+ Cil.mkString ~loc s, Typed_number.Str_R
in
match c with
| Integer(n, _repr) ->
@@ -163,7 +59,7 @@ let constant_to_exp ~loc t c =
| Typing.Rational -> mk_real (Integer.to_string n)
| Typing.Gmpz ->
(* too large integer *)
- Cil.mkString ~loc (Integer.to_string n), Str_Z
+ Cil.mkString ~loc (Integer.to_string n), Typed_number.Str_Z
| Typing.C_float fkind ->
Cil.kfloat ~loc fkind (Int64.to_float (Integer.to_int64 n)), C_number
| Typing.C_integer kind ->
@@ -171,7 +67,7 @@ let constant_to_exp ~loc t c =
match cast, kind with
| Some ty, (ILongLong | IULongLong) when Gmp_types.Z.is_t ty ->
(* too large integer *)
- Cil.mkString ~loc (Integer.to_string n), Str_Z
+ Cil.mkString ~loc (Integer.to_string n), Typed_number.Str_Z
| Some ty, _ when Gmp_types.Q.is_t ty ->
mk_real (Integer.to_string n)
| (None | Some _), _ ->
@@ -181,15 +77,15 @@ let constant_to_exp ~loc t c =
long] addition and so [1LL]. If we keep the initial string
representation, the kind would be ignored in the generated code and
so [1] would be generated. *)
- Cil.kinteger64 ~loc ~kind n, C_number)
- | LStr s -> Cil.new_exp ~loc (Const (CStr s)), C_number
- | LWStr s -> Cil.new_exp ~loc (Const (CWStr s)), C_number
- | LChr c -> Cil.new_exp ~loc (Const (CChr c)), C_number
+ Cil.kinteger64 ~loc ~kind n, Typed_number.C_number)
+ | LStr s -> Cil.new_exp ~loc (Const (CStr s)), Typed_number.C_number
+ | LWStr s -> Cil.new_exp ~loc (Const (CWStr s)), Typed_number.C_number
+ | LChr c -> Cil.new_exp ~loc (Const (CChr c)), Typed_number.C_number
| LReal lr ->
if lr.r_lower = lr.r_upper
- then Cil.kfloat ~loc FDouble lr.r_nearest, C_number
+ then Cil.kfloat ~loc FDouble lr.r_nearest, Typed_number.C_number
else mk_real lr.r_literal
- | LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), C_number
+ | LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), Typed_number.C_number
let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
let env = Env.pop (Env.pop env3) in
@@ -274,17 +170,18 @@ 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
- Smart_exp.lval ~loc lv, env, C_number, name
- | TSizeOf ty -> Cil.sizeOf ~loc ty, env, C_number, "sizeof"
+ Smart_exp.lval ~loc lv, env, Typed_number.C_number, name
+ | TSizeOf ty -> Cil.sizeOf ~loc ty, env, Typed_number.C_number, "sizeof"
| TSizeOfE t ->
let e, env = term_to_exp kf env t in
- Cil.sizeOf ~loc (Cil.typeOf e), env, C_number, "sizeof"
+ Cil.sizeOf ~loc (Cil.typeOf e), env, Typed_number.C_number, "sizeof"
| TSizeOfStr s ->
- Cil.new_exp ~loc (SizeOfStr s), env, C_number, "sizeofstr"
- | TAlignOf ty -> Cil.new_exp ~loc (AlignOf ty), env, C_number, "alignof"
+ Cil.new_exp ~loc (SizeOfStr s), env, Typed_number.C_number, "sizeofstr"
+ | TAlignOf ty ->
+ Cil.new_exp ~loc (AlignOf ty), env, Typed_number.C_number, "alignof"
| TAlignOfE t ->
let e, env = term_to_exp kf env t in
- Cil.new_exp ~loc (AlignOfE e), env, C_number, "alignof"
+ Cil.new_exp ~loc (AlignOfE e), env, Typed_number.C_number, "alignof"
| TUnOp(Neg | BNot as op, t') ->
let ty = Typing.get_typ t in
let e, env = term_to_exp kf env t' in
@@ -303,11 +200,11 @@ and context_insensitive_term_to_exp kf env t =
(Some t)
(fun _ ev -> [ Smart_stmt.rtl_call ~loc ~prefix:"" name [ ev; e ] ])
in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else if Gmp_types.Q.is_t ty then
Env.not_yet env "reals: Neg | BNot"
else
- Cil.new_exp ~loc (UnOp(op, e, ty)), env, C_number, ""
+ Cil.new_exp ~loc (UnOp(op, e, ty)), env, Typed_number.C_number, ""
| TUnOp(LNot, t) ->
let ty = Typing.get_op t in
if Gmp_types.Z.is_t ty then
@@ -318,18 +215,19 @@ and context_insensitive_term_to_exp kf env t =
let e, env =
comparison_to_exp kf ~loc ~name:"not" env Typing.gmpz Eq t zero (Some t)
in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else begin
assert (Cil.isIntegralType ty);
let e, env = term_to_exp kf env t in
- Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env, C_number, ""
+ let e = Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)) in
+ e, env, Typed_number.C_number, ""
end
| TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
let ty = Typing.get_typ t in
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
if Gmp_types.Z.is_t ty then
- let name = name_of_mpz_arith_bop bop in
+ let name = Gmp.name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
~prefix:""
name
@@ -338,13 +236,13 @@ and context_insensitive_term_to_exp kf env t =
let _, e, env =
Env.new_var_and_mpz_init ~loc ~name env kf (Some t) mk_stmts
in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else if Gmp_types.Q.is_t ty then
let e, env = Rational.binop ~loc bop e1 e2 env kf (Some t) in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
- Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, Typed_number.C_number, ""
end
| TBinOp(Div | Mod as bop, t1, t2) ->
let ty = Typing.get_typ t in
@@ -355,7 +253,7 @@ and context_insensitive_term_to_exp kf env t =
RTE should do this automatically. *)
let ctx = Typing.get_number_ty t in
let t = Some t in
- let name = name_of_mpz_arith_bop bop in
+ let name = Gmp.name_of_mpz_arith_bop bop in
(* [TODO] can now do better since the type system got some info about
possible values of [t2] *)
(* guarding divisions and modulos *)
@@ -384,20 +282,20 @@ and context_insensitive_term_to_exp kf env t =
in
let name = Misc.name_of_binop bop in
let _, e, env = Env.new_var_and_mpz_init ~loc ~name env kf t mk_stmts in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else if Gmp_types.Q.is_t ty then
let e, env = Rational.binop ~loc bop e1 e2 env kf (Some t) in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
(* no guard required since RTEs are generated separately *)
- Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, Typed_number.C_number, ""
end
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
let ity = Typing.get_integer_op t in
let e, env = comparison_to_exp ~loc kf env ity bop t1 t2 (Some t) in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
| TBinOp((Shiftlt | Shiftrt) as bop, t1, t2) ->
(* left/right shift *)
let ty = Typing.get_typ t in
@@ -486,7 +384,7 @@ and context_insensitive_term_to_exp kf env t =
(* Create the shift instruction *)
let mk_shift_instr result_e =
- let name = name_of_mpz_arith_bop bop in
+ let name = Gmp.name_of_mpz_arith_bop bop in
Smart_stmt.rtl_call ~loc
~prefix:""
name
@@ -543,10 +441,10 @@ and context_insensitive_term_to_exp kf env t =
in
let name = bop_name in
let _, e, env = Env.new_var_and_mpz_init ~loc ~name env kf t mk_stmts in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
- Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, Typed_number.C_number, ""
end
| TBinOp(LOr, t1, t2) ->
(* t1 || t2 <==> if t1 then true else t2 *)
@@ -560,7 +458,7 @@ and context_insensitive_term_to_exp kf env t =
~name:"or" loc kf (Some t) e1 (Cil.one loc, env') res2
)
in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
| TBinOp(LAnd, t1, t2) ->
(* t1 && t2 <==> if t1 then t2 else false *)
let e, env =
@@ -573,7 +471,7 @@ and context_insensitive_term_to_exp kf env t =
~name:"and" loc kf (Some t) e1 res2 (Cil.zero loc, env3)
)
in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
| TBinOp((BOr | BXor | BAnd) as bop, t1, t2) ->
(* other logic/arith operators *)
let ty = Typing.get_typ t in
@@ -581,17 +479,17 @@ and context_insensitive_term_to_exp kf env t =
let e2, env = term_to_exp kf env t2 in
if Gmp_types.Z.is_t ty then
let mk_stmts _v e =
- let name = name_of_mpz_arith_bop bop in
+ let name = Gmp.name_of_mpz_arith_bop bop in
let instr = Smart_stmt.rtl_call ~loc ~prefix:"" name [ e; e1; e2 ] in
[ instr ]
in
let name = Misc.name_of_binop bop in
let t = Some t in
let _, e, env = Env.new_var_and_mpz_init ~loc ~name env kf t mk_stmts in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else begin
assert (Logic_typing.is_integral_type t.term_type);
- Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, Typed_number.C_number, ""
end
| TBinOp(PlusPI | IndexPI | MinusPI as bop, t1, t2) ->
if Misc.is_set_of_ptr_or_array t1.term_type ||
@@ -607,14 +505,15 @@ and context_insensitive_term_to_exp kf env t =
in
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
- Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
+ Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, Typed_number.C_number, ""
| TBinOp(MinusPP, t1, t2) ->
begin match Typing.get_number_ty t with
| Typing.C_integer _ ->
let e1, env = term_to_exp kf env t1 in
let e2, env = term_to_exp kf env t2 in
let ty = Typing.get_typ t in
- Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)), env, C_number, ""
+ let e = Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)) in
+ e, env, Typed_number.C_number, ""
| Typing.Gmpz ->
Env.not_yet env "pointer subtraction resulting in gmp"
| Typing.(C_float _ | Rational | Real | Nan) ->
@@ -623,73 +522,27 @@ and context_insensitive_term_to_exp kf env t =
| TCastE(ty, t') ->
let e, env = term_to_exp kf env t' in
let e, env =
- add_cast ~loc ~name:"cast" env kf (Some ty) C_number (Some t) e
+ Typed_number.add_cast
+ ~loc
+ ~name:"cast"
+ env
+ kf
+ (Some ty)
+ Typed_number.C_number
+ (Some t)
+ e
in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
| TLogic_coerce _ -> assert false (* handle in [term_to_exp] *)
| TAddrOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
- Cil.mkAddrOf ~loc lv, env, C_number, "addrof"
+ Cil.mkAddrOf ~loc lv, env, Typed_number.C_number, "addrof"
| TStartOf lv ->
let lv, env, _ = tlval_to_lval kf env lv in
- Cil.mkAddrOrStartOf ~loc lv, env, C_number, "startof"
- | Tapp(li, [], targs) ->
- let fname = li.l_var_info.lv_name in
- (* build the varinfo (as an expression) which stores the result of the
- function call. *)
- let _, e, env =
- if Builtins.mem li.l_var_info.lv_name then
- (* E-ACSL built-in function call *)
- let args, env =
- try
- List.fold_right
- (fun targ (l, env) ->
- let e, env = term_to_exp kf env targ in
- e :: l, env)
- targs
- ([], env)
- with Invalid_argument _ ->
- Options.fatal
- "[Tapp] unexpected number of arguments when calling %s"
- fname
- in
- Env.new_var
- ~loc
- ~name:(fname ^ "_app")
- env
- kf
- (Some t)
- (Misc.cty (Option.get li.l_type))
- (fun vi _ ->
- [ Smart_stmt.rtl_call ~loc
- ~result:(Cil.var vi)
- ~prefix:""
- fname
- args ])
- else
- (* build the arguments and compute the integer_ty of the parameters *)
- let params_ty, args, env =
- List.fold_right
- (fun targ (params_ty, args, env) ->
- let e, env = term_to_exp kf env targ in
- let param_ty = Typing.get_number_ty targ in
- let e, env =
- try
- let ty = Typing.typ_of_number_ty param_ty in
- add_cast loc env kf (Some ty) C_number (Some targ) e
- with Typing.Not_a_number ->
- e, env
- in
- param_ty :: params_ty, e :: args, env)
- targs
- ([], [], env)
- in
- let gen_fname =
- Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
- in
- Logic_functions.tapp_to_exp ~loc gen_fname env kf t li params_ty args
- in
- e, env, C_number, "app"
+ Cil.mkAddrOrStartOf ~loc lv, env, Typed_number.C_number, "startof"
+ | Tapp(_, [], _) ->
+ let e, env = Logic_functions.tapp_to_exp kf env t in
+ e, env, Typed_number.C_number, "app"
| Tapp(_, _ :: _, _) ->
Env.not_yet env "logic functions with labels"
| Tlambda _ -> Env.not_yet env "functional"
@@ -704,16 +557,16 @@ and context_insensitive_term_to_exp kf env t =
conditional_to_exp loc kf (Some t) e1 res2 res3
)
in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
| Tat(t, BuiltinLabel Here) ->
let e, env = term_to_exp kf env t in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
| Tat(t', label) ->
let lscope = Env.Logic_scope.get env in
let pot = Lscope.PoT_term t' in
if Lscope.is_used lscope pot then
let e, env = At_with_lscope.to_exp ~loc kf env pot label in
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
else
let e, env = term_to_exp kf (Env.push env) t' in
let e, env, sty = at_to_exp_no_lscope env kf (Some t) label e in
@@ -721,22 +574,23 @@ and context_insensitive_term_to_exp kf env t =
| Tbase_addr(BuiltinLabel Here, t) ->
let name = "base_addr" in
let e, env = Memory_translate.call ~loc kf name Cil.voidPtrType env t in
- e, env, C_number, name
+ e, env, Typed_number.C_number, name
| Tbase_addr _ -> Env.not_yet env "labeled \\base_addr"
| Toffset(BuiltinLabel Here, t) ->
let size_t = Cil.theMachine.Cil.typeOfSizeOf in
let name = "offset" in
let e, env = Memory_translate.call ~loc kf name size_t env t in
- e, env, C_number, name
+ e, env, Typed_number.C_number, name
| Toffset _ -> Env.not_yet env "labeled \\offset"
| Tblock_length(BuiltinLabel Here, t) ->
let size_t = Cil.theMachine.Cil.typeOfSizeOf in
let name = "block_length" in
let e, env = Memory_translate.call ~loc kf name size_t env t in
- e, env, C_number, name
+ e, env, Typed_number.C_number, name
| Tblock_length _ -> Env.not_yet env "labeled \\block_length"
| Tnull ->
- Cil.mkCast (TPtr(TVoid [], [])) (Cil.zero ~loc), env, C_number, "null"
+ let e = Cil.mkCast (TPtr(TVoid [], [])) (Cil.zero ~loc) in
+ e, env, Typed_number.C_number, "null"
| TUpdate _ -> Env.not_yet env "functional update"
| Ttypeof _ -> Env.not_yet env "typeof"
| Ttype _ -> Env.not_yet env "C type"
@@ -751,7 +605,7 @@ and context_insensitive_term_to_exp kf env t =
let env = env_of_li li kf env loc in
let e, env = term_to_exp kf env t in
Interval.Env.remove li.l_var_info;
- e, env, C_number, ""
+ e, env, Typed_number.C_number, ""
(* Convert an ACSL term into a corresponding C expression (if any) in the given
environment. Also extend this environment in order to include the generating
@@ -767,7 +621,7 @@ and term_to_exp kf env t =
let env = if generate_rte then translate_rte kf env e else env in
let cast = Typing.get_cast t in
let name = if name = "" then None else Some name in
- add_cast
+ Typed_number.add_cast
~loc:t.term_loc
?name
env
@@ -878,7 +732,7 @@ and at_to_exp_no_lscope env kf t_opt label e =
end
in
ignore (Visitor.visitFramacStmt o stmt);
- res, !env_ref, C_number
+ res, !env_ref, Typed_number.C_number
and env_of_li li kf env loc =
let t = Misc.term_of_li li in
@@ -994,7 +848,7 @@ and predicate_content_to_exp ?name kf env p =
(* convert [t'] to [e] in a separated local env *)
let e, env = predicate_to_exp kf (Env.push env) p' in
let e, env, sty = at_to_exp_no_lscope env kf None label e in
- assert (sty = C_number);
+ assert (sty = Typed_number.C_number);
e, env
end
| Pvalid_read(BuiltinLabel Here as llabel, t) as pc
@@ -1087,13 +941,13 @@ and predicate_to_exp ?name kf ?rte env p =
let e, env = predicate_content_to_exp ?name kf env p in
let env = if rte then translate_rte kf env e else env in
let cast = Typing.get_cast_of_predicate p in
- add_cast
+ Typed_number.add_cast
~loc:p.pred_loc
?name
env
kf
cast
- C_number
+ Typed_number.C_number
None
e
)
@@ -1205,10 +1059,15 @@ let untyped_predicate_to_exp p =
let env = Env.push Env.empty in
let env = Env.rte env false in
let e, env =
- try generalized_untyped_predicate_to_exp ~must_clear_typing:false (Kernel_function.dummy ()) env p
+ try generalized_untyped_predicate_to_exp
+ ~must_clear_typing:false
+ (Kernel_function.dummy ())
+ env
+ p
with Rtl.Symbols.Unregistered _ -> raise (No_simple_predicate_translation p)
in
- if not (Env.has_no_new_stmt env) then raise (No_simple_predicate_translation p);
+ if not (Env.has_no_new_stmt env)
+ then raise (No_simple_predicate_translation p);
e
(* This function is used by plug-in [Cfp]. *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index 2046b2b4bed3954cd134ae8cf36ec5864bb8c7c3..e4f26ec3919ed0ecbc5de7c3e0c9186077de6bb1 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -57,7 +57,7 @@ let pre_funspec kf kinstr env funspec =
unsupported
(fun spec ->
let ppt = Property.ip_decreases_of_spec kf kinstr spec in
- if must_translate_opt ppt then Env.not_yet env "variant clause")
+ if must_translate_opt ppt then Env.not_yet env "decreases clause")
funspec;
(* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
unsupported
@@ -67,8 +67,9 @@ let pre_funspec kf kinstr env funspec =
funspec;
env
in
- let env = convert_unsupported_clauses env in
let loc = Kernel_function.get_location kf in
+ Cil.CurrentLoc.set loc;
+ let env = convert_unsupported_clauses env in
let contract = Contract.create ~loc funspec in
Env.with_rte env true
~f:(fun env -> Contract.translate_preconditions kf kinstr env contract)
@@ -110,9 +111,9 @@ let pre_code_annotation kf stmt env annot =
else env
else
env
- | AVariant _ ->
+ | AVariant (t, measure) ->
if must_translate (Property.ip_of_code_annot_single kf stmt annot)
- then Env.not_yet env "variant"
+ then Env.set_loop_variant env ?measure t
else env
| AAssigns _ ->
(* TODO: it is not a precondition --> should not be handled here,
diff --git a/src/plugins/e-acsl/src/code_generator/typed_number.ml b/src/plugins/e-acsl/src/code_generator/typed_number.ml
new file mode 100644
index 0000000000000000000000000000000000000000..dfa8a4497a868038fade0ac52e77a056075c37cc
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/typed_number.ml
@@ -0,0 +1,109 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Manipulate the type of numbers. *)
+
+type strnum =
+ | Str_Z (* integers *)
+ | Str_R (* reals *)
+ | C_number (* integers and floats included *)
+
+let add_cast ~loc ?name env kf ctx strnum t_opt e =
+ let mk_mpz e =
+ let _, e, env =
+ Env.new_var
+ ~loc
+ ?name
+ env
+ kf
+ t_opt
+ (Gmp_types.Z.t ())
+ (fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
+ in
+ e, env
+ in
+ let e, env = match strnum with
+ | Str_Z -> mk_mpz e
+ | Str_R -> Rational.create ~loc ?name e env kf t_opt
+ | C_number -> e, env
+ in
+ match ctx with
+ | None ->
+ e, env
+ | Some ctx ->
+ let ty = Cil.typeOf e in
+ match Gmp_types.Z.is_t ty, Gmp_types.Z.is_t ctx with
+ | true, true ->
+ (* Z --> Z *)
+ e, env
+ | false, true ->
+ if Gmp_types.Q.is_t ty then
+ (* R --> Z *)
+ Rational.cast_to_z ~loc ?name e env
+ else
+ (* C integer --> Z *)
+ let e =
+ if not (Cil.isIntegralType ty) && strnum = C_number then
+ (* special case for \null that must be casted to long: it is the
+ only non integral value that can be seen as an integer, while the
+ type system infers that it is C-representable (see
+ tests/runtime/null.i) *)
+ Cil.mkCast Cil.longType e (* \null *)
+ else
+ e
+ in
+ mk_mpz e
+ | _, false ->
+ if Gmp_types.Q.is_t ctx then
+ if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *)
+ e, env
+ else (* C integer or Z --> R *)
+ Rational.create ~loc ?name e env kf t_opt
+ else if Gmp_types.Z.is_t ty || strnum = Str_Z then
+ (* Z --> C type or the integer is represented by a string:
+ anyway, it fits into a C integer: convert it *)
+ let fname, new_ty =
+ if Cil.isSignedInteger ctx then "__gmpz_get_si", Cil.longType
+ else "__gmpz_get_ui", Cil.ulongType
+ in
+ let _, e, env =
+ Env.new_var
+ ~loc
+ ?name
+ env
+ kf
+ None
+ new_ty
+ (fun v _ ->
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var v)
+ ~prefix:""
+ fname
+ [ e ] ])
+ in
+ e, env
+ else if Gmp_types.Q.is_t ty || strnum = Str_R then
+ (* R --> C type or the real is represented by a string *)
+ Rational.add_cast ~loc ?name e env kf ctx
+ else
+ (* C type --> another C type *)
+ Cil.mkCastT ~force:false ~oldt:ty ~newt:ctx e, env
diff --git a/src/plugins/e-acsl/src/code_generator/typed_number.mli b/src/plugins/e-acsl/src/code_generator/typed_number.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf75cc1cfe617ed4ff73ce2f39f1632e5fa58362
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/typed_number.mli
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Manipulate the type of numbers. *)
+
+open Cil_types
+
+(** Type of a string that represents a number.
+ Used when a string is required to encode a constant number because it is not
+ representable in any C type *)
+type strnum =
+ | Str_Z (* integers *)
+ | Str_R (* reals *)
+ | C_number (* integers and floats included *)
+
+(** [add_cast ~loc ?name env kf ctx sty t_opt e] convert number expression [e]
+ in a way that it is compatible with the given typing context [ctx].
+ [sty] indicates if the expression is a string representing a number (integer
+ or real) or directly a C number type.
+ [t_opt] is the term that is represented by the expression [e]. *)
+val add_cast:
+ loc:location ->
+ ?name:string ->
+ Env.t ->
+ kernel_function ->
+ typ option ->
+ strnum ->
+ term option ->
+ exp ->
+ exp * Env.t
diff --git a/src/plugins/e-acsl/tests/constructs/decrease.i b/src/plugins/e-acsl/tests/constructs/decrease.i
new file mode 100644
index 0000000000000000000000000000000000000000..b5dc3a50ca7515eb3f4fa32bcff259c351083bce
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/decrease.i
@@ -0,0 +1,87 @@
+/* run.config_ci, run.config_dev
+ STDOPT: +"-eva-ignore-recursive-calls -eva-slevel 7"
+ */
+
+// Test that the last iteration of the variant can be negative
+int f(int x) {
+ /*@ loop variant x; */
+ while (x >= 0) {
+ x -= 2;
+ }
+ return x;
+}
+
+// Test variant with general measure
+/*@ predicate lexico(integer x, integer y) =
+ x > y && 0 <= x; */
+int g(int x) {
+ /*@ loop variant x for lexico; */
+ while (x >= 0) {
+ x -= 2;
+ }
+ return x;
+}
+
+// Test classic variant
+/*@ requires n <= 12; */
+int fact(int n) {
+ int result = n;
+ /*@ loop invariant n >= 1;
+ loop variant n; */
+ while (n > 1) {
+ result *= (n - 1);
+ --n;
+ }
+ return result;
+}
+
+// Test decreases on recursive function
+/*@ decreases n; */
+int fib(int n) {
+ if (n == 1) return 1;
+ if (n <= 0) return 0;
+ return fib(n - 1) + fib(n - 2);
+}
+
+// Test decreases on mutually recursive functions
+int odd(int);
+/*@ requires n >= 0;
+ decreases n; */
+int even(int n) {
+ if (n == 0) return 1;
+ return odd(n - 1);
+}
+/*@ requires n >= 0;
+ decreases n; */
+int odd(int n) {
+ if (n == 0) return 0;
+ return even(n - 1);
+}
+
+int main() {
+ int f10 = f(10);
+ //@ assert f10 == -2;
+ int f7 = f(7);
+ //@ assert f7 == -1;
+ int g10 = g(10);
+ //@ assert g10 == -2;
+ int g7 = g(7);
+ //@ assert g7 == -1;
+
+ int fact7 = fact(7);
+ //@ assert fact7 == 5040;
+
+ int fib7 = fib(7);
+ //@ assert fib7 == 13;
+
+ int even7 = even(7);
+ //@ assert even7 == 0;
+ int even10 = even(10);
+ //@ assert even10 == 1;
+ int odd7 = odd(7);
+ //@ assert odd7 == 1;
+ int odd10 = odd(10);
+ //@ assert odd10 == 0;
+
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..74f4f63423966d0396e43ebbb9a02c8887c3ddcf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle
@@ -0,0 +1,73 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/constructs/decrease.i:50: Warning:
+ E-ACSL construct `decreases clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/constructs/decrease.i:47: Warning:
+ E-ACSL construct `decreases clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/constructs/decrease.i:40: Warning:
+ E-ACSL construct `decreases clause' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva] tests/constructs/decrease.i:43: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_fib (__gen_e_acsl_fib <- fib :: tests/constructs/decrease.i:40 <-
+ __gen_e_acsl_fib :: tests/constructs/decrease.i:74 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva] tests/constructs/decrease.i:43: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_fib (__gen_e_acsl_fib <- fib :: tests/constructs/decrease.i:40 <-
+ __gen_e_acsl_fib :: tests/constructs/decrease.i:74 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:43: Warning:
+ signed overflow.
+ assert -2147483648 ≤ tmp + tmp_0;
+ (tmp from fib(n - 1), tmp_0 from fib(n - 2))
+[eva:alarm] tests/constructs/decrease.i:43: Warning:
+ signed overflow.
+ assert tmp + tmp_0 ≤ 2147483647;
+ (tmp from fib(n - 1), tmp_0 from fib(n - 2))
+[eva:alarm] tests/constructs/decrease.i:75: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva] tests/constructs/decrease.i:58: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_even (__gen_e_acsl_even <- odd :: tests/constructs/decrease.i:47 <-
+ __gen_e_acsl_odd :: tests/constructs/decrease.i:52 <-
+ even :: tests/constructs/decrease.i:50 <-
+ __gen_e_acsl_even :: tests/constructs/decrease.i:77 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:78: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva] tests/constructs/decrease.i:58: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_even (__gen_e_acsl_even <- odd :: tests/constructs/decrease.i:47 <-
+ __gen_e_acsl_odd :: tests/constructs/decrease.i:52 <-
+ even :: tests/constructs/decrease.i:50 <-
+ __gen_e_acsl_even :: tests/constructs/decrease.i:79 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:80: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva] tests/constructs/decrease.i:52: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_odd (__gen_e_acsl_odd <- even :: tests/constructs/decrease.i:50 <-
+ __gen_e_acsl_even :: tests/constructs/decrease.i:58 <-
+ odd :: tests/constructs/decrease.i:47 <-
+ __gen_e_acsl_odd :: tests/constructs/decrease.i:81 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:82: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva] tests/constructs/decrease.i:52: Warning:
+ recursive call during value analysis
+ of __gen_e_acsl_odd (__gen_e_acsl_odd <- even :: tests/constructs/decrease.i:50 <-
+ __gen_e_acsl_even :: tests/constructs/decrease.i:58 <-
+ odd :: tests/constructs/decrease.i:47 <-
+ __gen_e_acsl_odd :: tests/constructs/decrease.i:83 <-
+ main).
+ Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:84: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c
new file mode 100644
index 0000000000000000000000000000000000000000..41a66ca7b5efb2a1f491aca7a9eefbe396862a59
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c
@@ -0,0 +1,226 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern int __e_acsl_sound_verdict;
+
+int f(int x)
+{
+ int __gen_e_acsl_old_variant;
+ /*@ loop variant x; */
+ while (1) {
+ __gen_e_acsl_old_variant = x;
+ if (! (x >= 0)) break;
+ x -= 2;
+ __e_acsl_assert(__gen_e_acsl_old_variant >= 0,1,"Variant","f",
+ "(old x) \342\211\245 0","tests/constructs/decrease.i",8);
+ __e_acsl_assert(__gen_e_acsl_old_variant > x,1,"Variant","f",
+ "(old x) > x","tests/constructs/decrease.i",8);
+ }
+ return x;
+}
+
+/*@ predicate lexico(ℤ x, ℤ y) = x > y ∧ 0 ≤ x;
+
+*/
+int __gen_e_acsl_lexico(int x, int y);
+
+int g(int x)
+{
+ int __gen_e_acsl_old_variant;
+ /*@ loop variant x for lexico; */
+ while (1) {
+ __gen_e_acsl_old_variant = x;
+ if (! (x >= 0)) break;
+ x -= 2;
+ {
+ int __gen_e_acsl_lexico_2;
+ __gen_e_acsl_lexico_2 = __gen_e_acsl_lexico(__gen_e_acsl_old_variant,x);
+ __e_acsl_assert(__gen_e_acsl_lexico_2,1,"Variant","g",
+ "lexico(old x, x)","tests/constructs/decrease.i",19);
+ }
+ }
+ return x;
+}
+
+/*@ requires n ≤ 12; */
+int __gen_e_acsl_fact(int n);
+
+int fact(int n)
+{
+ int __gen_e_acsl_old_variant;
+ int result = n;
+ __e_acsl_assert(n >= 1,1,"Invariant","fact","n >= 1",
+ "tests/constructs/decrease.i",29);
+ /*@ loop invariant n ≥ 1;
+ loop variant n; */
+ while (1) {
+ __gen_e_acsl_old_variant = n;
+ if (! (n > 1)) break;
+ result *= n - 1;
+ n --;
+ __e_acsl_assert(n >= 1,1,"Invariant","fact","n >= 1",
+ "tests/constructs/decrease.i",29);
+ __e_acsl_assert(__gen_e_acsl_old_variant >= 0,1,"Variant","fact",
+ "(old n) \342\211\245 0","tests/constructs/decrease.i",
+ 31);
+ __e_acsl_assert(__gen_e_acsl_old_variant > n,1,"Variant","fact",
+ "(old n) > n","tests/constructs/decrease.i",31);
+ }
+ return result;
+}
+
+/*@ decreases n; */
+int __gen_e_acsl_fib(int n);
+
+int fib(int n)
+{
+ int __retres;
+ int tmp;
+ int tmp_0;
+ if (n == 1) {
+ __retres = 1;
+ goto return_label;
+ }
+ if (n <= 0) {
+ __retres = 0;
+ goto return_label;
+ }
+ tmp = __gen_e_acsl_fib(n - 1);
+ tmp_0 = __gen_e_acsl_fib(n - 2);
+ /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp + tmp_0; */
+ /*@ assert Eva: signed_overflow: tmp + tmp_0 ≤ 2147483647; */
+ __retres = tmp + tmp_0;
+ return_label: return __retres;
+}
+
+/*@ requires n ≥ 0;
+ decreases n; */
+int __gen_e_acsl_odd(int n);
+
+int odd(int n);
+
+/*@ requires n ≥ 0;
+ decreases n; */
+int __gen_e_acsl_even(int n);
+
+int even(int n)
+{
+ int __retres;
+ int tmp;
+ if (n == 0) {
+ __retres = 1;
+ goto return_label;
+ }
+ tmp = __gen_e_acsl_odd(n - 1);
+ __retres = tmp;
+ return_label: return __retres;
+}
+
+int odd(int n)
+{
+ int __retres;
+ int tmp;
+ if (n == 0) {
+ __retres = 0;
+ goto return_label;
+ }
+ tmp = __gen_e_acsl_even(n - 1);
+ __retres = tmp;
+ return_label: return __retres;
+}
+
+int main(void)
+{
+ int __retres;
+ int f10 = f(10);
+ __e_acsl_assert(f10 == -2,1,"Assertion","main","f10 == -2",
+ "tests/constructs/decrease.i",63);
+ /*@ assert f10 ≡ -2; */ ;
+ int f7 = f(7);
+ __e_acsl_assert(f7 == -1,1,"Assertion","main","f7 == -1",
+ "tests/constructs/decrease.i",65);
+ /*@ assert f7 ≡ -1; */ ;
+ int g10 = g(10);
+ __e_acsl_assert(g10 == -2,1,"Assertion","main","g10 == -2",
+ "tests/constructs/decrease.i",67);
+ /*@ assert g10 ≡ -2; */ ;
+ int g7 = g(7);
+ __e_acsl_assert(g7 == -1,1,"Assertion","main","g7 == -1",
+ "tests/constructs/decrease.i",69);
+ /*@ assert g7 ≡ -1; */ ;
+ int fact7 = __gen_e_acsl_fact(7);
+ __e_acsl_assert(fact7 == 5040,1,"Assertion","main","fact7 == 5040",
+ "tests/constructs/decrease.i",72);
+ /*@ assert fact7 ≡ 5040; */ ;
+ int fib7 = __gen_e_acsl_fib(7);
+ __e_acsl_assert(fib7 == 13,1,"Assertion","main","fib7 == 13",
+ "tests/constructs/decrease.i",75);
+ /*@ assert fib7 ≡ 13; */ ;
+ int even7 = __gen_e_acsl_even(7);
+ __e_acsl_assert(even7 == 0,1,"Assertion","main","even7 == 0",
+ "tests/constructs/decrease.i",78);
+ /*@ assert even7 ≡ 0; */ ;
+ int even10 = __gen_e_acsl_even(10);
+ __e_acsl_assert(even10 == 1,1,"Assertion","main","even10 == 1",
+ "tests/constructs/decrease.i",80);
+ /*@ assert even10 ≡ 1; */ ;
+ int odd7 = __gen_e_acsl_odd(7);
+ __e_acsl_assert(odd7 == 1,1,"Assertion","main","odd7 == 1",
+ "tests/constructs/decrease.i",82);
+ /*@ assert odd7 ≡ 1; */ ;
+ int odd10 = __gen_e_acsl_odd(10);
+ __e_acsl_assert(odd10 == 0,1,"Assertion","main","odd10 == 0",
+ "tests/constructs/decrease.i",84);
+ /*@ assert odd10 ≡ 0; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+/*@ requires n ≥ 0;
+ decreases n; */
+int __gen_e_acsl_even(int n)
+{
+ int __retres;
+ __e_acsl_assert(n >= 0,1,"Precondition","even","n >= 0",
+ "tests/constructs/decrease.i",48);
+ __retres = even(n);
+ return __retres;
+}
+
+/*@ requires n ≥ 0;
+ decreases n; */
+int __gen_e_acsl_odd(int n)
+{
+ int __retres;
+ __e_acsl_assert(n >= 0,1,"Precondition","odd","n >= 0",
+ "tests/constructs/decrease.i",54);
+ __retres = odd(n);
+ return __retres;
+}
+
+/*@ decreases n; */
+int __gen_e_acsl_fib(int n)
+{
+ int __retres;
+ __retres = fib(n);
+ return __retres;
+}
+
+/*@ requires n ≤ 12; */
+int __gen_e_acsl_fact(int n)
+{
+ int __retres;
+ __e_acsl_assert(n <= 12,1,"Precondition","fact","n <= 12",
+ "tests/constructs/decrease.i",26);
+ __retres = fact(n);
+ return __retres;
+}
+
+int __gen_e_acsl_lexico(int x, int y)
+{
+ int __gen_e_acsl_and;
+ if (x > y) __gen_e_acsl_and = 0 <= x; else __gen_e_acsl_and = 0;
+ return __gen_e_acsl_and;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/decrease.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/decrease.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
index 2a20efd543f570f710b1f32d7177806c057ed931..6420addb008c45e48b24143a2062ccc305fbe9b7 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
@@ -4,8 +4,6 @@
[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:26: Warning:
- E-ACSL construct `variant' is not yet supported. Ignoring annotation.
[e-acsl] tests/special/e-acsl-valid.c:24: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
index 5653d657ff06a0a63975ad0803668d46a9f06e70..8fd9ca39e0bf76b673897322fa3d71b82bcf9f84 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
@@ -26,6 +26,7 @@ void __gen_e_acsl_f(int *x, int *y);
void f(int *x, int *y)
{
+ long __gen_e_acsl_old_variant;
{
int __gen_e_acsl_valid_read;
__e_acsl_store_block((void *)(& y),(size_t)8);
@@ -51,10 +52,18 @@ void f(int *x, int *y)
int i = 0;
/*@ loop invariant 0 ≤ i ≤ 1;
loop variant 2 - i; */
- while (i < 1) {
+ while (1) {
+ __gen_e_acsl_old_variant = 2L - i;
+ if (! (i < 1)) break;
/*@ assert 1 ≡ 1; */ ;
/*@ assert \valid(y); */ ;
i ++;
+ __e_acsl_assert(__gen_e_acsl_old_variant >= 0L,1,"Variant","f",
+ "(old 2 - i) \342\211\245 0",
+ "tests/special/e-acsl-valid.c",31);
+ __e_acsl_assert(__gen_e_acsl_old_variant > 2L - i,1,"Variant","f",
+ "(old 2 - i) > 2 - i","tests/special/e-acsl-valid.c",
+ 31);
}
}
__e_acsl_delete_block((void *)(& y));