TODO list


CIL
------

Front-end
 - trigraph sequences (??:, ...) ISO 5.2.1.1
 - name spaces for struct/enum/union are the same ISO 6.2.3
 - check integer conversion ISO 6.3.1.1
 - character constants (type, value, escapes) ISO 6.4.4.4
 - string literals (value, escapes) ISO 6.4.5
 - punctuation tokens ISO 6.4.6
 - default argument promotions in function calls ISO 6.5.2.2
 - compound literals ISO 6.5.2.5. Missing fields initialized to 0!!
 - check that long long is properly done in type specs ISO 6.7.2
 - Initialization ISO 6.7.8

- MSVC has a bug in the handling of shift operators: arithemtic conversions
are applies on both operands instead of just integral promotions. We duplicate
this bug in doBinOp in cabs2cil.

 - we should allow the user to specify a logging function that takes
   printf()-style arguments (rather than hardcoding syslog/printk/printf). 

 - the restrict attribute is dropped in cabs2cil

 - struct and union must share the name space

 - when merging we use too much memory. We should be droping the references to
 the CABS files once we convert each one to CIL.

CCURED
==============

 - if we use memcpy to copy some stuff from local variables to the heap we
 might be moving stack pointers that way. The only way to prevent that is to
 disallow storing stack pointers in local variables that are arrays or whose
 address is taken.

 - in box.ml offsetOfFirstScalar looks only at the first field of a union.

 - in box.ml when we check tags we check all fields in a union. This is sound
   but excessive. 

(2) Make a file with global declarations of common functions like strcpy().
    These declarations should include pointer annotations and should be
    used instead of the ones that appear in the source.
?(9) Find some way to describe [recursive] types at runtime and use them as
     tags. 


 - on MSVC we turn on 32-bit packing of stuff

 - Writing or reading unaligned pointers is not allowed. 

 - Right now when we try to read a pointer and we don't find one in tags, we
   overwrite the base part of the pointer to be read with 0. But this might
   have undesired side-effects.

 - I wonder what do we do when casting between abstract types (struct foo *
   where struct foo is not defined)

 - change CHECK_RETURNPTR and CHECK_STOREPTR so that the range checked
    is 512K (instead of 1 meg) for Linux Kernel Drivers.

 - add a flag that effectively puts #pragma box(off) / #pragma box(on)
   around all global initializers in a file. 


 - turning interface char* into ROSTRING is unsound. This is done even when
   the item is subject to writes. 

 - printf is not quite safe. If we do not manage to verify statically the
   arguments we should be calling a wrapper. Do we do that? 

 - in a SEQ pointer we must keep the end = null if the poiner is an integer.
   Else there is trouble when we cast to FSEQ. Can we cast integers into FSEQ?

   
 - sm: because wild area lengths have word-level granularity, we can't protect
   the final 0 of a char array unless the alignment works out; solutions
   include changing granularity to bytes (painful) or changing the array-
   expander to ensure alignment (potentially wasteful of a few bytes here
   and there)