[PPL-devel] [GIT] ppl/ppl(master): Fixed a bug where the tokens for widening were not being updated.

Patricia Hill p.m.hill at leeds.ac.uk
Thu Mar 26 11:50:52 CET 2009


Module: ppl/ppl
Branch: master
Commit: aadc083b812f6bc477ad2c4bd08155f04992d310
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=aadc083b812f6bc477ad2c4bd08155f04992d310

Author: Patricia Hill <p.m.hill at leeds.ac.uk>
Date:   Thu Mar 26 10:44:57 2009 +0000

Fixed a bug where the tokens for widening were not being updated.

---

 .../OCaml/ppl_interface_generator_ocaml_cc_code.m4 |   12 +++---
 interfaces/OCaml/tests/test1.ml                    |   36 ++++++++++++++++---
 2 files changed, 36 insertions(+), 12 deletions(-)

diff --git a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4 b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4
index bcb359a..aecad4f 100644
--- a/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4
+++ b/interfaces/OCaml/ppl_interface_generator_ocaml_cc_code.m4
@@ -605,11 +605,11 @@ ppl_ at CLASS@_ at WIDEN@_widening_assign_with_tokens
   CAMLparam3(ph1, ph2, integer);
   @CPP_CLASS@& pph1 = *p_ at CLASS@_val(ph1);
   @CPP_CLASS@& pph2 = *p_ at CLASS@_val(ph2);
-  int cpp_int = Val_int(integer);
+  int cpp_int = Int_val(integer);
   check_int_is_unsigned(cpp_int);
   unsigned int unsigned_value = cpp_int;
   pph1. at WIDEN@_widening_assign(pph2, &unsigned_value);
-  CAMLreturn(Int_val(unsigned_value));
+  CAMLreturn(Val_int(unsigned_value));
 }
 CATCH_ALL
 
@@ -640,11 +640,11 @@ ppl_ at CLASS@_widening_assign_with_tokens(value ph1, value ph2,
   CAMLparam3(ph1, ph2, integer);
   @CPP_CLASS@& pph1 = *p_ at CLASS@_val(ph1);
   @CPP_CLASS@& pph2 = *p_ at CLASS@_val(ph2);
-  int cpp_int = Val_int(integer);
+  int cpp_int = Int_val(integer);
   check_int_is_unsigned(cpp_int);
   unsigned int unsigned_value = cpp_int;
   pph1.widening_assign(pph2, &unsigned_value);
-  CAMLreturn(Int_val(unsigned_value));
+  CAMLreturn(Val_int(unsigned_value));
 }
 CATCH_ALL
 
@@ -662,12 +662,12 @@ ppl_ at CLASS@_ at LIMITEDBOUNDED@_ at WIDENEXPN@_extrapolation_assign_with_tokens(value
   @CPP_CLASS@& pph1 = *p_ at CLASS@_val(ph1);
   @CPP_CLASS@& pph2 = *p_ at CLASS@_val(ph2);
   @!CONSTRAINER at _System ppl_cs = build_ppl_@!CONSTRAINER at _System(caml_cs);
-  int cpp_int = Val_int(integer);
+  int cpp_int = Int_val(integer);
   check_int_is_unsigned(cpp_int);
   unsigned int unsigned_value = cpp_int;
   pph1. at LIMITEDBOUNDED@_ at WIDENEXPN@_extrapolation_assign(pph2, ppl_cs,
 							 &unsigned_value);
-  CAMLreturn(Int_val(unsigned_value));
+  CAMLreturn(Val_int(unsigned_value));
 }
 CATCH_ALL
 
diff --git a/interfaces/OCaml/tests/test1.ml b/interfaces/OCaml/tests/test1.ml
index 8a69ebc..5b1d06b 100644
--- a/interfaces/OCaml/tests/test1.ml
+++ b/interfaces/OCaml/tests/test1.ml
@@ -203,7 +203,6 @@ let e3 =
   -/
   (linear_expression_of_int 7)
 ;;
