Commit f8dd6af6 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

negative literals: protect against bad usage of ls_of_const

parent 6ee33b56
...@@ -524,9 +524,9 @@ let rec tr_positive p = match kind_of_term p with ...@@ -524,9 +524,9 @@ let rec tr_positive p = match kind_of_term p with
| _ -> | _ ->
raise NotArithConstant raise NotArithConstant
let const_of_big_int is_negative b = let const_of_big_int is_neg b =
Term.t_const Term.t_const
(Number.(ConstInt { ic_negative = is_negative ; (Number.(ConstInt { ic_negative = is_neg ;
ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) })) ic_abs = Number.int_const_dec (Big_int.string_of_big_int b) }))
ty_int ty_int
......
...@@ -83,11 +83,13 @@ let lsdecl_of_ts ts = create_param_decl (ls_of_ts ts) ...@@ -83,11 +83,13 @@ let lsdecl_of_ts ts = create_param_decl (ls_of_ts ts)
(* convert a constant to a functional symbol of type ty_base *) (* convert a constant to a functional symbol of type ty_base *)
let ls_of_const = let ls_of_const =
Hty.memo 3 (fun ty_base -> Hty.memo 3 (fun ty_base ->
Hterm.memo 63 (fun t -> match t.t_node with Hterm.memo 63 (fun t ->
| Tconst _ -> match t.t_node with
let s = "const_" ^ Pp.string_of_wnl Pretty.print_term t in | Tconst c ->
create_fsymbol (id_fresh s) [] ty_base assert (not (Number.is_negative c));
| _ -> assert false)) let s = "const_" ^ Pp.string_of_wnl Pretty.print_term t in
create_fsymbol (id_fresh s) [] ty_base
| _ -> assert false))
let ls_of_const ty_base t = ls_of_const ty_base (t_label Slab.empty t) let ls_of_const ty_base t = ls_of_const ty_base (t_label Slab.empty t)
......
...@@ -37,6 +37,11 @@ type constant = ...@@ -37,6 +37,11 @@ type constant =
| ConstInt of integer_constant | ConstInt of integer_constant
| ConstReal of real_constant | ConstReal of real_constant
let is_negative c =
match c with
| ConstInt i -> i.ic_negative
| ConstReal r -> r.rc_negative
exception InvalidConstantLiteral of int * string exception InvalidConstantLiteral of int * string
let invalid_constant_literal n s = raise (InvalidConstantLiteral(n,s)) let invalid_constant_literal n s = raise (InvalidConstantLiteral(n,s))
......
...@@ -39,6 +39,8 @@ type constant = ...@@ -39,6 +39,8 @@ type constant =
| ConstInt of integer_constant | ConstInt of integer_constant
| ConstReal of real_constant | ConstReal of real_constant
val is_negative : constant -> bool
val int_const_dec : string -> integer_literal val int_const_dec : string -> integer_literal
val int_const_hex : string -> integer_literal val int_const_hex : string -> integer_literal
val int_const_oct : string -> integer_literal val int_const_oct : string -> integer_literal
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment