diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml index 12125d84..f8c9cf9b 100644 --- a/lib/CStarToC11.ml +++ b/lib/CStarToC11.ml @@ -1301,7 +1301,6 @@ let mk_type_or_external m (w: where) ?(is_inline_static=false) (d: decl): C.decl (Z.of_int (List.length cases)), if custom_values <> [] then List.hd custom_values else Z.zero in - KPrint.bprintf "max_value=%s, min_value=%s\n" (Z.to_string max_value) (Z.to_string min_value); let t = if Z.(geq min_value zero && leq max_value (of_string "0xff")) then K.UInt8 diff --git a/lib/Simplify.ml b/lib/Simplify.ml index 94788715..c900ec96 100644 --- a/lib/Simplify.ml +++ b/lib/Simplify.ml @@ -132,11 +132,17 @@ let use_mark_to_inline_temporaries = object (self) b.node.name = "scrut" || Structs.should_rewrite b.typ = NoCopies ) && - v = AtMost 1 && ( - is_readonly_c_expression e1 && - safe_readonly_use e2 || - safe_pure_use e2 - ) (* || is_readonly_and_variable_free_c_expression e1 && b.node.mut *) + (v = AtMost 1 && ( + is_readonly_c_expression e1 && + safe_readonly_use e2 || + safe_pure_use e2 + ) || + is_readonly_and_variable_free_c_expression e1 && not b.node.mut) + (* b.node.mut is an approximation of "the address of this variable is taken" + -- TODO this is somewhat incompatible with the phase that changes size-1 + arrays into variables who address is taken, so we should also check beore + inlining that the address of this variable is not taken... this is + starting to be quite an expensive check! *) then (* Don't drop a potentially useful comment into the ether *) let e1 = { e1 with meta = e1.meta @ b.meta } in