From be3154c8a55679e450f4dae2107c1f70a4d79f54 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 13 Jul 2021 16:59:50 +0200
Subject: [PATCH] [eacsl] Add a "not yet" error in case of GMP loop variant
---
.../e-acsl/src/code_generator/loops.ml | 57 ++++++++++---------
1 file changed, 31 insertions(+), 26 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 9e5d2e827ee..c6d6e726ba7 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -48,32 +48,37 @@ let handle_annotations env kf stmt =
| Loop(_, ({ bstmts = stmts } as blk), loc, cont, break) ->
(* 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
+ Error.handle
+ (fun (stmts, env, _) ->
+ 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
+ if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
+ 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
+ let stmts = Smart_stmt.block_stmt blk :: stmts in
+ stmts, env, Some (t, e_old, measure_opt)
+ | None -> stmts, env, None)
+ (stmts, env, None)
in
(* Auxiliary function to generate variant and invariant checks *)
let rec aux (stmts, env) = function
--
GitLab