Strings in value analysis results
ID0001191: This issue was created automatically from Mantis Issue 1191. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001191 | Frama-C | Plug-in > Eva | public | 2012-06-08 | 2012-11-18 |
| Reporter | Anne | Assigned To | pascal | Resolution | won't fix |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
String constant are nicely printed in value analysis results, but other strings are not (see additional information). Wouldn't it be possible (I mean: not too much work) to also print nicely the known variable strings ?
Additional Information :
For the file : int main (void) { char toto[] = "bonjour"; char * titi = "coucou"; char * ptoto = toto; char * ptiti = titi; return 0; } $ frama-c -val toto.c [value] Values for function main: toto[0] ? {98} [1] ? {111} [2] ? {110} [3] ? {106} [4] ? {111} [5] ? {117} [6] ? {114} [7] ? {0} titi ? {{ &"coucou" }} ptoto ? {{ &toto }} ptiti ? {{ &"coucou" }}
It would be nice to have toto ? {"bonjour"} when there is only one possible value. (I understand that if some of the character can have several values, you cannot enumerate all the possible strings...)