Skip to content
Snippets Groups Projects
Commit a5e7798c authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl] improved style in gmp.ml*

parent 39ee3f67
No related branches found
No related tags found
No related merge requests found
...@@ -130,9 +130,7 @@ let init_set ~loc lv ev e = ...@@ -130,9 +130,7 @@ let init_set ~loc lv ev e =
mpz_init_set "__gmpz_init_set" mpz_init_set "__gmpz_init_set"
else if Gmp_types.Q.is_t ty then else if Gmp_types.Q.is_t ty then
Smart_stmt.block_stmt Smart_stmt.block_stmt
(Cil.mkBlock (Cil.mkBlock [ init ~loc ev; assign ~loc lv ev e ])
[ init ~loc ev ;
assign ~loc lv ev e ])
else else
mpz_init_set "" mpz_init_set ""
...@@ -175,7 +173,7 @@ module Z = struct ...@@ -175,7 +173,7 @@ module Z = struct
kf kf
t_opt t_opt
(Gmp_types.Z.t ()) (Gmp_types.Z.t ())
(fun lv v -> [ init_set ~loc (Cil.var lv) v e ]) (fun vi vi_e -> [ init_set ~loc (Cil.var vi) vi_e e ])
in in
e, env e, env
...@@ -208,9 +206,7 @@ module Z = struct ...@@ -208,9 +206,7 @@ module Z = struct
name name
[ e; e1; e2 ] ] in [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in let name = Misc.name_of_binop bop in
let _, e, env = let _, e, env = new_var ~loc ~name env kf t_opt mk_stmts in
new_var ~loc ~name env kf t_opt mk_stmts
in
e,env e,env
let cmp ~loc name t_opt bop env kf e1 e2 = let cmp ~loc name t_opt bop env kf e1 e2 =
...@@ -338,9 +334,7 @@ module Q = struct ...@@ -338,9 +334,7 @@ module Q = struct
kf kf
t_opt t_opt
(Gmp_types.Q.t ()) (Gmp_types.Q.t ())
(fun vi vi_e -> (fun vi vi_e -> [ init_set ~loc (Cil.var vi) vi_e e ])
[ init ~loc vi_e ;
assign ~loc (Cil.var vi) vi_e e ])
in in
e, env e, env
...@@ -349,9 +343,9 @@ module Q = struct ...@@ -349,9 +343,9 @@ module Q = struct
Error.not_yet "reals: cast from R to Z" Error.not_yet "reals: cast from R to Z"
let add_cast ~loc ?name env kf ty e = let add_cast ~loc ?name env kf ty e =
(* TODO: The best solution would actually be to directly write all the needed (* TODO: The best solution would actually be to directly write all the
functions as C builtins then just call them here depending on the situation needed functions as C builtins then just call them here depending on the
at hand. *) situation at hand. *)
assert (Gmp_types.Q.is_t (Cil.typeOf e)); assert (Gmp_types.Q.is_t (Cil.typeOf e));
let get_double e env = let get_double e env =
let _, e, env = let _, e, env =
...@@ -379,8 +373,8 @@ module Q = struct ...@@ -379,8 +373,8 @@ module Q = struct
get_double e env get_double e env
| TFloat(FFloat, _) -> | TFloat(FFloat, _) ->
(* No "get_float" in GMPQ, but fortunately, [float] \subset [double]. (* No "get_float" in GMPQ, but fortunately, [float] \subset [double].
HOWEVER: going through double as intermediate step might be unsound since HOWEVER: going through double as intermediate step might be unsound
it could cause double rounding. See: [Boldo2013, Sec 2.2] since it could cause double rounding. See: [Boldo2013, Sec 2.2]
https://hal.inria.fr/hal-00777639/document *) https://hal.inria.fr/hal-00777639/document *)
let e, env = get_double e env in let e, env = get_double e env in
Options.warning Options.warning
...@@ -410,8 +404,6 @@ module Q = struct ...@@ -410,8 +404,6 @@ module Q = struct
let binop ~loc t_opt bop env kf e1 e2 = let binop ~loc t_opt bop env kf e1 e2 =
let name = name_arith_bop bop in let name = name_arith_bop bop in
(* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
[e2] *)
let e1, env = create ~loc None env kf e1 in let e1, env = create ~loc None env kf e1 in
let e2, env = create ~loc None env kf e2 in let e2, env = create ~loc None env kf e2 in
let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
...@@ -424,8 +416,6 @@ module Q = struct ...@@ -424,8 +416,6 @@ module Q = struct
let cmp ~loc name t_opt bop env kf e1 e2 = let cmp ~loc name t_opt bop env kf e1 e2 =
let fname = "__gmpq_cmp" in let fname = "__gmpq_cmp" in
(* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
[e2] *)
let e1, env = create ~loc None env kf e1 in let e1, env = create ~loc None env kf e1 in
let e2, env = create ~loc None env kf e2 in let e2, env = create ~loc None env kf e2 in
let _, e, env = let _, e, env =
......
...@@ -43,7 +43,7 @@ val assign: loc:location -> lval -> exp -> exp -> stmt ...@@ -43,7 +43,7 @@ val assign: loc:location -> lval -> exp -> exp -> stmt
module Z : sig module Z : sig
val name_arith_bop: binop -> string val name_arith_bop: binop -> string
(** [name_of_mpz_arith_bop bop] returns the name of the GMP function on integer (** [name_of_mpz_arith_bop bop] returns the name of the GMP integer function
corresponding to the [bop] arithmetic operation. *) corresponding to the [bop] arithmetic operation. *)
val new_var: val new_var:
...@@ -57,7 +57,7 @@ module Z : sig ...@@ -57,7 +57,7 @@ module Z : sig
val create: val create:
loc:location -> ?name:string -> term option -> Env.t -> kernel_function -> loc:location -> ?name:string -> term option -> Env.t -> kernel_function ->
exp -> exp * Env.t exp -> exp * Env.t
(** Create an integer *) (** Create an integer number. *)
val add_cast: val add_cast:
loc:location -> ?name:string -> Env.t -> kernel_function -> typ -> exp -> loc:location -> ?name:string -> Env.t -> kernel_function -> typ -> exp ->
...@@ -74,15 +74,16 @@ module Z : sig ...@@ -74,15 +74,16 @@ module Z : sig
val cmp: val cmp:
loc:location -> string -> term option -> binop -> Env.t -> loc:location -> string -> term option -> binop -> Env.t ->
kernel_function -> exp -> exp -> exp * Env.t kernel_function -> exp -> exp -> exp * Env.t
(** Compares two expressions according to the given [binop]. The optional term (** Compares two expressions according to the given [binop]. The optional
indicates whether the comparison has a correspondance in the logic. *) term indicates whether the comparison has a correspondance in the
logic. *)
end end
module Q : sig module Q : sig
val name_arith_bop: binop -> string val name_arith_bop: binop -> string
(** [name_of_mpz_arith_bop bop] returns the name of the GMP function on integer (** [name_of_mpz_arith_bop bop] returns the name of the GMP rational function
corresponding to the [bop] arithmetic operation. *) corresponding to the [bop] arithmetic operation. *)
val normalize_str: string -> string val normalize_str: string -> string
...@@ -95,7 +96,7 @@ module Q : sig ...@@ -95,7 +96,7 @@ module Q : sig
val create: val create:
loc:location -> ?name:string -> term option -> Env.t -> kernel_function -> loc:location -> ?name:string -> term option -> Env.t -> kernel_function ->
exp -> exp * Env.t exp -> exp * Env.t
(** Create a real *) (** Create a rational number. *)
val cast_to_z: loc:location -> ?name:string -> Env.t -> exp -> exp * Env.t val cast_to_z: loc:location -> ?name:string -> Env.t -> exp -> exp * Env.t
(** Assumes that the given exp is of real type and casts it into Z *) (** Assumes that the given exp is of real type and casts it into Z *)
...@@ -115,8 +116,9 @@ module Q : sig ...@@ -115,8 +116,9 @@ module Q : sig
val cmp: val cmp:
loc:location -> string -> term option -> binop -> Env.t -> loc:location -> string -> term option -> binop -> Env.t ->
kernel_function -> exp -> exp -> exp * Env.t kernel_function -> exp -> exp -> exp * Env.t
(** Compares two expressions according to the given [binop]. The optional term (** Compares two expressions according to the given [binop]. The optional
indicates whether the comparison has a correspondance in the logic. *) term indicates whether the comparison has a correspondance in the
logic. *)
end end
......
...@@ -116,8 +116,7 @@ let affect_binop ~loc var_as_varinfo var_as_exp binop exp_type exp1 exp2 = ...@@ -116,8 +116,7 @@ let affect_binop ~loc var_as_varinfo var_as_exp binop exp_type exp1 exp2 =
[exp1; exp2] [exp1; exp2]
| Some e -> | Some e ->
let name = Gmp.Z.name_arith_bop binop in let name = Gmp.Z.name_arith_bop binop in
Smart_stmt.rtl_call Smart_stmt.rtl_call ~loc ~prefix:"" name [e; exp1; exp2])
~loc ~prefix:"" name [e; exp1; exp2])
else if Gmp_types.Q.is_t exp_type then else if Gmp_types.Q.is_t exp_type then
Error.not_yet "rational in affect_binop" Error.not_yet "rational in affect_binop"
else else
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment