Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion lib/CStarToC11.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
16 changes: 11 additions & 5 deletions lib/Simplify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down