From 7110b0227b580b174cc390bad9bc93a82b058e96 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 2 Mar 2020 19:33:31 +0100
Subject: [PATCH] [crowbar] less UB in generated casts
---
tests/crowbar/constfold.ml | 18 +++++++++++-------
1 file changed, 11 insertions(+), 7 deletions(-)
diff --git a/tests/crowbar/constfold.ml b/tests/crowbar/constfold.ml
index 4bfcc8a7a35..6adcf9fd6b3 100644
--- a/tests/crowbar/constfold.ml
+++ b/tests/crowbar/constfold.ml
@@ -83,7 +83,14 @@ let protected_cast t e =
mk_exp(BINARY(GE,e,mk_exp (CONSTANT(CONST_INT("0"))))),
e,
mk_exp(CONSTANT(CONST_INT("0")))))
- | _ -> e
+ | _ ->
+ let max = mk_exp (CONSTANT(CONST_INT("255"))) in
+ let min = mk_exp (UNARY(MINUS,max)) in
+ mk_exp(
+ QUESTION(
+ mk_exp(BINARY(GE,e,min)),
+ mk_exp(QUESTION(mk_exp(BINARY(LE,e,max)),e,max)),
+ min))
let gen_expr =
fix
@@ -165,10 +172,7 @@ let () = Dynamic.set_module_load_path [ "lib/plugins" ]
let () = Dynamic.load_module "frama-c-eva"
-let on_from_name s f =
- Project.on (Project.from_unique_name s) f ()
-let () =
-Cmdline.run_after_extended_stage (fun () -> Format.printf "Extended stage@.")
+let on_from_name s f = Project.on (Project.from_unique_name s) f ()
let () =
Cmdline.(
@@ -185,11 +189,11 @@ let run typ expr =
Kernel.SignedDowncast.off ();
Kernel.UnsignedOverflow.off ();
Kernel.UnsignedDowncast.off ();
+ Kernel.add_debug_keys Kernel.dkey_constfold;
(* otherwise, we must load scope in addition to eva. *)
Dynamic.Parameter.Bool.off "-eva-remove-redundant-alarms" ();
Errorloc.clear_errors ();
- Format.printf "This is the cabs:@\n%a@."
- Cprint.printFile cabs;
+ Format.printf "Cabs is@\n%a@." Cprint.printFile cabs;
let cil =
try Cabs2cil.convFile cabs
with exn ->
--
GitLab