Skip to content

Commit da7ab8c

Browse files
committed
Implement SizeOfE in eval_rv_base
1 parent 2466d25 commit da7ab8c

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

src/analyses/base.ml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -960,9 +960,13 @@ struct
960960
| bytes -> Int (ID.of_int !Cil.kindOfSizeOf (Z.of_int bytes))
961961
| exception SizeOfError _ -> Int (ID.top_of !Cil.kindOfSizeOf) (* TODO: does this ever happen? *)
962962
end
963+
| SizeOfE e -> (* based on [Cil.constFold true] and inlined SizeOf *)
964+
begin match Cilfacade.bytesSizeOf (Cilfacade.typeOf e) with
965+
| bytes -> Int (ID.of_int !Cil.kindOfSizeOf (Z.of_int bytes))
966+
| exception SizeOfError _ -> Int (ID.top_of !Cil.kindOfSizeOf) (* TODO: does this ever happen? *)
967+
end
963968
| Real _
964969
| Imag _
965-
| SizeOfE _
966970
| SizeOfStr _
967971
| AlignOf _
968972
| AlignOfE _

0 commit comments

Comments
 (0)