-
 print_linear_expression e3; print_string_if_noisy "\n" ;;
 
 (* Probably the most convenient thing for the user will be to use the
@@ -248,6 +247,16 @@ for i = 6 downto 0 do
 done;;
 print_string_if_noisy "\n";;
 
+let c1 = (a  >=/ linear_expression_of_int 0);;
+let c2 = (a  <=/ linear_expression_of_int 2);;
+let c2a = (a  <=/ linear_expression_of_int 3);;
+let c3 = (b  >=/ linear_expression_of_int 0);;
+let c4 = (b  <=/ linear_expression_of_int 2);;
+let cs1 = [c1; c2; c3; c4];;
+let cs2 = [c1; c2a; c3; c4];;
+let poly1 = ppl_new_C_Polyhedron_from_constraints(cs1);;
+let poly2 = ppl_new_C_Polyhedron_from_constraints(cs2);;
+
 let polyhedron1 = ppl_new_C_Polyhedron_from_constraints(constraints1);;
 let polyhedron2 = ppl_new_C_Polyhedron_from_generators(generators1);;
 let result =  ppl_Polyhedron_bounds_from_above polyhedron1 e2;;
@@ -267,17 +276,32 @@ ppl_Polyhedron_concatenate_assign polyhedron1 polyhedron2;;
 let congruences = ppl_Polyhedron_get_congruences polyhedron1 in
 List.iter print_congruence congruences;;
 print_string_if_noisy "\n";;
+
+print_string_if_noisy "\nTesting affine transformations \n";;
 ppl_Polyhedron_bounded_affine_preimage polyhedron1 1 e1 e2 (Z.from_int 10);;
 ppl_Polyhedron_bounded_affine_preimage polyhedron1 1 e1 e2 (Z.from_int 10);;
 ppl_Polyhedron_affine_image polyhedron1 1 e1 (Z.from_int 10);;
-let a = ppl_Polyhedron_limited_BHRZ03_extrapolation_assign_with_tokens
+
+print_string_if_noisy "\nTesting widenings and extrapolations \n";;
+let tokens_l_BHRZ03 =
+  ppl_Polyhedron_limited_BHRZ03_extrapolation_assign_with_tokens
   polyhedron1 polyhedron1 constraints1 10;;
-let b = ppl_Polyhedron_bounded_BHRZ03_extrapolation_assign_with_tokens
+let tokens_b_BHRZ03 =
+  ppl_Polyhedron_bounded_BHRZ03_extrapolation_assign_with_tokens
   polyhedron1 polyhedron1 constraints1 10;;
-let b = ppl_Polyhedron_bounded_H79_extrapolation_assign_with_tokens
+let tokens_b_H79 = ppl_Polyhedron_bounded_H79_extrapolation_assign_with_tokens
   polyhedron1 polyhedron1 constraints1 10;;
- ppl_Polyhedron_H79_widening_assign polyhedron1 ;;
-print_int_if_noisy b;;
+let tokens_H79 = ppl_Polyhedron_H79_widening_assign_with_tokens poly2 poly1 2;;
+ppl_Polyhedron_H79_widening_assign polyhedron1 polyhedron1 ;;
+print_string_if_noisy "tokens b_H79 = ";;
+print_int_if_noisy tokens_b_H79;;
+print_string_if_noisy "\n";;
+print_string_if_noisy "tokens b_BHRZ03 = ";;
+print_int_if_noisy tokens_b_BHRZ03;;
+print_string_if_noisy "\n";;
+print_string_if_noisy "tokens H79 = ";;
+print_int_if_noisy tokens_H79;;
+print_string_if_noisy "\n";;
 
 let b = ppl_Polyhedron_OK polyhedron1;;
 ppl_Polyhedron_generalized_affine_preimage_lhs_rhs




More information about the PPL-devel mailing list