Skip to content

Commit 6101935

Browse files
committed
Fix ValueDomain indentation
1 parent c477445 commit 6101935

File tree

1 file changed

+18
-18
lines changed

1 file changed

+18
-18
lines changed

src/cdomain/value/cdomains/valueDomain.ml

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -438,24 +438,24 @@ struct
438438
function
439439
| Addr.Addr ({ vtype; _} as v, o) as a ->
440440
begin match Cil.unrollType vtype, Cil.unrollType t with
441-
(* only allow conversion of float pointers if source and target type are the same *)
442-
| TFloat (fkind, _), TFloat (fkind', _) when fkind = fkind' -> a
443-
(* do not allow conversion from/to float pointers*)
444-
| TFloat _, _
445-
| _, TFloat _ -> UnknownPtr
446-
| TVoid _, _ when not (Cilfacade.isCharType t) -> (* we had no information about the type (e.g. malloc), so we add it; ignore for casts to char* since they're special conversions (N1570 6.3.2.3.7) *)
447-
Addr ({ v with vtype = t }, o) (* HACK: equal varinfo with different type, causes inconsistencies down the line, when we again assume vtype being "right", but joining etc gives no consideration to which type version to keep *)
448-
| _, _ ->
449-
begin try Addr (v, (adjust_offs v o None)) (* cast of one address by adjusting the abstract offset *)
450-
with
451-
| CastError s -> (* don't know how to handle this cast :( *)
452-
if M.tracing then M.tracel "caste" "%s" s;
453-
a (* probably garbage, but this is deref's problem *)
454-
(*raise (CastError s)*)
455-
| SizeOfError (s,t) ->
456-
M.warn "size of error: %s" s;
457-
a
458-
end
441+
(* only allow conversion of float pointers if source and target type are the same *)
442+
| TFloat (fkind, _), TFloat (fkind', _) when fkind = fkind' -> a
443+
(* do not allow conversion from/to float pointers*)
444+
| TFloat _, _
445+
| _, TFloat _ -> UnknownPtr
446+
| TVoid _, _ when not (Cilfacade.isCharType t) -> (* we had no information about the type (e.g. malloc), so we add it; ignore for casts to char* since they're special conversions (N1570 6.3.2.3.7) *)
447+
Addr ({ v with vtype = t }, o) (* HACK: equal varinfo with different type, causes inconsistencies down the line, when we again assume vtype being "right", but joining etc gives no consideration to which type version to keep *)
448+
| _, _ ->
449+
begin try Addr (v, (adjust_offs v o None)) (* cast of one address by adjusting the abstract offset *)
450+
with
451+
| CastError s -> (* don't know how to handle this cast :( *)
452+
if M.tracing then M.tracel "caste" "%s" s;
453+
a (* probably garbage, but this is deref's problem *)
454+
(*raise (CastError s)*)
455+
| SizeOfError (s,t) ->
456+
M.warn "size of error: %s" s;
457+
a
458+
end
459459
end
460460
| x -> x (* TODO we should also keep track of the type here *)
461461
in

0 commit comments

Comments
 (0)