2021-01-18 17:00 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000730Frama-CPlug-in > Evapublic2014-02-12 16:54
Assigned Topascal 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000730: Print addresses in hexadecimal
DescriptionIt would be really helpful to have an option that asks the value analysis to print memory addresses in hexadecimal instead of base 10 integers.
That is, print eg. NULL[117445956..117445959] as NULL[0x7001544-7001547]. I think this would also be fine for smaller offsets.

I tried to do the change myself, but Big_int.to_hex_string (or anything equivalent) does not exists... Ideas are welcome.
TagsNo tags attached.
Attached Files




signoles (manager)

Could be a kernel option if some other plug-ins would print addresses?


pascal (reporter)

I think that Boris does not wish to see all integers printed as hexadecimal (if he was that kind of person he would know how to convert an integer to a string of its hexadecimal representation). It seems he wants hexadecimal only for offsets associated to base NULL in Location_bytes, when these Location_bytes are used as addresses. The problem is that last part: there is no way to distinguish an integer that is in fact an absolute address in memory from an integer that is in fact an integer.


yakobowski (manager)

After some testing, the patch would be either quite invasive, or incomplete. Something more reasonable would be to print all values above a certain treshold as hexadecimal. This works quite well in practice, and has the added benefit of printing [min_int..max_int] ranges in a readable way.

(All is not perfect, though. For example, should min_int be printed as "-" ^ (-minint), or using two's complement. The second has the drawback of depending on the range of the value being printed. The first uses an integer that the Ocaml parser may refuse.)


yakobowski (manager)

Last solution has been implemented : all ints greater than a user-selected value are printed in hexadecimal.

-Issue History
Date Modified Username Field Change
2011-02-18 00:44 yakobowski New Issue
2011-02-18 00:44 yakobowski Status new => assigned
2011-02-18 00:44 yakobowski Assigned To => pascal
2011-02-18 09:36 signoles Note Added: 0001514
2011-02-20 18:18 pascal Note Added: 0001524
2011-02-24 14:31 yakobowski Note Added: 0001530
2011-03-11 12:53 yakobowski Note Added: 0001595
2011-03-11 13:07 svn
2011-03-11 13:08 yakobowski Status assigned => resolved
2011-03-11 13:08 yakobowski Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 yakobowski Source_changeset_attached => framac master accf6dc1
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon accf6dc1
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History